rwth.i2.ltlrv.management
Interface IFormulaFactory

All Known Implementing Classes:

FormulaFactory

public interface IFormulaFactory

IFormulaFactory - Common interface for formula factories. Used ot instantiate formulae of any kind.

Author:

Eric Bodden

Method Summary

IAnd	And(IFormula formula1, IFormula formula2) Generates an conjunct.
IEquivalent	Eq(IFormula formula1, IFormula formula2) Generates an equivalence relation.
IFinally	F(IFormula formula) Generates a Finally formula.
IFF	FF() Returns the negative positive sink state.
IGlobally	G(IFormula formula) Generates a Globally formula.
IImplies	Impl(IFormula formula1, IFormula formula2) Generates an implication.
INot	Not(IFormula formula) Generates a negation.
IOr	Or(IFormula formula1, IFormula formula2) Generates an disjunct.
IProposition	Proposition(String label, String... boundFormals) Returns a proposition with the given parameters.
IProposition	Proposition(String label, String[] boundFormals, IIfClosure[] ifClosures) Returns a proposition with the given parameters.
IProposition	Proposition(String label, WeakValuesMap<String,Object> bindings) Deprecated.
IRelease	Release(IFormula formula1, IFormula formula2) Generates a Release formula.
ITT	TT() Returns the unique positive sink state.
IUntil	Until(IFormula formula1, IFormula formula2) Generates an Until formula.
INext	X(IFormula formula) Generates a Next formula.

Method Detail

And

IAnd And(IFormula formula1,
         IFormula formula2)

Generates an conjunct.

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 /\ formula2

Or

IOr Or(IFormula formula1,
       IFormula formula2)

Generates an disjunct.

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 \/ formula2

Impl

IImplies Impl(IFormula formula1,
              IFormula formula2)

Generates an implication.

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 -> formula2

Eq

IEquivalent Eq(IFormula formula1,
               IFormula formula2)

Generates an equivalence relation.

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 <-> formula2

Release

IRelease Release(IFormula formula1,
                 IFormula formula2)

Generates a Release formula.

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 R formula2

Until

IUntil Until(IFormula formula1,
             IFormula formula2)

Generates an Until formula.

Parameters:

formula1 - left subformula

formula2 - right subformula

Returns:

formula1 U formula2

F

IFinally F(IFormula formula)

Generates a Finally formula.

Parameters:

formula - the subformula

Returns:

F subformula

G

IGlobally G(IFormula formula)

Generates a Globally formula.

Parameters:

formula - the subformula

Returns:

G subformula

X

INext X(IFormula formula)

Generates a Next formula.

Parameters:

formula - the subformula

Returns:

X subformula

Not

INot Not(IFormula formula)

Generates a negation.

Parameters:

formula - the subformula

Returns:

! subformula

TT

ITT TT()

Returns the unique positive sink state.

Returns:

TT

FF

IFF FF()

Returns the negative positive sink state.

Returns:

TT

Proposition

IProposition Proposition(String label,
                         String... boundFormals)

Returns a proposition with the given parameters.

Parameters:

label - a label; this should be distinct for semantically distinct propositions

boundFormals - the formals which will be bound by this pointcut at runtime

Returns:

an appropriate proposition with boundFormals initialized to IProposition.UNBOUND

Proposition

IProposition Proposition(String label,
                         String[] boundFormals,
                         IIfClosure[] ifClosures)

Returns a proposition with the given parameters.

Parameters:

label - a label; this should be distinct for semantically distinct propositions

boundFormals - the formals which will be bound by this pointcut at runtime

ifClosures - the if-closures which this pointcut has to satisfy (@see IIfClosure)

Returns:

an appropriate proposition with boundFormals initialized to IProposition.UNBOUND

Proposition

@Deprecated
IProposition Proposition(String label,
                                    WeakValuesMap<String,Object> bindings)

Deprecated.

This is only to be used by the test harness!

Parameters:

label - a label; this should be distinct for semantically distinct propositions

bindings - a map of current bindings

Returns:

an appropriate proposition with the given bindings