rwth.i2.ltlrv.afastate.impl
Class Until

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.afastate.base.AbstractAFAState
          rwth.i2.ltlrv.afastate.base.BinaryAFAState
              rwth.i2.ltlrv.afastate.impl.Until

All Implemented Interfaces:

IAFAState, IBinaryAFAState, IUntil, IBinaryTerm, IFormula

public class Until
extends BinaryAFAState
implements IUntil

Until - Implements the Until operator in LTL. Until and Release subformulae are the essence of an AFA representation of a LTL formula. They represent the actual states of an AFA.s

Author:

Eric Bodden

See Also:

Release

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

subformula1, subformula2, substate1, substate2

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

factory

Constructor Summary

Until(IFormula subFormula1, IFormula subFormula2)
Constructs a new formula with the given subformulae.

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.
boolean	isFinalStateInAFA() Returns true if this formula represents a final state in the AFA.
IAFAState	negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions. This form also holds only IUntil, IRelease, IAnd, IOr, INot, IProposition subformulae. This must return a copy of the original formula. The major work is done in Not.negationNormalForm().
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 t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.
String	symbol() Returns the symbol for this term constructor.
String	toString()

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

equals, getSubformula1, getSubformula2, hashCode, requires, specializeBindings, unboundVariablesAtCurrentJoinpoint, 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.IBinaryTerm

getSubformula1, getSubformula2

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

provides, requires, specializeBindings, transition, unboundVariablesAtCurrentJoinpoint, validate

Constructor Detail

Until

public Until(IFormula subFormula1,
             IFormula subFormula2)

Constructs a new formula with the given subformulae.

Parameters:

subFormula1 - left subformula

subFormula2 - right subformula

Method Detail

negationNormalForm

public IAFAState negationNormalForm()

Produces a formula in negation normal form, where negations occur only in front of propositions. This form also holds only IUntil, IRelease, IAnd, IOr, INot, IProposition subformulae. This must return a copy of the original formula. The major work is done in Not.negationNormalForm().

Specified by:

negationNormalForm in interface IFormula

Overrides:

negationNormalForm in class BinaryAFAState

Returns:

the formula in negation normal form

See Also:

IUntil, IRelease, IAnd, IOr, IProposition

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)

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.

reconstruct

public IAFAState reconstruct(IFormula t1,
                             IFormula t2)

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

Specified by:

reconstruct in interface IBinaryAFAState

Parameters:

t1 - left subformula

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

toString

public String toString()

Overrides:

toString in class BinaryAFAState