Class FF

  extended by rwth.i2.ltlrv.formula.base.AbstractFormula
      extended by rwth.i2.ltlrv.afastate.base.AbstractAFAState
          extended by rwth.i2.ltlrv.afastate.base.NullaryAFAState
              extended by rwth.i2.ltlrv.afastate.impl.FF
All Implemented Interfaces:
IAFAState, IFF, INullaryAFAState, IFormula

public class FF
extends NullaryAFAState
implements IFF

FF - Implements the sink state / formula representing false.

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
Constructor Summary
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 equals(Object obj)
 boolean isFinalStateInAFA()
          Returns true if this formula represents a final state in the AFA.
 String symbol()
          Returns the symbol for this term constructor.
Methods inherited from class rwth.i2.ltlrv.afastate.base.NullaryAFAState
getInstance, hashCode, negationNormalForm, providesNeg, providesPos, 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.afastate.interfaze.IAFAState
provides, providesNeg, providesPos, requires, specializeBindings, transition, unboundVariablesAtCurrentJoinpoint, validate

Constructor Detail


public FF()
Method Detail


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
true if this formula represents a final state in the AFA
See Also:
IRelease, ITT


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


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
The symbol for this term constructor.


public boolean equals(Object obj)

equals in class Object