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

Packages that use ROBDD
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.robdds This package implements reduced ordered binary decision diagrams (ROBDDs). 
 

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

Methods in de.upb.swt.mcie.formulas that return ROBDD
 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.
 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 ROBDD in de.upb.swt.mcie.mc
 

Fields in de.upb.swt.mcie.mc declared as ROBDD
private  ROBDD FairModel.fair
          The set of all states in which a fair path starts.
private  ROBDD[] FairModel.fairness
          An array of ROBDDs representing the fairness conditions.
private  ROBDD Transitionsystem.init
          The ROBDD representing the initial condition.
private  ROBDD Kripkestructure.init
          The ROBDD representing the initial condition.
private  ROBDD Transitionsystem.reachable
          The reachable states of this transition system.
private  ROBDD Kripkestructure.reachable
          If calculated already, this represents the reachable states of the Kripke structure.
private  ROBDD Kripkestructure.relation
          The ROBDD representing the transition relation.
private  ROBDD[] Transitionsystem.transitions
          An array of ROBDDs representing the transitions.
 

Methods in de.upb.swt.mcie.mc that return ROBDD
 ROBDD Transitionsystem.computeReachable()
          Returns the reachable states of the transition system.
 ROBDD Model.computeReachable()
          Sometimes model checking procedures are more efficient, when the reachable states of the model are calculated first and used in the model checking procedures.
 ROBDD Kripkestructure.computeReachable()
          Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state.
 ROBDD FairModel.computeReachable()
          Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state.
 ROBDD Model.eg(ROBDD f)
          Standard implementation of the operation EG f.
 ROBDD FairModel.eg(ROBDD f)
          Implements the operation EG considering the fairness conditions.
 ROBDD Model.er(ROBDD f1, ROBDD f2)
          Standard implementation of the operation E[ f1 R f2 ].
 ROBDD FairModel.er(ROBDD f1, ROBDD f2)
          Implements the operation ER considering the fairness conditions.
 ROBDD Model.eu(ROBDD f1, ROBDD f2)
          Standard implementation of the operation E[ f1 U f2 ].
 ROBDD FairModel.eu(ROBDD f1, ROBDD f2)
          Implements the operation EU considering the fairness conditions.
 ROBDD Transitionsystem.ex(ROBDD f)
          Implements the operation EX.
abstract  ROBDD Model.ex(ROBDD f)
          Must implement the EX operator for this particular model.
 ROBDD Kripkestructure.ex(ROBDD f)
          Implements the operation EX.
 ROBDD FairModel.ex(ROBDD f)
          Implements the operation EX considering the fairness conditions.
private  ROBDD Kripkestructure.reachable()
          Computes the reachable states of the Kripke structure.
 ROBDD FairModel.reachable()
          Computes the reachable states of the fair model.
static ROBDD Procedures.transClosure(Context context, ROBDD r)
          This method calculates the transitive closure of a given relation.
 

Methods in de.upb.swt.mcie.mc with parameters of type ROBDD
 ROBDD Model.eg(ROBDD f)
          Standard implementation of the operation EG f.
 ROBDD FairModel.eg(ROBDD f)
          Implements the operation EG considering the fairness conditions.
 ROBDD Model.er(ROBDD f1, ROBDD f2)
          Standard implementation of the operation E[ f1 R f2 ].
 ROBDD FairModel.er(ROBDD f1, ROBDD f2)
          Implements the operation ER considering the fairness conditions.
 ROBDD Model.eu(ROBDD f1, ROBDD f2)
          Standard implementation of the operation E[ f1 U f2 ].
 ROBDD FairModel.eu(ROBDD f1, ROBDD f2)
          Implements the operation EU considering the fairness conditions.
 ROBDD Transitionsystem.ex(ROBDD f)
          Implements the operation EX.
abstract  ROBDD Model.ex(ROBDD f)
          Must implement the EX operator for this particular model.
 ROBDD Kripkestructure.ex(ROBDD f)
          Implements the operation EX.
 ROBDD FairModel.ex(ROBDD f)
          Implements the operation EX considering the fairness conditions.
 boolean Transitionsystem.isValid(ROBDD f)
          Checks whether all initial states are contained in the set f.
 boolean Model.isValid(ROBDD f)
          Checks whether f is valid in the system.
 boolean Kripkestructure.isValid(ROBDD f)
          Checks whether all initial states are contained in the set f.
 boolean FairModel.isValid(ROBDD f)
          Checks whether all initial states are contained in the set f.
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 ROBDD
FairModel(Model model, ROBDD[] fairness)
          Constructs a fair model from some model and from a set of fairness conditions.
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, 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).
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 ROBDD in de.upb.swt.mcie.robdds
 

Subclasses of ROBDD in de.upb.swt.mcie.robdds
(package private)  class InnerNode
          Represents the inner nodes of an ROBDD.
(package private)  class TerminalNode
          This class represents a terminal Node of an ROBDD.
 

Fields in de.upb.swt.mcie.robdds declared as ROBDD
(package private)  ROBDD InnerNode.high
          Outgoing arc for value 1.
(package private)  ROBDD InnerNode.low
          Outgoing arc for value 0.
private  ROBDD NodePair.n1
          The first node of the pair.
private  ROBDD NodePair.n2
          The second node of the pair.
(package private)  ROBDD Variable.repr
          The ROBDD representing the formula that consists of this variable only.
 

Methods in de.upb.swt.mcie.robdds that return ROBDD
private  ROBDD BinOp.apply(InnerNode n1, InnerNode n2)
          Applies the binary operation to the two ROBDDs.
 ROBDD BinOp.apply(ROBDD n1, ROBDD n2)
          Applies the binary operation to the two ROBDDs.
