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.

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