rwth.i2.ltlrv.afastate.impl
Class Next

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.afastate.base.AbstractAFAState
          rwth.i2.ltlrv.afastate.base.UnaryAFAState
              rwth.i2.ltlrv.afastate.impl.Next

All Implemented Interfaces:

IAFAState, INext, IUnaryAFAState, IFormula, IUnaryTerm

public class Next
extends UnaryAFAState
implements INext

Next - Implements the Next formula constructor of LTL.

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.afastate.base.UnaryAFAState

subformula

Fields inherited from class rwth.i2.ltlrv.formula.base.AbstractFormula

factory

Constructor Summary

Next(IFormula subFormula)
Constructs a new formula with the given subformula.

Method Summary

void	doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
private WeakValuesMap<String,Object>	filterBinding(Set<String> context, WeakValuesMap<String,Object> binding) Filters bindings for those which are contained in the given context.
boolean	isFinalStateInAFA() Returns true if this formula represents a final state in the AFA.
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.
IAFAState	reconstruct(IFormula t) Creates a formula with the same operator as this but a different subformula.
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.
String	symbol() Returns the symbol for this term constructor.
void	unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result) Override cutting off the recursive search, since the Next operator builds the boundary between the current and the next joinpoints.

Methods inherited from class rwth.i2.ltlrv.afastate.base.UnaryAFAState

equals, getSubformula, hashCode, negationNormalForm, specializeBindings, toString, validate

Methods inherited from class rwth.i2.ltlrv.afastate.base.AbstractAFAState

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.formula.interfaze.IUnaryTerm

getSubformula

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

negationNormalForm

Methods inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState

provides, specializeBindings, transition, validate

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

negationNormalForm

Constructor Detail

Next

public Next(IFormula subFormula)

Constructs a new formula with the given subformula.

Parameters:

subFormula - the subformula

Method Detail

isFinalStateInAFA

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

Specified by:

isFinalStateInAFA in interface IAFAState

Returns:

true if this formula represents a final state in the AFA

See Also:

IRelease, ITT

doTransition

public void doTransition(Set<String> context,
                         PropositionSet currentProps,
                         WeakValuesMap<String,Object> currentBinding,
                         Set<Set<IAFAState>> result)

Performs the actual transition based on the current context.

Specified by:

doTransition in class AbstractAFAState

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), AbstractAFAState.transition(Set, PropositionSet, WeakValuesMap, Set), AbstractAFAState.updateContext(Set)

filterBinding

private WeakValuesMap<String,Object> filterBinding(Set<String> context,
                                                   WeakValuesMap<String,Object> binding)

Filters bindings for those which are contained in the given context.

Parameters:

context - the current context

binding - the original binding

Returns:

the filtered binding

unboundVariablesAtCurrentJoinpoint

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

Override cutting off the recursive search, since the Next operator builds the boundary between the current and the next joinpoints.

Specified by:

unboundVariablesAtCurrentJoinpoint in interface IAFAState

Overrides:

unboundVariablesAtCurrentJoinpoint in class UnaryAFAState

Parameters:

variableKind - TODO

See Also:

IAFAState.unboundVariablesAtCurrentJoinpoint(VariableKind, Set)

providesPos

public 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
     

Specified by:

providesPos in interface IAFAState

Parameters:

result - The result will be placed here.

providesNeg

public 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
     

Specified by:

providesNeg in interface IAFAState

Parameters:

result - The result will be placed here.

requires

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

Specified by:

requires in interface IAFAState

Overrides:

requires in class UnaryAFAState

Parameters:

result - The result will be placed here.

reconstruct

public IAFAState reconstruct(IFormula t)

Creates a formula with the same operator as this but a different subformula. This is used for recursion with nondestructive updates.

Specified by:

reconstruct in interface IUnaryAFAState

Parameters:

t - the new subformula

Returns:

the new instance

symbol

public String symbol()

Returns the symbol for this term constructor. Propositions should return their label. All symbols, including those for nullary term constructors should be distinct.

Specified by:

symbol in interface IFormula

Returns:

The symbol for this term constructor.