A B C D E F G H I J K L M N O P Q R S T U V W X _

U

UnaryAFAState - Class in rwth.i2.ltlrv.afastate.base

UnaryAFAState - Abstract superclass of all unary formulae.

UnaryAFAState(IFormula) - Constructor for class rwth.i2.ltlrv.afastate.base.UnaryAFAState

UnaryFormula - Class in rwth.i2.ltlrv.formula.base

BinaryFormula - Abstract superclass of all unary formulae.

UnaryFormula(IFormula) - Constructor for class rwth.i2.ltlrv.formula.base.UnaryFormula

UNBOUND - Static variable in interface rwth.i2.ltlrv.afastate.interfaze.IProposition

Constant meaning "unbound binding".

unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind, Set<String>) - Method in class rwth.i2.ltlrv.afastate.base.BinaryAFAState

Default implementation.

unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind, Set<String>) - Method in class rwth.i2.ltlrv.afastate.base.NullaryAFAState

unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind, Set<String>) - Method in class rwth.i2.ltlrv.afastate.base.UnaryAFAState

Default implementation.

unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind, Set<String>) - Method in class rwth.i2.ltlrv.afastate.impl.Next

Override cutting off the recursive search, since the Next operator builds the boundary between the current and the next joinpoints.

unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind, Set<String>) - Method in class rwth.i2.ltlrv.afastate.impl.Proposition

unboundVariablesAtCurrentJoinpoint(IAFAState.VariableKind, Set<String>) - Method in interface rwth.i2.ltlrv.afastate.interfaze.IAFAState

Until - Class in rwth.i2.ltlrv.afastate.impl

Until - Implements the Until operator in LTL.

Until(IFormula, IFormula) - Constructor for class rwth.i2.ltlrv.afastate.impl.Until

Constructs a new formula with the given subformulae.

Until(IFormula, IFormula) - Method in class rwth.i2.ltlrv.management.FormulaFactory

Generates an Until formula.

Until(IFormula, IFormula) - Method in interface rwth.i2.ltlrv.management.IFormulaFactory

Generates an Until formula.

updateContext(Set<String>) - Method in class rwth.i2.ltlrv.afastate.base.AbstractAFAState

Updates the context according to the current layer.

updateFormula(String, PropositionSet) - Method in class rwth.i2.ltlrv.management.VerificationRuntime

Requests that the formula with the given ID shall be updated.

useThreadLocal - Static variable in class org.aspectbench.runtime.internal.DecideThreadLocal