Uses of Interface
rwth.i2.ltlrv.afastate.interfaze.IAFAState

Packages that use IAFAState

rwth.i2.ltlrv.afastate.base	Abstract base classes for all AFA states.
rwth.i2.ltlrv.afastate.impl	Implementing classes of AFA states.
rwth.i2.ltlrv.afastate.interfaze	Common interfaces for all AFA states.
rwth.i2.ltlrv.formula.impl	Implementing classes for LTL term constructors.
rwth.i2.ltlrv.formula.interfaze	Common interfaces for LTL term constructors.
rwth.i2.ltlrv.management	Holds classes for configuration management and formula creation.
rwth.i2.ltlrv.util	Holds utility classes.

Uses of IAFAState in rwth.i2.ltlrv.afastate.base

Classes in rwth.i2.ltlrv.afastate.base that implement IAFAState

class	AbstractAFAState Abstract superclass of all formulae.
class	BinaryAFAState BinaryAFAState - Abstract superclass of all binary formulae.
class	CommutativeBinaryAFAState Represents a binary formula, which is commutative.
class	NullaryAFAState NullaryAFAState - Abstract base class of all nullary AFA states.
class	UnaryAFAState UnaryAFAState - Abstract superclass of all unary formulae.

Fields in rwth.i2.ltlrv.afastate.base declared as IAFAState

protected IAFAState	BinaryAFAState.substate1
protected IAFAState	BinaryAFAState.substate2

Methods in rwth.i2.ltlrv.afastate.base that return IAFAState

IAFAState	UnaryAFAState.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
IAFAState	NullaryAFAState.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
IAFAState	BinaryAFAState.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
IAFAState	UnaryAFAState.specializeBindings(WeakValuesMap<String,Object> bindings) Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument.
IAFAState	NullaryAFAState.specializeBindings(WeakValuesMap<String,Object> bindings) Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument.
IAFAState	BinaryAFAState.specializeBindings(WeakValuesMap<String,Object> bindings) Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument.

Method parameters in rwth.i2.ltlrv.afastate.base with type arguments of type IAFAState

protected abstract void	AbstractAFAState.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	AbstractAFAState.transition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs a transition on this term under the given propositions and bindings.

Uses of IAFAState in rwth.i2.ltlrv.afastate.impl

Classes in rwth.i2.ltlrv.afastate.impl that implement IAFAState

class	And And - Implements a conjunct.
class	FF FF - Implements the sink state / formula representing false.
class	Next Next - Implements the Next formula constructor of LTL.
class	Not Not - Implements the Not operator.
class	Or Or - Implements a disjunct.
class	Proposition Proposition - Implements a proposition.
class	Release Release - Implements the Release operator in LTL.
class	TT TT - Implements the sink state / formula representing true.
class	Until Until - Implements the Until operator in LTL.

Methods in rwth.i2.ltlrv.afastate.impl that return IAFAState

IAFAState	Until.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions. This form also holds only IUntil, IRelease, IAnd, IOr, INot, IProposition subformulae. This must return a copy of the original formula. The major work is done in Not.negationNormalForm().
IAFAState	Release.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions. This form also holds only IUntil, IRelease, IAnd, IOr, INot, IProposition subformulae. This must return a copy of the original formula. The major work is done in Not.negationNormalForm().
IAFAState	Not.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions. This form also holds only IUntil, IRelease, IAnd, IOr, INot, IProposition subformulae. This must return a copy of the original formula. The major work is done in Not.negationNormalForm().
IAFAState	Not.reconstruct(IFormula t) Creates a formula with the same operator as this but a different subformula.
IAFAState	Next.reconstruct(IFormula t) Creates a formula with the same operator as this but a different subformula.
IAFAState	Until.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.
IAFAState	Release.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.
IAFAState	Or.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.
IAFAState	And.reconstruct(IFormula t1, IFormula t2) Creates a formula with the same operator as this but different subformulae.

Method parameters in rwth.i2.ltlrv.afastate.impl with type arguments of type IAFAState

void	Until.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	TT.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	Release.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	Proposition.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	Or.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	Not.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	Next.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	FF.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.
void	And.doTransition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs the actual transition based on the current context.

Uses of IAFAState in rwth.i2.ltlrv.afastate.interfaze

Subinterfaces of IAFAState in rwth.i2.ltlrv.afastate.interfaze

interface	IAnd IAnd represents a conjunct.
interface	IBinaryAFAState IBinaryAFAState - Common interface for all binary AFA states.
interface	IFF IFF represents FF = false
interface	INext INext represents the Next operator
interface	INot INot represents the negation operator
interface	INullaryAFAState INullaryAFAState - Common interface for nullary AFA states.
interface	IOr IOr represents a disjunct
interface	IProposition IProposition represents a proposition
interface	IRelease IRelease - Interface representing the binary Release operator in LTL.
interface	ITT ITT represents TT = true
interface	IUnaryAFAState IUnaryAFAState - Common interface for unary AFA states.
interface	IUntil IUntil - Interface representing the binary Until operator in LTL.

