|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object rwth.i2.ltlrv.formula.base.AbstractFormula rwth.i2.ltlrv.afastate.base.AbstractAFAState
public abstract class AbstractAFAState
Abstract superclass of all formulae. For ease of use only.
Nested Class Summary |
---|
Nested classes/interfaces inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState |
---|
IAFAState.ValidationException, IAFAState.VariableKind |
Field Summary |
---|
Fields inherited from class rwth.i2.ltlrv.formula.base.AbstractFormula |
---|
factory |
Constructor Summary | |
---|---|
AbstractAFAState()
|
Method Summary | |
---|---|
protected abstract void |
doTransition(Set<String> context,
PropositionSet currentProps,
WeakValuesMap<String,Object> currentBinding,
Set<Set<IAFAState>> result)
Performs the actual transition based on the current context. |
void |
provides(Set<String> context)
This returns the set of provided variables at the current temporal levels. |
void |
transition(Set<String> context,
PropositionSet currentProps,
WeakValuesMap<String,Object> currentBinding,
Set<Set<IAFAState>> result)
Performs a transition on this term under the given propositions and bindings. |
protected Set<String> |
updateContext(Set<String> context)
Updates the context according to the current layer. |
void |
validate()
Implementation of IAFAState.validate() . |
abstract void |
validate(Set<String> context)
To be implemented by actual formulae as described in IAFAState.validate() . |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Methods inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState |
---|
isFinalStateInAFA, providesNeg, providesPos, requires, specializeBindings, unboundVariablesAtCurrentJoinpoint |
Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula |
---|
negationNormalForm, symbol |
Constructor Detail |
---|
public AbstractAFAState()
Method Detail |
---|
public void transition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result)
result
variable and is actually a set of clauses
representing a disjunct of a conjunct of states. This may not yet be the minimal model. It can be
reduced by applying subsumption reduction (@see rwth.i2.ltlrv.management.Configuration#subsumptionReduction(Set)).
A typicall initial call would be:
Set<Set<IAFAState>> result = new HashSet<Set<IAFAState>>();
transition(new HastSet<String>(), props, binding, result);
transition
in interface IAFAState
context
- The context holds the set of variables that are provided by the outer (previous) temporal layers.
Initially this is empty. Then it has to be updated on each layer by adding the variables which
IAFAState.provides(Set)
returns. It is only used by the INext
operator
(@see Next#doTransition(Set, PropositionSet, WeakValuesMap, Set)).currentProps
- The set of propositions that are currently active.
Those must hold all bindings they provide.currentBinding
- The current binding to evaluate under. (@see PropositionSet#validCombinationsOfBindings())result
- The result will be placed here.protected Set<String> updateContext(Set<String> context)
context
- the context of the last (earlier) temporal layer
context
join provides(this)
IAFAState.provides(Set)
protected abstract void doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result)
context
- @see #transition(Set, PropositionSet, WeakValuesMap, Set)currentProps
- @see #transition(Set, PropositionSet, WeakValuesMap, Set)currentBinding
- @see #transition(Set, PropositionSet, WeakValuesMap, Set)result
- @see #transition(Set, PropositionSet, WeakValuesMap, Set)IAFAState.transition(Set, PropositionSet, WeakValuesMap, Set)
,
transition(Set, PropositionSet, WeakValuesMap, Set)
,
updateContext(Set)
public void provides(Set<String> context)
provides
in interface IAFAState
context
- The result will be placed here.IAFAState.providesPos(Set)
,
IAFAState.providesNeg(Set)
public void validate() throws IAFAState.ValidationException
IAFAState.validate()
. This creates an empty context and then
recurses further using validate(Set)
.
validate
in interface IAFAState
ValidationException
- @inheritDoc
IAFAState.ValidationException
IAFAState.provides(Set)
,
IAFAState.requires(Set)
,
IAFAState.ValidationException.IAFAState.ValidationException(String, IAFAState)
public abstract void validate(Set<String> context) throws IAFAState.ValidationException
IAFAState.validate()
.
context
- Here the context is passed in from the outer (earlier) temporal layers.
ValidationException
- @see #validate()
IAFAState.ValidationException
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |