de.upb.swt.mcie.robdds
Class ROBDD

java.lang.Object
  extended by de.upb.swt.mcie.robdds.ROBDD
Direct Known Subclasses:
InnerNode, TerminalNode

public abstract class ROBDD
extends java.lang.Object

This abstract class represents the nodes of an ROBDD. All constructions on ROBDDs preserve their reducedness, because no operation will ever create a duplicate node or a redundant node.

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
(package private)  Context context
          The context of the ROBDD.
 
Constructor Summary
ROBDD()
           
 
Method Summary
abstract  ROBDD eval(Assignment ass)
          Evaluates the ROBDD in the given assignment ass, where the result is the ROBDD node at which the evaluation terminates.
abstract  Assignment getAssignment()
          Returns an assignment for which the ROBDD evaluates to true.
abstract  boolean isValid()
          Returns true, if the ROBDD is valid (i.e. if it evaluates to true for any assignment).
abstract  ROBDD negate()
          Returns the negation of the ROBDD.
abstract  ROBDD predecessors(ROBDD n)
          Considers this ROBBD as a transition relation and computes the predecessors of the set given as parameter.
abstract  ROBDD predecessors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the predecessors of a given set.
abstract  ROBDD relProd(ROBDD n)
          Computes the product of two relations.
abstract  ROBDD successors(ROBDD n)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
abstract  ROBDD successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

context

Context context
The context of the ROBDD.

Constructor Detail

ROBDD

public ROBDD()
Method Detail

negate

public abstract ROBDD negate()
Returns the negation of the ROBDD.

Returns:
the negation of the ROBDD.

predecessors

public abstract ROBDD predecessors(ROBDD n)
Considers this ROBBD as a transition relation and computes the predecessors of the set given as parameter.

Parameters:
n - the ROBDD representing the set for which the predecessors should be computed; this ROBDD must not refer to primed variables
Returns:
the set of predecessors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable
InternalError - can occur only, if somebody messed up the implementation of the ROBDD package

predecessors

public abstract ROBDD predecessors(ROBDD n,
                                   ChangeSet changeset)
Considers this ROBBD as a transition relation and computes the predecessors of a given set. Only the variables in the set changeable can be changed by the transition relation.

Parameters:
n - the ROBDD representing the set for which the predecessors should be computed; this ROBDD must not refer to primed variables
changeset - set of variables that may change in the transition relation; all other variables are not changed
Returns:
the set of predecessors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable or if the transition relation contains a primed variable that is not contained in the changeset
InternalError - can occur only, if somebody messed up the implementation of the ROBDD package

successors

public abstract ROBDD successors(ROBDD n)
Considers this ROBBD as a transition relation and computes the successors of a given set.

Parameters:
n - the ROBDD representing the set for which the successors should be computed; this ROBDD must not refer to primed variables
Returns:
the set of successors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable
InternalError - can occur only, if somebody messed up the implementation of the ROBDD package

successors

public abstract ROBDD successors(ROBDD n,
                                 ChangeSet changeset)
Considers this ROBBD as a transition relation and computes the successors of a given set. Only the variables in the set changeable can be changed by the transition relation.

Parameters:
n - the ROBDD representing the set for which the successors should be computed; this ROBDD must not refer to primed variables
changeset - set of variables that may change in the transition relation; all other variables are not changed
Returns:
the set of successors represented as an ROBDD
Throws:
IncorrectUseException - if the set n contains a primed variable or if the transition relation has a primed variable that is not contained in the changeset
InternalError - can occur only, if somebody messed up the implementation of the ROBDD package

isValid

public abstract boolean isValid()
Returns true, if the ROBDD is valid (i.e. if it evaluates to true for any assignment). This is true for the TerminalNode with value 1 only.

Returns:
true, if the ROBDD is valid.

getAssignment

public abstract Assignment getAssignment()
Returns an assignment for which the ROBDD evaluates to true.

Returns:
an assignment that evaluates to true for this ROBDD; null, if no such assignment exists

relProd

public abstract ROBDD relProd(ROBDD n)
Computes the product of two relations. This object is considered as the first relation, argument n is considered as the second relation.

This method is not fully tested yet!

Parameters:
n - the set second relation
Returns:
the product of the two relations

eval

public abstract ROBDD eval(Assignment ass)
Evaluates the ROBDD in the given assignment ass, where the result is the ROBDD node at which the evaluation terminates. If the evaluation is successful, it is the corresponding TerminalNode; if the evaluation is stuck due to an undefined value for some inner node, this node is returned. It is an error, if the assignment is from a different context.

Parameters:
ass - for which the ROBDD should be evaluated
Returns:
the final node
Throws:
IncorrectUseException - if the assignment is from a context different from the context of the ROBDD