Overview
Package
Class
Use
Tree
Deprecated
Index
Help
PREV LETTER
NEXT LETTER
FRAMES
NO FRAMES
All Classes
A
B
C
D
E
F
G
H
I
K
L
M
N
O
P
R
S
T
U
V
X
C
ChangeSet
- Class in
de.upb.swt.mcie.robdds
This class represents a set of variables, which restrict the changed variables in a transition relation.
ChangeSet(Context)
- Constructor for class de.upb.swt.mcie.robdds.
ChangeSet
Constructs an empty change set for a given context.
ChangeSet(Context, Variable[])
- Constructor for class de.upb.swt.mcie.robdds.
ChangeSet
Constructs a set of variables in a given context.
changeSets
- Variable in class de.upb.swt.mcie.mc.
Transitionsystem
An array of ChangeSets representing those variables that may change in the corresponding transition.
clearHashtable()
- Method in class de.upb.swt.mcie.robdds.
BinOp
Clears the hash table keeping track of pairs of ROBDD nodes for which this binary operation has already been computed in this context.
clearHashTables()
- Method in class de.upb.swt.mcie.mc.
Model
If the model maintains hash tables, calling this method will clear all hash tables (if possible).
clearHashTables()
- Method in class de.upb.swt.mcie.mc.
Transitionsystem
Clears all hash tables associated with this model.
clearHashTables()
- Method in class de.upb.swt.mcie.robdds.
ChangeSet
Clears the hash tables for the predecessor calculations with respect to this changeset.
clearHashTables()
- Method in class de.upb.swt.mcie.robdds.
Context
Clears the hash tables of all operations in this context.
CLOSE
- Static variable in class de.upb.swt.mcie.parser.token.
Brack
The code for a closing bracket.
column
- Variable in class de.upb.swt.mcie.parser.
Scanner
The column number of the current position in the reader.
column
- Variable in class de.upb.swt.mcie.parser.token.
Token
The column in the character sequence at which the token starts.
COMMA
- Static variable in class de.upb.swt.mcie.parser.token.
Sep
The code for a comma.
computeReachable()
- Method in class de.upb.swt.mcie.mc.
FairModel
Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state.
computeReachable()
- Method in class de.upb.swt.mcie.mc.
Kripkestructure
Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state.
computeReachable()
- Method in class de.upb.swt.mcie.mc.
Model
Sometimes model checking procedures are more efficient, when the reachable states of the model are calculated first and used in the model checking procedures.
computeReachable()
- Method in class de.upb.swt.mcie.mc.
Transitionsystem
Returns the reachable states of the transition system.
Const
- Class in
de.upb.swt.mcie.parser.token
Implements a token for a constant.
Const(int)
- Constructor for class de.upb.swt.mcie.parser.token.
Const
Constructs a token for a constant with the given value.
Constant
- Class in
de.upb.swt.mcie.formulas
Implements a constants, which can be true or false.
Constant(int)
- Constructor for class de.upb.swt.mcie.formulas.
Constant
Constructs a constant with the provided value.
contains(Variable)
- Method in class de.upb.swt.mcie.robdds.
ChangeSet
Checks whether the given variable is in this set.
context
- Variable in class de.upb.swt.mcie.mc.
Kripkestructure
The context associated with this Kripkestructure.
context
- Variable in class de.upb.swt.mcie.mc.
Transitionsystem
The context associated with this transition system.
context
- Variable in class de.upb.swt.mcie.robdds.
BinOp
The context for this binary operation.
context
- Variable in class de.upb.swt.mcie.robdds.
ChangeSet
The context.
Context
- Class in
de.upb.swt.mcie.robdds
Implements the context for an ROBDD, which comprises the set of variables and the order on these variables.
Context()
- Constructor for class de.upb.swt.mcie.robdds.
Context
context
- Variable in class de.upb.swt.mcie.robdds.
HashAssignment
The context of the assignment.
context
- Variable in class de.upb.swt.mcie.robdds.
ROBDD
The context of the ROBDD.
context
- Variable in class de.upb.swt.mcie.robdds.
Variable
The context in which this variable is defined.
CONTEXT_MISMATCH
- Static variable in exception de.upb.swt.mcie.robdds.
IncorrectUseException
Error number: This error indicates that an operation used ROBDDs from different contexts.
createInnerNode(Variable, ROBDD, ROBDD)
- Method in class de.upb.swt.mcie.robdds.
Context
Creates the inner node, provided that it is not duplicate and not redundant.
createVariable(String)
- Method in class de.upb.swt.mcie.robdds.
Context
Creates a pair of new variables for the given name and returns the unprimed version of this pair as a result.
current
- Variable in class de.upb.swt.mcie.parser.
Scanner
The current token.
currentChar
- Variable in class de.upb.swt.mcie.parser.
Scanner
The character at the current position in the reader.
Overview
Package
Class
Use
Tree
Deprecated
Index
Help
PREV LETTER
NEXT LETTER
FRAMES
NO FRAMES
All Classes
A
B
C
D
E
F
G
H
I
K
L
M
N
O
P
R
S
T
U
V
X