Methods in rwth.i2.ltlrv.afastate.interfaze that return IAFAState

IAFAState	IUnaryAFAState.reconstruct(IFormula subformula) Creates a formula with the same operator as this but a different subformula.
IAFAState	IBinaryAFAState.reconstruct(IFormula subformula1, IFormula subformula2) Creates a formula with the same operator as this but different subformulae.
IAFAState	IAFAState.specializeBindings(WeakValuesMap<String,Object> bindings) Returns a fresh copy of this subformula with bindings in propositions specialized by the bindings of propositions, which are passed in as argument.

Method parameters in rwth.i2.ltlrv.afastate.interfaze with type arguments of type IAFAState

void	IAFAState.transition(Set<String> context, PropositionSet currentProps, WeakValuesMap<String,Object> currentBinding, Set<Set<IAFAState>> result) Performs a transition on this term under the given propositions and bindings.

Constructors in rwth.i2.ltlrv.afastate.interfaze with parameters of type IAFAState

IAFAState.ValidationException(String variableName, IAFAState subformula)

Uses of IAFAState in rwth.i2.ltlrv.formula.impl

Methods in rwth.i2.ltlrv.formula.impl that return IAFAState

IAFAState	Implies.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
IAFAState	Globally.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
IAFAState	Finally.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.
IAFAState	Equivalent.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.

Uses of IAFAState in rwth.i2.ltlrv.formula.interfaze

Methods in rwth.i2.ltlrv.formula.interfaze that return IAFAState

IAFAState

IFormula.negationNormalForm() Produces a formula in negation normal form, where negations occur only in front of propositions.

Uses of IAFAState in rwth.i2.ltlrv.management

Fields in rwth.i2.ltlrv.management with type parameters of type IAFAState

private Set<Set<IAFAState>>	Configuration.globalState The current global state as a disjunct of conjuncts of terms.
private static Map<IAFAState,Integer>	Configuration.termToNumber Maps a term to a number.

Methods in rwth.i2.ltlrv.management that return types with arguments of type IAFAState

private static Set<Set<IAFAState>>	Configuration.subsumptionReduction(Set<Set<IAFAState>> set) Removes sets which contain another set (in order to find the smallest model)
private static Set<Set<IAFAState>>	Configuration.transition(Set<Set<IAFAState>> globalState, PropositionSet currentProps) Performs a transition from the given state (set of clauses) to the sucessor state for the given set of propositions.

Methods in rwth.i2.ltlrv.management with parameters of type IAFAState

private static int	Configuration.numberOf(IAFAState term) Returns a (possibly new) number for a term, based on equality.
private static String	Configuration.numberStringOf(IAFAState term) Returns a unique number string for the term, based on equality.

Method parameters in rwth.i2.ltlrv.management with type arguments of type IAFAState

private static String	Configuration.clauseSetToString(Set<Set<IAFAState>> clauseSet)
private static boolean	Configuration.isClauseSetFinal(Set<Set<IAFAState>> clauseSet)
private static Set<Set<IAFAState>>	Configuration.subsumptionReduction(Set<Set<IAFAState>> set) Removes sets which contain another set (in order to find the smallest model)
private static Set<Set<IAFAState>>	Configuration.transition(Set<Set<IAFAState>> globalState, PropositionSet currentProps) Performs a transition from the given state (set of clauses) to the sucessor state for the given set of propositions.

Constructors in rwth.i2.ltlrv.management with parameters of type IAFAState

Configuration(IAFAState initialState)
Constructs a new configuration for an initial state.

Uses of IAFAState in rwth.i2.ltlrv.util

Methods in rwth.i2.ltlrv.util that return types with arguments of type IAFAState

static Set<IAFAState>	SetUtils.clauseTT() Constructs an empty clause which represents TT (true).
static Set<Set<IAFAState>>	SetUtils.emptyClauseSet() Constructs an empty clause set.
static Set<Set<IAFAState>>	SetUtils.FF() Constructs an empty clause set, representing FF.
static Set<Set<IAFAState>>	SetUtils.singletonClauseSet(IAFAState... elements) Constructs a set holding one single clause holding the given terms.
static Set<IAFAState>	SetUtils.termClause(IAFAState... elements) Constructs a term clause/set for the given elements.
static Set<Set<IAFAState>>	SetUtils.TT() Constructs an empty clause set, which represents TT (true).

Methods in rwth.i2.ltlrv.util with parameters of type IAFAState

static Set<Set<IAFAState>>	SetUtils.singletonClauseSet(IAFAState... elements) Constructs a set holding one single clause holding the given terms.
static Set<IAFAState>	SetUtils.termClause(IAFAState... elements) Constructs a term clause/set for the given elements.