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
FF
public FF()
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