rwth.i2.ltlrv.afastate.impl
Class Not

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

All Implemented Interfaces:

IAFAState, INot, IUnaryAFAState, IFormula, IUnaryTerm

public class Not
extends UnaryAFAState
implements INot

Not - Implements the Not operator. This holds the major implementation of bringing a formula into negation normal form.

Author:

Eric Bodden

See Also:

IFormula.negationNormalForm()

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

Not(IFormula subFormula)
A negated form of the subformula passed in.

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 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 t) Creates a formula with the same operator as this but a different subformula.
String	symbol() Returns the symbol for this term constructor.

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

equals, getSubformula, hashCode, requires, specializeBindings, toString, 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.IUnaryTerm

getSubformula

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

provides, requires, specializeBindings, transition, unboundVariablesAtCurrentJoinpoint, validate

Constructor Detail

Not

public Not(IFormula subFormula)

A negated form of the subformula passed in.

Parameters:

subFormula - the 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 negationNormalForm().

Specified by:

negationNormalForm in interface IFormula

Overrides:

negationNormalForm in class UnaryAFAState

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