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