rwth.i2.ltlrv.afastate.impl
Class FF

java.lang.Object
  rwth.i2.ltlrv.formula.base.AbstractFormula
      rwth.i2.ltlrv.afastate.base.AbstractAFAState
          rwth.i2.ltlrv.afastate.base.NullaryAFAState
              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.

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

FF()

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

FF

public FF()

Method Detail

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)

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.

equals

public boolean equals(Object obj)

Overrides:

equals in class Object