private  ROBDD BinOp.apply(ROBDD n1, TerminalNode n2)
          Applies the binary operation to the two ROBDDs.
private  ROBDD BinOp.apply(TerminalNode n1, ROBDD n2)
          Applies the binary operation to the two ROBDDs.
(package private)  ROBDD Context.createInnerNode(Variable variable, ROBDD low, ROBDD high)
          Creates the inner node, provided that it is not duplicate and not redundant.
 ROBDD TerminalNode.eval(Assignment ass)
          Evaluates the ROBDD in the given assignment, where the result is the ROBDD node at which the evaluation terminates.
abstract  ROBDD ROBDD.eval(Assignment ass)
          Evaluates the ROBDD in the given assignment ass, where the result is the ROBDD node at which the evaluation terminates.
 ROBDD InnerNode.eval(Assignment ass)
          Evaluates the ROBDD in the given assignment, where the result is the ROBDD node at which the evaluation terminates.
 ROBDD TerminalNode.negate()
          Returns the negation of the ROBDD in this context.
abstract  ROBDD ROBDD.negate()
          Returns the negation of the ROBDD.
 ROBDD InnerNode.negate()
          Returns the negation of this ROBDD.
private  ROBDD TerminalNode.predecessors(InnerNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD InnerNode.predecessors(InnerNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD TerminalNode.predecessors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD InnerNode.predecessors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD TerminalNode.predecessors(ROBDD n)
          Returns the ROBBD with all the predecessors of a set n.
abstract  ROBDD ROBDD.predecessors(ROBDD n)
          Considers this ROBBD as a transition relation and computes the predecessors of the set given as parameter.
 ROBDD InnerNode.predecessors(ROBDD n)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD TerminalNode.predecessors(ROBDD n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
abstract  ROBDD ROBDD.predecessors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the predecessors of a given set.
 ROBDD InnerNode.predecessors(ROBDD n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD TerminalNode.predecessors(TerminalNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD InnerNode.predecessors(TerminalNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD TerminalNode.predecessors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD InnerNode.predecessors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD TerminalNode.relProd(InnerNode n)
          Computes the product of two relations.
private  ROBDD InnerNode.relProd(InnerNode n)
          Computes the product of two relations.
 ROBDD TerminalNode.relProd(ROBDD n)
          Computes the product of two relations.
abstract  ROBDD ROBDD.relProd(ROBDD n)
          Computes the product of two relations.
 ROBDD InnerNode.relProd(ROBDD n)
          Computes the product of two relations.
private  ROBDD TerminalNode.relProd(TerminalNode n)
          Computes the product of two relations.
private  ROBDD InnerNode.relProd(TerminalNode n)
          Computes the product of two relations.
 ROBDD TerminalNode.successors(InnerNode n)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD InnerNode.successors(InnerNode n)
          Returns the ROBBD with all the successors of a set n.
 ROBDD TerminalNode.successors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD InnerNode.successors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
 ROBDD TerminalNode.successors(ROBDD n)
          Returns the ROBBD with all the successors of a set n.
abstract  ROBDD ROBDD.successors(ROBDD n)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
 ROBDD InnerNode.successors(ROBDD n)
          Returns the ROBBD with all the successors of a set n.
 ROBDD TerminalNode.successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
abstract  ROBDD ROBDD.successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
 ROBDD InnerNode.successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
private  ROBDD TerminalNode.successors(TerminalNode n)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD InnerNode.successors(TerminalNode n)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD TerminalNode.successors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD InnerNode.successors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
 ROBDD Variable.toROBDD()
          Returns the ROBDD representation for this variable (considered as a formula).
 

Methods in de.upb.swt.mcie.robdds with parameters of type ROBDD
 ROBDD BinOp.apply(ROBDD n1, ROBDD n2)
          Applies the binary operation to the two ROBDDs.
private  ROBDD BinOp.apply(ROBDD n1, TerminalNode n2)
          Applies the binary operation to the two ROBDDs.
private  ROBDD BinOp.apply(TerminalNode n1, ROBDD n2)
          Applies the binary operation to the two ROBDDs.
(package private)  ROBDD Context.createInnerNode(Variable variable, ROBDD low, ROBDD high)
          Creates the inner node, provided that it is not duplicate and not redundant.
 ROBDD TerminalNode.predecessors(ROBDD n)
          Returns the ROBBD with all the predecessors of a set n.
abstract  ROBDD ROBDD.predecessors(ROBDD n)
          Considers this ROBBD as a transition relation and computes the predecessors of the set given as parameter.
 ROBDD InnerNode.predecessors(ROBDD n)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD TerminalNode.predecessors(ROBDD n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
abstract  ROBDD ROBDD.predecessors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the predecessors of a given set.
 ROBDD InnerNode.predecessors(ROBDD n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD TerminalNode.relProd(ROBDD n)
          Computes the product of two relations.
abstract  ROBDD ROBDD.relProd(ROBDD n)
          Computes the product of two relations.
 ROBDD InnerNode.relProd(ROBDD n)
          Computes the product of two relations.
 ROBDD TerminalNode.successors(ROBDD n)
          Returns the ROBBD with all the successors of a set n.
abstract  ROBDD ROBDD.successors(ROBDD n)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
 ROBDD InnerNode.successors(ROBDD n)
          Returns the ROBBD with all the successors of a set n.
 ROBDD TerminalNode.successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
abstract  ROBDD ROBDD.successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
 ROBDD InnerNode.successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
 

Constructors in de.upb.swt.mcie.robdds with parameters of type ROBDD
InnerNode(Variable variable, ROBDD low, ROBDD high)
          Creates a new inner node.
NodePair(ROBDD n1, ROBDD n2)
          Constructs a pair of two ROBDD nodes.