[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Research / RV / Ltl2ba4j / Docs / Api / Index-all
Printer-friendly
Index (LTL2BA4J)
A B D E F G H I L M N O P R S T U X

A

And(IFormula, IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
And - Class in rwth.i2.ltl2ba4j.formula.impl
 
And(IFormula, IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.And
 
And(IFormula, IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
automatonToDot(Collection<ITransition>) - Static method in class rwth.i2.ltl2ba4j.DottyWriter
 

B

BAJni - Class in rwth.i2.ltl2ba4j.internal.jnibridge
 
BAJni(IFormula) - Constructor for class rwth.i2.ltl2ba4j.internal.jnibridge.BAJni
Constructs a new automaton for the given formula.
BAJni(String) - Constructor for class rwth.i2.ltl2ba4j.internal.jnibridge.BAJni
Constructs a new automaton for the given formula.

D

DottyWriter - Class in rwth.i2.ltl2ba4j
 
DottyWriter() - Constructor for class rwth.i2.ltl2ba4j.DottyWriter
 

E

Eq(IFormula, IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
Eq(IFormula, IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
equals(Object) - Method in class rwth.i2.ltl2ba4j.formula.impl.Proposition
Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
equals(Object) - Method in interface rwth.i2.ltl2ba4j.formula.IProposition
Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
equals(Object) - Method in interface rwth.i2.ltl2ba4j.model.IGraphProposition
Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
equals(Object) - Method in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
equals(Object) - Method in class rwth.i2.ltl2ba4j.model.impl.State
Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
equals(Object) - Method in class rwth.i2.ltl2ba4j.model.impl.Transition
/** Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
equals(Object) - Method in interface rwth.i2.ltl2ba4j.model.IState
Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
equals(Object) - Method in interface rwth.i2.ltl2ba4j.model.ITransition
/** Clients should implement this method, since the implementation uses HashSets, which require a proper notion of equality.
Equivalent - Class in rwth.i2.ltl2ba4j.formula.impl
 
Equivalent(IFormula, IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Equivalent
 

F

F(IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
F(IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
Finally - Class in rwth.i2.ltl2ba4j.formula.impl
 
Finally(IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Finally
 
FormulaFactory - Class in rwth.i2.ltl2ba4j.formula.impl
 
FormulaFactory() - Constructor for class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
 
formulaToBA(IFormula) - Static method in class rwth.i2.ltl2ba4j.LTL2BA4J
Converts the given formula into a finite state machine.
formulaToBA(String) - Static method in class rwth.i2.ltl2ba4j.LTL2BA4J
Converts the given formula into a finite state machine.

G

G(IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
G(IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
getFullLabel() - Method in interface rwth.i2.ltl2ba4j.model.IGraphProposition
 
getFullLabel() - Method in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
getGraphFactory() - Static method in class rwth.i2.ltl2ba4j.LTL2BA4J
 
getLabel() - Method in class rwth.i2.ltl2ba4j.formula.impl.Proposition
getLabel() - Method in interface rwth.i2.ltl2ba4j.formula.IProposition
 
getLabel() - Method in interface rwth.i2.ltl2ba4j.model.IGraphProposition
 
getLabel() - Method in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
getLabel() - Method in class rwth.i2.ltl2ba4j.model.impl.State
getLabel() - Method in interface rwth.i2.ltl2ba4j.model.IState
 
getLabels() - Method in class rwth.i2.ltl2ba4j.model.impl.Transition
getLabels() - Method in interface rwth.i2.ltl2ba4j.model.ITransition
 
getSourceState() - Method in class rwth.i2.ltl2ba4j.model.impl.Transition
getSourceState() - Method in interface rwth.i2.ltl2ba4j.model.ITransition
 
getSubformula() - Method in class rwth.i2.ltl2ba4j.formula.impl.Finally
getSubformula() - Method in class rwth.i2.ltl2ba4j.formula.impl.Globally
getSubformula() - Method in class rwth.i2.ltl2ba4j.formula.impl.Next
getSubformula() - Method in class rwth.i2.ltl2ba4j.formula.impl.Not
getSubformula() - Method in interface rwth.i2.ltl2ba4j.formula.IUnaryFormula
 
getSubformula1() - Method in interface rwth.i2.ltl2ba4j.formula.IBinaryFormula
 
getSubformula1() - Method in class rwth.i2.ltl2ba4j.formula.impl.And
getSubformula1() - Method in class rwth.i2.ltl2ba4j.formula.impl.Equivalent
getSubformula1() - Method in class rwth.i2.ltl2ba4j.formula.impl.Implies
getSubformula1() - Method in class rwth.i2.ltl2ba4j.formula.impl.Or
getSubformula1() - Method in class rwth.i2.ltl2ba4j.formula.impl.Release
getSubformula1() - Method in class rwth.i2.ltl2ba4j.formula.impl.Until
getSubformula2() - Method in interface rwth.i2.ltl2ba4j.formula.IBinaryFormula
 
getSubformula2() - Method in class rwth.i2.ltl2ba4j.formula.impl.And
getSubformula2() - Method in class rwth.i2.ltl2ba4j.formula.impl.Equivalent
getSubformula2() - Method in class rwth.i2.ltl2ba4j.formula.impl.Implies
getSubformula2() - Method in class rwth.i2.ltl2ba4j.formula.impl.Or
getSubformula2() - Method in class rwth.i2.ltl2ba4j.formula.impl.Release
getSubformula2() - Method in class rwth.i2.ltl2ba4j.formula.impl.Until
getTargetState() - Method in class rwth.i2.ltl2ba4j.model.impl.Transition
getTargetState() - Method in interface rwth.i2.ltl2ba4j.model.ITransition
 
getTransitions() - Method in class rwth.i2.ltl2ba4j.internal.jnibridge.BAJni
Returns the resulting automaton as a list of transitions.
Globally - Class in rwth.i2.ltl2ba4j.formula.impl
 
Globally(IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Globally
 
GraphFactory - Class in rwth.i2.ltl2ba4j.model.impl
 
GraphFactory() - Constructor for class rwth.i2.ltl2ba4j.model.impl.GraphFactory
 
GraphProposition - Class in rwth.i2.ltl2ba4j.model.impl
 
GraphProposition(boolean, boolean) - Constructor for class rwth.i2.ltl2ba4j.model.impl.GraphProposition
 
GraphProposition(String, boolean) - Constructor for class rwth.i2.ltl2ba4j.model.impl.GraphProposition
 

H

hashCode() - Method in class rwth.i2.ltl2ba4j.formula.impl.Proposition
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
hashCode() - Method in interface rwth.i2.ltl2ba4j.formula.IProposition
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
hashCode() - Method in interface rwth.i2.ltl2ba4j.model.IGraphProposition
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
hashCode() - Method in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
hashCode() - Method in class rwth.i2.ltl2ba4j.model.impl.State
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
hashCode() - Method in class rwth.i2.ltl2ba4j.model.impl.Transition
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
hashCode() - Method in interface rwth.i2.ltl2ba4j.model.IState
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.
hashCode() - Method in interface rwth.i2.ltl2ba4j.model.ITransition
Clients should implement this method, since the implementation uses HashSets, which require a proper hash code.

I

IAnd - Interface in rwth.i2.ltl2ba4j.formula
 
IBinaryFormula - Interface in rwth.i2.ltl2ba4j.formula
 
IEquivalent - Interface in rwth.i2.ltl2ba4j.formula
 
IFinally - Interface in rwth.i2.ltl2ba4j.formula
 
IFormula - Interface in rwth.i2.ltl2ba4j.formula
 
IFormulaFactory - Interface in rwth.i2.ltl2ba4j.formula
 
IGlobally - Interface in rwth.i2.ltl2ba4j.formula
 
IGraphFactory - Interface in rwth.i2.ltl2ba4j.model
 
IGraphProposition - Interface in rwth.i2.ltl2ba4j.model
 
IImplies - Interface in rwth.i2.ltl2ba4j.formula
 
Impl(IFormula, IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
Impl(IFormula, IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
Implies - Class in rwth.i2.ltl2ba4j.formula.impl
 
Implies(IFormula, IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Implies
 
INext - Interface in rwth.i2.ltl2ba4j.formula
 
INot - Interface in rwth.i2.ltl2ba4j.formula
 
IOr - Interface in rwth.i2.ltl2ba4j.formula
 
IProposition - Interface in rwth.i2.ltl2ba4j.formula
 
IRelease - Interface in rwth.i2.ltl2ba4j.formula
 
isFinal - Variable in class rwth.i2.ltl2ba4j.model.impl.State
 
isFinal() - Method in class rwth.i2.ltl2ba4j.model.impl.State
 
isFinal() - Method in interface rwth.i2.ltl2ba4j.model.IState
 
isInitial - Variable in class rwth.i2.ltl2ba4j.model.impl.State
 
isInitial() - Method in class rwth.i2.ltl2ba4j.model.impl.State
 
isInitial() - Method in interface rwth.i2.ltl2ba4j.model.IState
 
isNegated() - Method in interface rwth.i2.ltl2ba4j.model.IGraphProposition
 
isNegated() - Method in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
IState - Interface in rwth.i2.ltl2ba4j.model
 
ITransition - Interface in rwth.i2.ltl2ba4j.model
 
IUnaryFormula - Interface in rwth.i2.ltl2ba4j.formula
 
IUntil - Interface in rwth.i2.ltl2ba4j.formula
 

L

label - Variable in class rwth.i2.ltl2ba4j.formula.impl.Proposition
 
label - Variable in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
 
label - Variable in class rwth.i2.ltl2ba4j.model.impl.State
 
labels - Variable in class rwth.i2.ltl2ba4j.model.impl.Transition
 
LTL2BA4J - Class in rwth.i2.ltl2ba4j
 
LTL2BA4J() - Constructor for class rwth.i2.ltl2ba4j.LTL2BA4J
 

M

main(String[]) - Static method in class rwth.i2.ltl2ba4j.LTL2BA4J
 

N

negated - Variable in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
 
Next - Class in rwth.i2.ltl2ba4j.formula.impl
 
Next(IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Next
 
Not(IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
Not(IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
Not - Class in rwth.i2.ltl2ba4j.formula.impl
 
Not(IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Not
 

O

Or(IFormula, IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
Or(IFormula, IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
Or - Class in rwth.i2.ltl2ba4j.formula.impl
 
Or(IFormula, IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Or
 

P

Proposition(String) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
Proposition(String) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
Proposition - Class in rwth.i2.ltl2ba4j.formula.impl
 
Proposition(boolean) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Proposition
 
Proposition(String) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Proposition
 
Proposition(String, boolean) - Method in interface rwth.i2.ltl2ba4j.model.IGraphFactory
A proposition with the given label.
Proposition(String, boolean) - Method in class rwth.i2.ltl2ba4j.model.impl.GraphFactory
A proposition with the given label.

R

Release(IFormula, IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
Release(IFormula, IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
Release - Class in rwth.i2.ltl2ba4j.formula.impl
 
Release(IFormula, IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Release
 
rwth.i2.ltl2ba4j - package rwth.i2.ltl2ba4j
JNI bridge to ltl2ba.
rwth.i2.ltl2ba4j.formula - package rwth.i2.ltl2ba4j.formula
Interfaces defining Formulas in LTL.
rwth.i2.ltl2ba4j.formula.impl - package rwth.i2.ltl2ba4j.formula.impl
Default implementation.
rwth.i2.ltl2ba4j.internal.jnibridge - package rwth.i2.ltl2ba4j.internal.jnibridge
 
rwth.i2.ltl2ba4j.model - package rwth.i2.ltl2ba4j.model
Interfaces defining finite state machines.
rwth.i2.ltl2ba4j.model.impl - package rwth.i2.ltl2ba4j.model.impl
Default implementation.

S

setGraphFactory(IGraphFactory) - Static method in class rwth.i2.ltl2ba4j.LTL2BA4J
Sets a factory used to generate the resulting graph.
SigmaProposition() - Method in interface rwth.i2.ltl2ba4j.model.IGraphFactory
The unique SIGMA proposition, meaning any symbol.
SigmaProposition() - Method in class rwth.i2.ltl2ba4j.model.impl.GraphFactory
The unique SIGMA proposition, meaning any symbol.
SigmaProposition - Class in rwth.i2.ltl2ba4j.model.impl
 
SigmaProposition() - Constructor for class rwth.i2.ltl2ba4j.model.impl.SigmaProposition
 
sourceState - Variable in class rwth.i2.ltl2ba4j.model.impl.Transition
 
State(String, boolean, boolean) - Method in interface rwth.i2.ltl2ba4j.model.IGraphFactory
Constructs a state with the given label.
State(String, boolean, boolean) - Method in class rwth.i2.ltl2ba4j.model.impl.GraphFactory
Constructs a state with the given label.
State - Class in rwth.i2.ltl2ba4j.model.impl
 
State(String, boolean, boolean) - Constructor for class rwth.i2.ltl2ba4j.model.impl.State
 
subformula - Variable in class rwth.i2.ltl2ba4j.formula.impl.Finally
 
subformula - Variable in class rwth.i2.ltl2ba4j.formula.impl.Globally
 
subformula - Variable in class rwth.i2.ltl2ba4j.formula.impl.Next
 
subformula - Variable in class rwth.i2.ltl2ba4j.formula.impl.Not
 
subformula1 - Variable in class rwth.i2.ltl2ba4j.formula.impl.And
 
subformula1 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Equivalent
 
subformula1 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Implies
 
subformula1 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Or
 
subformula1 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Release
 
subformula1 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Until
 
subformula2 - Variable in class rwth.i2.ltl2ba4j.formula.impl.And
 
subformula2 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Equivalent
 
subformula2 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Implies
 
subformula2 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Or
 
subformula2 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Release
 
subformula2 - Variable in class rwth.i2.ltl2ba4j.formula.impl.Until
 

T

targetState - Variable in class rwth.i2.ltl2ba4j.model.impl.Transition
 
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.And
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Equivalent
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Finally
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Globally
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Implies
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Next
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Not
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Or
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Proposition
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Release
toString() - Method in class rwth.i2.ltl2ba4j.formula.impl.Until
toString() - Method in class rwth.i2.ltl2ba4j.model.impl.GraphProposition
toString() - Method in class rwth.i2.ltl2ba4j.model.impl.State
toString() - Method in class rwth.i2.ltl2ba4j.model.impl.Transition
Transition(Set<IGraphProposition>, IState, IState) - Method in interface rwth.i2.ltl2ba4j.model.IGraphFactory
A transition with the given label, source and target state
Transition(Set<IGraphProposition>, IState, IState) - Method in class rwth.i2.ltl2ba4j.model.impl.GraphFactory
A transition with the given label, source and target state
Transition - Class in rwth.i2.ltl2ba4j.model.impl
 
Transition(Set<IGraphProposition>, IState, IState) - Constructor for class rwth.i2.ltl2ba4j.model.impl.Transition
 

U

Until(IFormula, IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
Until(IFormula, IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory
Until - Class in rwth.i2.ltl2ba4j.formula.impl
 
Until(IFormula, IFormula) - Constructor for class rwth.i2.ltl2ba4j.formula.impl.Until
 

X

X(IFormula) - Method in interface rwth.i2.ltl2ba4j.formula.IFormulaFactory
 
X(IFormula) - Method in class rwth.i2.ltl2ba4j.formula.impl.FormulaFactory

A B D E F G H I L M N O P R S T U X

Eric Bodden, RWTH Aachen University, 2005.
Valid HTML 4.01 Strict! Valid CSS!