Uses of Class
de.upb.swt.mcie.robdds.Context

Packages that use Context
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). 
 

Uses of Context in de.upb.swt.mcie.formulas
 

Methods in de.upb.swt.mcie.formulas with parameters of type Context
 ROBDD Variable.toROBDD(Context context)
          Returns the ROBDD that represents the set of all states in which this formula is valid.
 ROBDD UnaryOp.toROBDD(Context context)
          Returns the ROBDD representation of the set of all states satisfying the formula.
abstract  ROBDD Formula.toROBDD(Context context)
          Returns the ROBDD representation of the set of all states respectively the set of transitions satisfying the formula.
 ROBDD Constant.toROBDD(Context context)
          Returns the ROBDD that represents the set of all states in which this formula is valid.
 ROBDD BinaryOp.toROBDD(Context context)
          Returns the ROBDD representation of the set of all states respectively the set of transitions satisfying the formula.
 

Uses of Context in de.upb.swt.mcie.mc
 

Fields in de.upb.swt.mcie.mc declared as Context
private  Context Transitionsystem.context
          The context associated with this transition system.
private  Context Kripkestructure.context
          The context associated with this Kripkestructure.
 

Methods in de.upb.swt.mcie.mc that return Context
 Context Transitionsystem.getContext()
          Returns the context associated with this Kripke structure.
abstract  Context Model.getContext()
          Must implement an operation that returns the Context associated with this model.
 Context Kripkestructure.getContext()
          Returns the context associated with this Kripke structure.
 Context FairModel.getContext()
          Returns the context associated with this fair model structure.
 

Methods in de.upb.swt.mcie.mc with parameters of type Context
static ROBDD Procedures.transClosure(Context context, ROBDD r)
          This method calculates the transitive closure of a given relation.
 

Constructors in de.upb.swt.mcie.mc with parameters of type Context
FairModel(Context context)
          Constructs an empty fair Model.
Kripkestructure(Context context)
          Constructs an empty Kripke structure.
Kripkestructure(Context context, ROBDD init, ROBDD relation)
          Constructs a Kripke structure from the provided ROBDDs for the initial condition and the transition relation.
Transitionsystem(Context context)
          Constructs an empty transition structure.
Transitionsystem(Context context, ROBDD init, ROBDD[] transitions, ChangeSet[] changeSets)
          Constructs a transition structure from the provided ROBDDs for the initial condition and an array of transition relation (along with the set of variables that may be change by a transition).
 

Uses of Context in de.upb.swt.mcie.parser
 

Methods in de.upb.swt.mcie.parser with parameters of type Context
 FairModel Parser.parseFairKripkestructure(Context context)
          Parses a fair Kripke structure and returns it as result.
 FairModel Parser.parseFairTransitionsystem(Context context)
          Parses a fair transition system and returns it as result.
 Kripkestructure Parser.parseKripkestructure(Context context)
          Parses a Kripke structure and returns it as result.
 Transitionsystem Parser.parseTransitionsystem(Context context)
          Parses a transition system and returns it as result.
 

Uses of Context in de.upb.swt.mcie.robdds
 

Fields in de.upb.swt.mcie.robdds declared as Context
(package private)  Context Variable.context
          The context in which this variable is defined.
(package private)  Context ROBDD.context
          The context of the ROBDD.
private  Context HashAssignment.context
          The context of the assignment.
(package private)  Context ChangeSet.context
          The context.
private  Context BinOp.context
          The context for this binary operation.
 

Methods in de.upb.swt.mcie.robdds that return Context
 Context HashAssignment.getContext()
          Returns the context of the assignment.
 Context Assignment.getContext()
          Returns the context of the assignment.
 

Constructors in de.upb.swt.mcie.robdds with parameters of type Context
BinOp(Context context, boolean[][] truthTable)
          Creates a new binary operation from the truth table.
ChangeSet(Context context)
          Constructs an empty change set for a given context.
ChangeSet(Context context, Variable[] variables)
          Constructs a set of variables in a given context.
HashAssignment(Context context)
          Constructs an empty assignment, i.e. a mapping that assigns don't care values (null) to each variable.
TerminalNode(Context context, int t)
          Creates a terminal node for the given truth value (0 or 1 for false and true).
Variable(Context context, java.lang.String name, int number, boolean isprimed)
          Constructs a variable.