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

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.