rwth.i2.ltlrv.afastate.interfaze
Interface IUntil

All Superinterfaces:

IAFAState, IBinaryTerm, IFormula

All Known Implementing Classes:

Until

public interface IUntil
extends IBinaryTerm, IAFAState

IUntil - Interface representing the binary Until operator in LTL.

Author:

Eric Bodden

Nested Class Summary

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

IAFAState.ValidationException, IAFAState.VariableKind

Method Summary

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