rwth.i2.ltlrv.afastate.interfaze
Interface IBinaryAFAState

All Superinterfaces:

IAFAState, IBinaryTerm, IFormula

All Known Implementing Classes:

And, BinaryAFAState, CommutativeBinaryAFAState, Or, Release, Until

public interface IBinaryAFAState
extends IBinaryTerm, IAFAState

IBinaryAFAState - Common interface for all binary AFA states.

Author:

Eric Bodden

Nested Class Summary

Nested classes/interfaces inherited from interface rwth.i2.ltlrv.afastate.interfaze.IAFAState

IAFAState.ValidationException, IAFAState.VariableKind

Method Summary

IAFAState

reconstruct(IFormula subformula1, IFormula subformula2) Creates a formula with the same operator as this but different subformulae.

Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IBinaryTerm

getSubformula1, getSubformula2

Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula

negationNormalForm, symbol

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

isFinalStateInAFA, provides, providesNeg, providesPos, requires, specializeBindings, transition, unboundVariablesAtCurrentJoinpoint, validate

Methods inherited from interface rwth.i2.ltlrv.formula.interfaze.IFormula

negationNormalForm, symbol

Method Detail

reconstruct

IAFAState reconstruct(IFormula subformula1,
                      IFormula subformula2)

Creates a formula with the same operator as this but different subformulae. This is used for recursion with nondestructive updates.

Parameters:

subformula1 - left subformula

subformula2 - right subformula

Returns:

the new instance