Uses of Interface
rwth.i2.ltlrv.formula.interfaze.IFormula

Packages that use IFormula

rwth.i2.ltlrv.afastate.base	Abstract base classes for all AFA states.
rwth.i2.ltlrv.afastate.impl	Implementing classes of AFA states.
rwth.i2.ltlrv.afastate.interfaze	Common interfaces for all AFA states.
rwth.i2.ltlrv.formula.base	Abstract base classes for LTL term constructors.
rwth.i2.ltlrv.formula.impl	Implementing classes for LTL term constructors.
rwth.i2.ltlrv.formula.interfaze	Common interfaces for LTL term constructors.
rwth.i2.ltlrv.management	Holds classes for configuration management and formula creation.

Uses of IFormula in rwth.i2.ltlrv.afastate.base

Classes in rwth.i2.ltlrv.afastate.base that implement IFormula

class	AbstractAFAState Abstract superclass of all formulae.
class	BinaryAFAState BinaryAFAState - Abstract superclass of all binary formulae.
class	CommutativeBinaryAFAState Represents a binary formula, which is commutative.
class	NullaryAFAState NullaryAFAState - Abstract base class of all nullary AFA states.
class	UnaryAFAState UnaryAFAState - Abstract superclass of all unary formulae.

Fields in rwth.i2.ltlrv.afastate.base declared as IFormula

protected IFormula	UnaryAFAState.subformula the subformula
protected IFormula	BinaryAFAState.subformula1 the subformulae
protected IFormula	BinaryAFAState.subformula2 the subformulae

Methods in rwth.i2.ltlrv.afastate.base that return IFormula

IFormula	UnaryAFAState.getSubformula()
IFormula	BinaryAFAState.getSubformula1()
IFormula	BinaryAFAState.getSubformula2()

Constructors in rwth.i2.ltlrv.afastate.base with parameters of type IFormula

BinaryAFAState(IFormula subformula1, IFormula subformula2)

CommutativeBinaryAFAState(IFormula subformula1, IFormula subformula2)

UnaryAFAState(IFormula subformula)

Uses of IFormula in rwth.i2.ltlrv.afastate.impl

Classes in rwth.i2.ltlrv.afastate.impl that implement IFormula

class	And And - Implements a conjunct.
class	FF FF - Implements the sink state / formula representing false.
class	Next Next - Implements the Next formula constructor of LTL.
class	Not Not - Implements the Not operator.
class	Or Or - Implements a disjunct.
class	Proposition Proposition - Implements a proposition.
class	Release Release - Implements the Release operator in LTL.
class	TT TT - Implements the sink state / formula representing true.
class	Until Until - Implements the Until operator in LTL.

Methods in rwth.i2.ltlrv.afastate.impl with parameters of type IFormula

IAFAState	Not.reconstruct(IFormula t) Creates a formula with the same operator as this but a different subformula.
IAFAState	Next.reconstruct(IFormula t) Creates a formula with the same operator as this but a different subformula.
IAFAState	Until.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.
IAFAState	Release.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.
IAFAState	Or.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.
IAFAState	And.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.

Constructors in rwth.i2.ltlrv.afastate.impl with parameters of type IFormula

And(IFormula subFormula1, IFormula subFormula2)
Constructs a conjunt of the two subformulae.

Next(IFormula subFormula)
Constructs a new formula with the given subformula.

Not(IFormula subFormula)
A negated form of the subformula passed in.

Or(IFormula subFormula1, IFormula subFormula2)
A disjunct of the two subformulae.

Release(IFormula subFormula1, IFormula subFormula2)
Constructs a new formula with the given subformulae.

Until(IFormula subFormula1, IFormula subFormula2)
Constructs a new formula with the given subformulae.

Uses of IFormula in rwth.i2.ltlrv.afastate.interfaze

Subinterfaces of IFormula in rwth.i2.ltlrv.afastate.interfaze

interface	IAFAState This interface reflects any subformula which is valid as input for AFA generation.
interface	IAnd IAnd represents a conjunct.
interface	IBinaryAFAState IBinaryAFAState - Common interface for all binary AFA states.
interface	IFF IFF represents FF = false
interface	INext INext represents the Next operator
interface	INot INot represents the negation operator
interface	INullaryAFAState INullaryAFAState - Common interface for nullary AFA states.
interface	IOr IOr represents a disjunct
interface	IProposition IProposition represents a proposition
interface	IRelease IRelease - Interface representing the binary Release operator in LTL.
interface	ITT ITT represents TT = true
interface	IUnaryAFAState IUnaryAFAState - Common interface for unary AFA states.
interface	IUntil IUntil - Interface representing the binary Until operator in LTL.

Methods in rwth.i2.ltlrv.afastate.interfaze with parameters of type IFormula

IAFAState	IUnaryAFAState.reconstruct(IFormula subformula) Creates a formula with the same operator as this but a different subformula.
IAFAState	IBinaryAFAState.reconstruct(IFormula subformula1, IFormula subformula2) Creates a formula with the same operator as this but different subformulae.

