rwth.i2.ltlrv.afastate.base
Class NullaryAFAState

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.afastate.base.AbstractAFAState
          rwth.i2.ltlrv.afastate.base.NullaryAFAState

All Implemented Interfaces:

IAFAState, INullaryAFAState, IFormula

Direct Known Subclasses:

FF, Proposition, TT

public abstract class NullaryAFAState
extends AbstractAFAState
implements INullaryAFAState

NullaryAFAState - Abstract base class of all nullary AFA states.

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

NullaryAFAState()

Method Summary

INullaryAFAState	getInstance()
int	hashCode()
IAFAState	negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
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.
String	toString()
void	unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind variableKind, Set<String> result)
void	validate(Set<String> context) To be implemented by actual formulae as described in IAFAState.validate().

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

doTransition, provides, transition, updateContext, validate

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, notify, notifyAll, wait, wait, wait

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

isFinalStateInAFA, provides, transition, validate

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

symbol

Constructor Detail

NullaryAFAState

public NullaryAFAState()

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

Returns:

the formula in negation normal form

See Also:

IUntil, IRelease, IAnd, IOr, IProposition

unboundVariablesAtCurrentJoinpoint

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

Specified by:

unboundVariablesAtCurrentJoinpoint in interface IAFAState

specializeBindings

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

Specified by:

specializeBindings in interface IAFAState

Parameters:

bindings - Set of propositions holding actual bindings.

Returns:

subformula with free bindings replaced by the bindings passed in

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

Parameters:

result - The result will be placed here.

validate

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

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

Specified by:

validate in class AbstractAFAState

Parameters:

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

Throws:

IAFAState.ValidationException

getInstance

public INullaryAFAState getInstance()

Specified by:

getInstance in interface INullaryAFAState

Returns:

The usually unique instance of this kind.

toString

public String toString()

Overrides:

toString in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object