rwth.i2.ltlrv.afastate.impl
Class Or
java.lang.Object
rwth.i2.ltlrv.formula.base.AbstractFormula
rwth.i2.ltlrv.afastate.base.AbstractAFAState
rwth.i2.ltlrv.afastate.base.BinaryAFAState
rwth.i2.ltlrv.afastate.base.CommutativeBinaryAFAState
rwth.i2.ltlrv.afastate.impl.Or
- All Implemented Interfaces:
- IAFAState, IBinaryAFAState, IOr, IBinaryTerm, IFormula
public class Or
- extends CommutativeBinaryAFAState
- implements IOr
Or - Implements a disjunct.
- Author:
- Eric Bodden
Constructor Summary |
Or(IFormula subFormula1,
IFormula subFormula2)
A disjunct of the two subformulae. |
Or
public Or(IFormula subFormula1,
IFormula subFormula2)
- A disjunct of the two subformulae.
- Parameters:
subFormula1
- left subformulasubFormula2
- right subformula
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 t1,
IFormula t2)
- Creates a formula with the same operator as
this
but different subformulae. This is used for recursion with
nondestructive updates.
- Specified by:
reconstruct
in interface IBinaryAFAState
- Parameters:
t1
- left subformulat2
- right 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.