Class AbstractAFAState

  extended by rwth.i2.ltlrv.formula.base.AbstractFormula
      extended by rwth.i2.ltlrv.afastate.base.AbstractAFAState
All Implemented Interfaces:
IAFAState, IFormula
Direct Known Subclasses:
BinaryAFAState, NullaryAFAState, UnaryAFAState

public abstract class AbstractAFAState
extends AbstractFormula
implements IAFAState

Abstract superclass of all formulae. For ease of use only.

Eric Bodden

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
Constructor Summary
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)
Performs a transition on this term under the given propositions and bindings. The result is returned in the 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 A typicall initial call would be:
       Set<Set<IAFAState>> result = new HashSet<Set<IAFAState>>();
       transition(new HastSet<String>(), props, binding, result);

Specified by:
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)
Updates the context according to the current layer. This means it adds all variables provided by the current layer to the context.

context - the context of the last (earlier) temporal layer
context join provides(this)
See Also:


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.

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)
See Also:
IAFAState.transition(Set, PropositionSet, WeakValuesMap, Set), transition(Set, PropositionSet, WeakValuesMap, Set), updateContext(Set)


public void provides(Set<String> context)
This returns the set of provided variables at the current temporal levels. At each state s it holds, that provides(s) = providesPos(s) join providesNeg(s).

Specified by:
provides in interface IAFAState
context - The result will be placed here.
See Also:
IAFAState.providesPos(Set), IAFAState.providesNeg(Set)


public void validate()
              throws IAFAState.ValidationException
Implementation of IAFAState.validate(). This creates an empty context and then recurses further using validate(Set).

Specified by:
validate in interface IAFAState
ValidationException - @inheritDoc
See Also:
IAFAState.provides(Set), IAFAState.requires(Set), IAFAState.ValidationException.IAFAState.ValidationException(String, IAFAState)


public abstract void validate(Set<String> context)
                       throws IAFAState.ValidationException
To be implemented by actual formulae as described in IAFAState.validate().

context - Here the context is passed in from the outer (earlier) temporal layers.
ValidationException - @see #validate()