rwth.i2.ltlrv.afastate.impl
Class Release

java.lang.Object
  extended by rwth.i2.ltlrv.formula.base.AbstractFormula
      extended by rwth.i2.ltlrv.afastate.base.AbstractAFAState
          extended by rwth.i2.ltlrv.afastate.base.BinaryAFAState
              extended by rwth.i2.ltlrv.afastate.impl.Release
All Implemented Interfaces:
IAFAState, IBinaryAFAState, IRelease, IBinaryTerm, IFormula

public class Release
extends BinaryAFAState
implements IRelease

Release - Implements the Release operator in LTL. Release and Until 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:
Until

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
Release(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

Release

public Release(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