Uses of Class
de.upb.swt.mcie.mc.Model

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.