|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
public interface IFormulaFactory
IFormulaFactory - Common interface for formula factories. Used ot instantiate formulae of any kind.
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 |
---|
IAnd And(IFormula formula1, IFormula formula2)
formula1
- left subformulaformula2
- right subformula
formula1 /\ formula2
IOr Or(IFormula formula1, IFormula formula2)
formula1
- left subformulaformula2
- right subformula
formula1 \/ formula2
IImplies Impl(IFormula formula1, IFormula formula2)
formula1
- left subformulaformula2
- right subformula
formula1 -> formula2
IEquivalent Eq(IFormula formula1, IFormula formula2)
formula1
- left subformulaformula2
- right subformula
formula1 <-> formula2
IRelease Release(IFormula formula1, IFormula formula2)
formula1
- left subformulaformula2
- right subformula
formula1 R formula2
IUntil Until(IFormula formula1, IFormula formula2)
formula1
- left subformulaformula2
- right subformula
formula1 U formula2
IFinally F(IFormula formula)
formula
- the subformula
F subformula
IGlobally G(IFormula formula)
formula
- the subformula
G subformula
INext X(IFormula formula)
formula
- the subformula
X subformula
INot Not(IFormula formula)
formula
- the subformula
! subformula
ITT TT()
TT
IFF FF()
TT
IProposition Proposition(String label, String... boundFormals)
label
- a label; this should be distinct for semantically distinct propositionsboundFormals
- the formals which will be bound by this pointcut at runtime
boundFormals
initialized to
IProposition.UNBOUND
IProposition Proposition(String label, String[] boundFormals, IIfClosure[] ifClosures)
label
- a label; this should be distinct for semantically distinct propositionsboundFormals
- the formals which will be bound by this pointcut at runtimeifClosures
- the if-closures which this pointcut has to satisfy
(@see IIfClosure)
boundFormals
initialized to
IProposition.UNBOUND
@Deprecated IProposition Proposition(String label, WeakValuesMap<String,Object> bindings)
label
- a label; this should be distinct for semantically distinct propositionsbindings
- a map of current bindings
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |