|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |