|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use ChangeSet | |
---|---|
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 ChangeSet in de.upb.swt.mcie.formulas |
---|
Methods in de.upb.swt.mcie.formulas with parameters of type ChangeSet | |
---|---|
void |
Variable.addChangedVariables(ChangeSet changeset)
Adds all variables that occur primed within the formula to the given change set. |
void |
UnaryOp.addChangedVariables(ChangeSet changeset)
Adds all variables that occur primed within the formula to the given change set. |
abstract void |
Formula.addChangedVariables(ChangeSet changeset)
Adds all variables that occur primed within the formula to the given change set. |
void |
Constant.addChangedVariables(ChangeSet changeset)
Adds all variables that occur primed within the formula to the given change set. |
void |
BinaryOp.addChangedVariables(ChangeSet changeset)
Adds all variables that occur primed within the formula to the given change set. |
Uses of ChangeSet in de.upb.swt.mcie.mc |
---|
Fields in de.upb.swt.mcie.mc declared as ChangeSet | |
---|---|
private ChangeSet[] |
Transitionsystem.changeSets
An array of ChangeSets representing those variables that may change in the corresponding transition. |
Constructors in de.upb.swt.mcie.mc with parameters of type ChangeSet | |
---|---|
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 ChangeSet in de.upb.swt.mcie.robdds |
---|
Methods in de.upb.swt.mcie.robdds with parameters of type ChangeSet | |
---|---|
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,
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,
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. |
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,
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,
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. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |