## 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