rwth.i2.ltlrv.afastate.interfaze
Interface IUnaryAFAState

All Superinterfaces:

IAFAState, IFormula, IUnaryTerm

All Known Implementing Classes:

Next, Not, UnaryAFAState

public interface IUnaryAFAState
extends IUnaryTerm, IAFAState

IUnaryAFAState - Common interface for unary 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 subformula) Creates a formula with the same operator as this but a different subformula.

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

getSubformula

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

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

Parameters:

subformula - the new subformula

Returns:

the new instance