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
I
Id
- Class in
de.upb.swt.mcie.parser.token
Implements the token for an identifier.
Id(String)
- Constructor for class de.upb.swt.mcie.parser.token.
Id
Constructs a token for the identifier with the provided name.
ILLEGAL_INNER_NODE
- Static variable in exception de.upb.swt.mcie.robdds.
InternalError
Error number: This error indicates that the creation of an illegal inner node was requested.
ILLEGAL_TERMINAL_NODE
- Static variable in exception de.upb.swt.mcie.robdds.
InternalError
Indicates that an illegal terminal node was encountered.
ILLEGAL_UNPRIMED_VARIABLE
- Static variable in exception de.upb.swt.mcie.robdds.
IncorrectUseException
Error number: This error indicates that an operation encountered an unprimed variable that is not allowed.
IMP
- Static variable in class de.upb.swt.mcie.formulas.
BinaryOp
Code for the IMPlication operation.
impl
- Variable in class de.upb.swt.mcie.robdds.
Context
The implication operation in this context.
IncorrectUseException
- Exception in
de.upb.swt.mcie.formulas
Exception that results from an incorrect use of the API.
IncorrectUseException(int)
- Constructor for exception de.upb.swt.mcie.formulas.
IncorrectUseException
Constructs an IncorrectUseException with the provided error number.
IncorrectUseException
- Exception in
de.upb.swt.mcie.mc
Exception that results from an incorrect use of the model checking procedures, the models, or their extensions.
IncorrectUseException(int)
- Constructor for exception de.upb.swt.mcie.mc.
IncorrectUseException
Constructs an IncorrectUseException with the provided error number.
IncorrectUseException
- Exception in
de.upb.swt.mcie.robdds
Exception that results from an incorrect use of the API.
IncorrectUseException(int)
- Constructor for exception de.upb.swt.mcie.robdds.
IncorrectUseException
Constructs an IncorrectUseException with the provided error number.
init
- Variable in class de.upb.swt.mcie.mc.
Kripkestructure
The ROBDD representing the initial condition.
init
- Variable in class de.upb.swt.mcie.mc.
Transitionsystem
The ROBDD representing the initial condition.
InnerNode
- Class in
de.upb.swt.mcie.robdds
Represents the inner nodes of an ROBDD.
InnerNode(Variable, ROBDD, ROBDD)
- Constructor for class de.upb.swt.mcie.robdds.
InnerNode
Creates a new inner node.
innerNodesTable
- Variable in class de.upb.swt.mcie.robdds.
Context
This hash table holds references to all existing inner nodes.
InternalError
- Exception in
de.upb.swt.mcie.robdds
This exception indicates that some internal error has occurred.
InternalError(int)
- Constructor for exception de.upb.swt.mcie.robdds.
InternalError
Constructs an InternalError exception with the provided error number.
Inval
- Class in
de.upb.swt.mcie.parser.token
Implements an invalid token.
Inval()
- Constructor for class de.upb.swt.mcie.parser.token.
Inval
isprimed
- Variable in class de.upb.swt.mcie.robdds.
Variable
Field indicating whether the variable is primed or unprimed.
isPrimed()
- Method in class de.upb.swt.mcie.robdds.
Variable
Checks whether the variable is a primed variable.
isStateFormula()
- Method in class de.upb.swt.mcie.formulas.
Formula
Checks whether the formula is a state formula.
isStateFormula()
- Method in class de.upb.swt.mcie.formulas.
Variable
Checks whether the formula is a state formula.
isStepFormula()
- Method in class de.upb.swt.mcie.formulas.
Formula
Checks whether the formula is a step formula.
isStepFormula()
- Method in class de.upb.swt.mcie.formulas.
Variable
Checks whether the formula is a step formula.
isTemporalFormula()
- Method in class de.upb.swt.mcie.formulas.
Formula
Checks whether the formula is a temporal formula.
isTemporalFormula()
- Method in class de.upb.swt.mcie.formulas.
Variable
Checks whether the formula is a temporal formula.
isValid(ROBDD)
- Method in class de.upb.swt.mcie.mc.
FairModel
Checks whether all initial states are contained in the set f.
isValid(ROBDD)
- Method in class de.upb.swt.mcie.mc.
Kripkestructure
Checks whether all initial states are contained in the set f.
isValid(ROBDD)
- Method in class de.upb.swt.mcie.mc.
Model
Checks whether f is valid in the system.
isValid(ROBDD)
- Method in class de.upb.swt.mcie.mc.
Transitionsystem
Checks whether all initial states are contained in the set f.
isValid()
- Method in class de.upb.swt.mcie.robdds.
InnerNode
Returns true, if the ROBDD is valid (i.e. if it evaluates to true for any assignment).
isValid()
- Method in class de.upb.swt.mcie.robdds.
ROBDD
Returns true, if the ROBDD is valid (i.e. if it evaluates to true for any assignment).
isValid()
- Method in class de.upb.swt.mcie.robdds.
TerminalNode
Returns true, if the ROBDD is valid (i.e. it evaluates to true for any assignment).
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