|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use de.upb.swt.mcie.robdds | |
---|---|
de.upb.swt.mcie.formulas | This package implements formulas, which can be state formulas, transition formulas or temporal formulas. |
de.upb.swt.mcie.mc | This package implements models with the corresponding model checking procedures, and the main method for invoking the model checker. |
de.upb.swt.mcie.parser | This package implements a parser and compiler for formulas and models. |
de.upb.swt.mcie.robdds | This package implements reduced ordered binary decision diagrams (ROBDDs). |
Classes in de.upb.swt.mcie.robdds used by de.upb.swt.mcie.formulas | |
---|---|
ChangeSet
This class represents a set of variables, which restrict the changed variables in a transition relation. |
|
Context
Implements the context for an ROBDD, which comprises the set of variables and the order on these variables. |
|
ROBDD
This abstract class represents the nodes of an ROBDD. |
Classes in de.upb.swt.mcie.robdds used by de.upb.swt.mcie.mc | |
---|---|
ChangeSet
This class represents a set of variables, which restrict the changed variables in a transition relation. |
|
Context
Implements the context for an ROBDD, which comprises the set of variables and the order on these variables. |
|
ROBDD
This abstract class represents the nodes of an ROBDD. |
Classes in de.upb.swt.mcie.robdds used by de.upb.swt.mcie.parser | |
---|---|
Context
Implements the context for an ROBDD, which comprises the set of variables and the order on these variables. |
Classes in de.upb.swt.mcie.robdds used by de.upb.swt.mcie.robdds | |
---|---|
Assignment
This interface defines the basic methods of an assignment of values to some variables of a Context . |
|
BinOp
This class implements binary operations on ROBDDs. |
|
ChangeSet
This class represents a set of variables, which restrict the changed variables in a transition relation. |
|
Context
Implements the context for an ROBDD, which comprises the set of variables and the order on these variables. |
|
IncorrectUseException
Exception that results from an incorrect use of the API. |
|
InnerNode
Represents the inner nodes of an ROBDD. |
|
ROBDD
This abstract class represents the nodes of an ROBDD. |
|
TerminalNode
This class represents a terminal Node of an ROBDD. |
|
Variable
Implements a variable within an ROBDD's context. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |