|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use Model | |
---|---|
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. |
Uses of Model in de.upb.swt.mcie.formulas |
---|
Methods in de.upb.swt.mcie.formulas with parameters of type Model | |
---|---|
ROBDD |
Variable.toROBDD(Model model)
Returns the ROBDD that represents the set of all states in which this formula is valid. |
ROBDD |
UnaryOp.toROBDD(Model model)
Returns the ROBDD representation of the set of all states satisfying the formula. |
abstract ROBDD |
Formula.toROBDD(Model model)
Returns the ROBDD representation of the set of all states satisfying the formula. |
ROBDD |
Constant.toROBDD(Model model)
Returns the ROBDD that represents the set of all states in which this formula is valid. |
ROBDD |
BinaryOp.toROBDD(Model model)
Returns the ROBDD representation of the set of all states satisfying the formula. |
Uses of Model in de.upb.swt.mcie.mc |
---|
Subclasses of Model in de.upb.swt.mcie.mc | |
---|---|
class |
FairModel
Implements a fair model based on some other model. |
class |
Kripkestructure
Implements a Kripke structure. |
class |
Transitionsystem
Implements a transition system. |
Fields in de.upb.swt.mcie.mc declared as Model | |
---|---|
private Model |
FairModel.model
The underlying model (without fairness). |
Constructors in de.upb.swt.mcie.mc with parameters of type Model | |
---|---|
FairModel(Model model,
ROBDD[] fairness)
Constructs a fair model from some model and from a set of fairness conditions. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |