|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
public interface IBinaryAFAState
IBinaryAFAState - Common interface for all binary AFA states.
Nested Class Summary |
---|
Nested classes/interfaces inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState |
---|
IAFAState.ValidationException, IAFAState.VariableKind |
Method Summary | |
---|---|
IAFAState |
reconstruct(IFormula subformula1,
IFormula subformula2)
Creates a formula with the same operator as this |
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IBinaryTerm |
---|
getSubformula1, getSubformula2 |
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula |
---|
negationNormalForm, symbol |
Methods inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState |
---|
isFinalStateInAFA, provides, providesNeg, providesPos, requires, specializeBindings, transition, unboundVariablesAtCurrentJoinpoint, validate |
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula |
---|
negationNormalForm, symbol |
Method Detail |
---|
IAFAState reconstruct(IFormula subformula1, IFormula subformula2)
this
but different subformulae. This is used for recursion with
nondestructive updates.
- Parameters:
subformula1
- left subformulasubformula2
- right subformula
- Returns:
- the new instance
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |