rwth.i2.ltlrv.afastate.interfaze
Interface IAFAState

All Superinterfaces:

IFormula

All Known Subinterfaces:

IAnd, IBinaryAFAState, IFF, INext, INot, INullaryAFAState, IOr, IProposition, IRelease, ITT, IUnaryAFAState, IUntil

All Known Implementing Classes:

AbstractAFAState, And, BinaryAFAState, CommutativeBinaryAFAState, FF, Next, Not, NullaryAFAState, Or, Proposition, Release, TT, UnaryAFAState, Until

public interface IAFAState
extends IFormula

This interface reflects any subformula which is valid as input for AFA generation. Those are IUntil, IRelease, IAnd, IOr, INot, INext, ITT, IFF and IProposition subformulae. Such formulae can be obtained by invoking IFormula.negationNormalForm().
Attention: A lot of algorithms here assume that the whole term structure remains in negation normal form. So be careful when generating INot terms somewhere: Always invoke IFormula.negationNormalForm() on the newly created term! (@see rwth.i2.ltlrv.formula.impl.Implies#negationNormalForm())

Author:

Eric Bodden

See Also:

IUntil, IRelease, IAnd, IOr, INext, ITT, IFF, IProposition

Nested Class Summary

static class	IAFAState.ValidationException ValidationException - Exception that is thrown on validation of a formula.
static class	IAFAState.VariableKind

Method Summary

boolean	isFinalStateInAFA() Returns true if this formula represents a final state in the AFA.
void	provides(Set<String> result) This returns the set of provided variables at the current temporal levels.
void	providesNeg(Set<String> result) This returns the set of negatively provided variables at the current temporal levels.
void	providesPos(Set<String> result) This returns the set of positively provided variables at the current temporal levels.
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.
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.
void	unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result)
void	validate() Validates a formula for consistent bindings.

Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula

negationNormalForm, symbol

Method Detail

isFinalStateInAFA

boolean isFinalStateInAFA()

Returns true if this formula represents a final state in the AFA. This is the case if the formula is either a Release subformula, TT, or a boolean combination of subformulae evaluating to true.

Returns:

true if this formula represents a final state in the AFA

See Also:

IRelease, ITT

specializeBindings

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.

Parameters:

bindings - Set of propositions holding actual bindings.

Returns:

subformula with free bindings replaced by the bindings passed in

transition

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

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 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.

unboundVariablesAtCurrentJoinpoint

void unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind,
                                        Set<String> result)

provides

void provides(Set<String> result)

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

Parameters:

result - The result will be placed here.

See Also:

providesPos(Set), providesNeg(Set)

providesPos

void providesPos(Set<String> result)

This returns the set of positively provided variables at the current temporal levels. This function is defined as:

        providesPos( phi /\ psi ) = providesPos( phi ) join providesPos( psi )

        providesPos( phi \/ psi ) = providesPos( phi ) intersect providesPos( psi )

        providesPos( phi R psi ) =  providesPos( (psi /\ phi) \/ (psi /\ X(phi R psi)) )
                                 =  providesPos( psi )

        providesPos( phi U psi ) = providesPos( psi \/ (phi /\ X(phi U psi) )
                                 = providesPos( psi ) intersect providesPos( phi ) 

        providesPos( X phi )     = emptyset

        providesPos( !prop )     = emptyset

        providesPos( prop )      = provided variables of prop
     

Parameters:

result - The result will be placed here.

providesNeg

void providesNeg(Set<String> result)

This returns the set of negatively provided variables at the current temporal levels. This function is defined as:

        providesNeg( phi /\ psi ) = providesNeg( phi ) intersect providesNeg( psi )

        providesNeg( phi \/ psi ) = providesNeg( phi ) join providesNeg( psi )

        providesNeg( phi R psi ) =  providesNeg( psi ) intersect providesNeg( phi )

        providesNeg( phi U psi ) =  providesNeg( psi )

        providesNeg( X phi )     = emptyset

        providesNeg( !prop )     = provided variables of prop

        providesNeg( prop )      = emptyset
     

Parameters:

result - The result will be placed here.

requires

void requires(Set<String> result)

This returns the set of required variables. This is the set of all variables which are free in propositions, meaning they occur in an if-pointcut but are not provided by the same pointcut at the same time.

Parameters:

result - The result will be placed here.

validate

void validate()
              throws IAFAState.ValidationException

Validates a formula for consistent bindings. Bindings are consistent, when at each point in time, the set of povided variables can be guaranteed to be a superset of the set of required variables.

Throws:

IAFAState.ValidationException - Thrown if a variable is unbound.

See Also:

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