Uses of IFormula in rwth.i2.ltlrv.formula.base

Classes in rwth.i2.ltlrv.formula.base that implement IFormula

class	AbstractFormula AbstractFormula - abstract superclass of all formulae.
class	BinaryFormula BinaryFormula - Abstract superclass of all binary formulae.
class	CommutativeBinaryFormula CommutativeBinaryFormula - Abstract superclass of all binary formulae which are commutative.
class	UnaryFormula BinaryFormula - Abstract superclass of all unary formulae.

Fields in rwth.i2.ltlrv.formula.base declared as IFormula

protected IFormula	UnaryFormula.subformula the subformula
protected IFormula	BinaryFormula.subformula1 the subformulae
protected IFormula	BinaryFormula.subformula2 the subformulae

Methods in rwth.i2.ltlrv.formula.base that return IFormula

IFormula	UnaryFormula.getSubformula()
IFormula	BinaryFormula.getSubformula1()
IFormula	BinaryFormula.getSubformula2()

Constructors in rwth.i2.ltlrv.formula.base with parameters of type IFormula

BinaryFormula(IFormula subformula1, IFormula subformula2)

CommutativeBinaryFormula(IFormula subformula1, IFormula subformula2)

UnaryFormula(IFormula subformula)

Uses of IFormula in rwth.i2.ltlrv.formula.impl

Classes in rwth.i2.ltlrv.formula.impl that implement IFormula

class	Equivalent Equivalent - Implements the equivalent relation as subformula.
class	Finally Finally - Implements the Finally formula constructor of LTL.
class	Globally Globally - Implements the Globally formula constructor of LTL.
class	Implies Implies - Implements the Implies relation as subformula.

Constructors in rwth.i2.ltlrv.formula.impl with parameters of type IFormula

Equivalent(IFormula subFormula1, IFormula subFormula2)
Constructs an equivalent relation for the two subformulae.

Finally(IFormula subFormula)
Constructs a new formula with the given subformula.

Globally(IFormula subFormula)
Constructs a new formula with the given subformula.

Implies(IFormula subFormula1, IFormula subFormula2)

Uses of IFormula in rwth.i2.ltlrv.formula.interfaze

Subinterfaces of IFormula in rwth.i2.ltlrv.formula.interfaze

interface	IBinaryTerm IBinaryTerm - Common interface for a binary term.
interface	IEquivalent IEquivalent represents the equivalence operator
interface	IFinally IFinally represents the finally operator
interface	IGlobally IGlobally represents the globally operator
interface	IImplies IImplies represents the Implication operator
interface	IUnaryTerm IUnaryTerm - Common interface for a unary term.

Methods in rwth.i2.ltlrv.formula.interfaze that return IFormula

IFormula	IUnaryTerm.getSubformula()
IFormula	IBinaryTerm.getSubformula1()
IFormula	IBinaryTerm.getSubformula2()

Uses of IFormula in rwth.i2.ltlrv.management

Methods in rwth.i2.ltlrv.management with parameters of type IFormula

IAnd	IFormulaFactory.And(IFormula formula1, IFormula formula2) Generates an conjunct.
IAnd	FormulaFactory.And(IFormula formula1, IFormula formula2) Generates an conjunct.
IEquivalent	IFormulaFactory.Eq(IFormula formula1, IFormula formula2) Generates an equivalence relation.
IEquivalent	FormulaFactory.Eq(IFormula formula1, IFormula formula2) Generates an equivalence relation.
IFinally	IFormulaFactory.F(IFormula formula) Generates a Finally formula.
IFinally	FormulaFactory.F(IFormula formula) Generates a Finally formula.
IGlobally	IFormulaFactory.G(IFormula formula) Generates a Globally formula.
IGlobally	FormulaFactory.G(IFormula formula) Generates a Globally formula.
IImplies	IFormulaFactory.Impl(IFormula formula1, IFormula formula2) Generates an implication.
IImplies	FormulaFactory.Impl(IFormula formula1, IFormula formula2) Generates an implication.
INot	IFormulaFactory.Not(IFormula formula) Generates a negation.
INot	FormulaFactory.Not(IFormula formula) Generates a negation.
IOr	IFormulaFactory.Or(IFormula formula1, IFormula formula2) Generates an disjunct.
IOr	FormulaFactory.Or(IFormula formula1, IFormula formula2) Generates an disjunct.
void	VerificationRuntime.registerFormula(String formulaId, IFormula formula) Registers a new formula.
IRelease	IFormulaFactory.Release(IFormula formula1, IFormula formula2) Generates a Release formula.
IRelease	FormulaFactory.Release(IFormula formula1, IFormula formula2) Generates a Release formula.
IUntil	IFormulaFactory.Until(IFormula formula1, IFormula formula2) Generates an Until formula.
IUntil	FormulaFactory.Until(IFormula formula1, IFormula formula2) Generates an Until formula.
INext	IFormulaFactory.X(IFormula formula) Generates a Next formula.
INext	FormulaFactory.X(IFormula formula) Generates a Next formula.