rwth.i2.ltlrv.afastate.base
Class AbstractAFAState

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      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.

Author:

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

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

AbstractAFAState

public AbstractAFAState()

Method Detail

transition

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 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);
       

Specified by:

transition in interface IAFAState

Parameters:

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.

updateContext

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.

Parameters:

context - the context of the last (earlier) temporal layer

Returns:

context join provides(this)

See Also:

IAFAState.provides(Set)

doTransition

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.

Parameters:

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)

provides

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

Parameters:

context - The result will be placed here.

See Also:

IAFAState.providesPos(Set), IAFAState.providesNeg(Set)

validate

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

Throws:

ValidationException - @inheritDoc

IAFAState.ValidationException

See Also:

IAFAState.provides(Set), IAFAState.requires(Set), IAFAState.ValidationException.IAFAState.ValidationException(String, IAFAState)

validate

public abstract void validate(Set<String> context)
                       throws IAFAState.ValidationException

To be implemented by actual formulae as described in IAFAState.validate().

Parameters:

context - Here the context is passed in from the outer (earlier) temporal layers.

Throws:

ValidationException - @see #validate()

IAFAState.ValidationException