|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectrwth.i2.ltlrv.formula.base.AbstractFormula
rwth.i2.ltlrv.afastate.base.AbstractAFAState
rwth.i2.ltlrv.afastate.base.BinaryAFAState
public abstract class BinaryAFAState
BinaryAFAState - Abstract superclass of all binary formulae.
Nested Class Summary |
---|
Nested classes/interfaces inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState |
---|
IAFAState.ValidationException, IAFAState.VariableKind |
Field Summary | |
---|---|
protected IFormula |
subformula1
the subformulae |
protected IFormula |
subformula2
the subformulae |
protected IAFAState |
substate1
|
protected IAFAState |
substate2
|
Fields inherited from class rwth.i2.ltlrv.formula.base.AbstractFormula |
---|
factory |
Constructor Summary | |
---|---|
BinaryAFAState(IFormula subformula1,
IFormula subformula2)
|
Method Summary | |
---|---|
boolean |
equals(Object oth)
|
IFormula |
getSubformula1()
|
IFormula |
getSubformula2()
|
int |
hashCode()
|
IAFAState |
negationNormalForm()
Produces a formula in negation normal form, where negations occur only in front of propositions. |
void |
requires(Set<String> result)
This returns the set of required variables. |
IAFAState |
specializeBindings(WeakValuesMap<String,Object> bindings)
Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument. |
String |
toString()
|
void |
unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind,
Set<String> result)
Default implementation. |
void |
validate(Set<String> context)
To be implemented by actual formulae as described in IAFAState.validate() . |
Methods inherited from class rwth.i2.ltlrv.afastate.base.AbstractAFAState |
---|
doTransition, provides, transition, updateContext, validate |
Methods inherited from class java.lang.Object |
---|
clone, finalize, getClass, notify, notifyAll, wait, wait, wait |
Methods inherited from interface rwth.i2.ltlrv.afastate.interfaze.IBinaryAFAState |
---|
reconstruct |
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula |
---|
symbol |
Methods inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState |
---|
isFinalStateInAFA, provides, providesNeg, providesPos, transition, validate |
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula |
---|
symbol |
Field Detail |
---|
protected IFormula subformula1
protected IFormula subformula2
protected IAFAState substate1
protected IAFAState substate2
Constructor Detail |
---|
public BinaryAFAState(IFormula subformula1, IFormula subformula2)
subformula1
- left subformulasubformula2
- right subformulaMethod Detail |
---|
public IFormula getSubformula1()
getSubformula1
in interface IBinaryTerm
public IFormula getSubformula2()
getSubformula2
in interface IBinaryTerm
public boolean equals(Object oth)
equals
in class Object
public int hashCode()
hashCode
in class Object
public String toString()
toString
in class Object
public void unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result)
unboundVariablesAtCurrentJoinpoint
in interface IAFAState
variableKind
- TODOIAFAState.unboundVariablesAtCurrentJoinpoint(VariableKind, Set)
public void requires(Set<String> result)
requires
in interface IAFAState
result
- The result will be placed here.public void validate(Set<String> context) throws IAFAState.ValidationException
IAFAState.validate()
.
validate
in class AbstractAFAState
context
- Here the context is passed in from the outer (earlier) temporal layers.
IAFAState.ValidationException
public IAFAState negationNormalForm()
Not.negationNormalForm()
.
negationNormalForm
in interface IFormula
IUntil
,
IRelease
,
IAnd
,
IOr
,
IProposition
public IAFAState specializeBindings(WeakValuesMap<String,Object> bindings)
specializeBindings
in interface IAFAState
bindings
- Set of propositions holding actual bindings.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |