de.upb.swt.mcie.robdds
Class TerminalNode

java.lang.Object
  extended by de.upb.swt.mcie.robdds.ROBDD
      extended by de.upb.swt.mcie.robdds.TerminalNode

 class TerminalNode
extends ROBDD

This class represents a terminal Node of an ROBDD. There is no need to have more than the two terminal nodes low and high in each context. The Context is responsible for instantiating these two terminal nodes as its members Context.low and Context.high.

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
(package private)  int value
          The value of the corresponding node.
 
Fields inherited from class de.upb.swt.mcie.robdds.ROBDD
context
 
Constructor Summary
TerminalNode(Context context, int t)
          Creates a terminal node for the given truth value (0 or 1 for false and true).
 
Method Summary
 ROBDD eval(Assignment ass)
          Evaluates the ROBDD in the given assignment, where the result is the ROBDD node at which the evaluation terminates.
 Assignment getAssignment()
          Returns an assignment for which the ROBDD evaluates to true.
 boolean isValid()
          Returns true, if the ROBDD is valid (i.e. it evaluates to true for any assignment).
 ROBDD negate()
          Returns the negation of the ROBDD in this context.
private  ROBDD predecessors(InnerNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD predecessors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD predecessors(ROBDD n)
          Returns the ROBBD with all the predecessors of a set n.
 ROBDD predecessors(ROBDD n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD predecessors(TerminalNode n)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD predecessors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the predecessors of a set n.
private  ROBDD relProd(InnerNode n)
          Computes the product of two relations.
 ROBDD relProd(ROBDD n)
          Computes the product of two relations.
private  ROBDD relProd(TerminalNode n)
          Computes the product of two relations.
 ROBDD successors(InnerNode n)
          Returns the ROBBD with all the successors of a set n.
 ROBDD successors(InnerNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
 ROBDD successors(ROBDD n)
          Returns the ROBBD with all the successors of a set n.
 ROBDD successors(ROBDD n, ChangeSet changeset)
          Considers this ROBBD as a transition relation and computes the successors of a given set.
private  ROBDD successors(TerminalNode n)
          Returns the ROBBD with all the successors of a set n.
private  ROBDD successors(TerminalNode n, ChangeSet changeset)
          Returns the ROBBD with all the successors of a set n.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

value

int value
The value of the corresponding node. The type is an int value rather than a boolean. 0 stands for false and 1 stands for true.

Constructor Detail

TerminalNode

TerminalNode(Context context,
             int t)
Creates a terminal node for the given truth value (0 or 1 for false and true). The constructor is not public such that no other terminal nodes can only be created from outside the ROBBD package.

Method Detail

negate

public ROBDD negate()
Returns the negation of the ROBDD in this context.

Specified by:
negate in class ROBDD
Returns:
the negated ROBDD
See Also:
Context

predecessors

public ROBDD predecessors(ROBDD n)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. An invocation of this method with an ROBDD from a different context results in an exception. This method only dispatches the call to more specific private methods.

Specified by:
predecessors in class ROBDD
Parameters:
n - the set for which the predecessors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
Returns:
the predecessors
Throws:
IncorrectUse - if contexts do not coincide
InternalError - if somebody messed up the implementation of this package
See Also:
ROBDD.predecessors(ROBDD), predecessors(TerminalNode), predecessors(InnerNode)

predecessors

private ROBDD predecessors(InnerNode n)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an inner node.

Parameters:
n - the set for which the predecessors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
Returns:
the predecessors
See Also:
ROBDD.predecessors(ROBDD)

predecessors

private ROBDD predecessors(TerminalNode n)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an terminal node.

Parameters:
n - the set for which the predecessors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
Returns:
the predecessors
See Also:
ROBDD.predecessors(ROBDD)

predecessors

public ROBDD predecessors(ROBDD n,
                          ChangeSet changeset)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. An invocation of this method with an ROBDD from a different context results in an exception. This method only dispatches the call to more specific private methods.

Specified by:
predecessors in class ROBDD
Parameters:
n - the set for which the predecessors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
changeset - the set of variables that may change
Returns:
the predecessors
Throws:
IncorrectUse - if contexts do not coincide
InternalError - if somebody messed up the implementation of this package
See Also:
ROBDD.predecessors(ROBDD, ChangeSet), predecessors(TerminalNode, ChangeSet), predecessors(InnerNode, ChangeSet)

predecessors

private ROBDD predecessors(InnerNode n,
                           ChangeSet changeset)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an inner node.

Parameters:
n - the set for which the predecessors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
changeset - the set of variables that may change
Returns:
the predecessors
See Also:
ROBDD.predecessors(ROBDD, ChangeSet)

predecessors

private ROBDD predecessors(TerminalNode n,
                           ChangeSet changeset)
Returns the ROBBD with all the predecessors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an terminal node.

Parameters:
n - the set for which the predecessors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
changeset - the set of variables that may change
Returns:
the predecessors
See Also:
ROBDD.predecessors(ROBDD, ChangeSet)

successors

public ROBDD successors(ROBDD n)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. An invocation of this method with an ROBDD from a different context results in an exception. This method only dispatches the call to more specific private methods.

Specified by:
successors in class ROBDD
Parameters:
n - the set for which the successors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
Returns:
the successors
Throws:
IncorrectUse - if contexts do not coincide
InternalError - if somebody messed up the implementation of this package
See Also:
ROBDD.successors(ROBDD), successors(InnerNode), successors(TerminalNode)

successors

public ROBDD successors(InnerNode n)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an inner node.

Parameters:
n - the set for which the successors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
Returns:
the successors
See Also:
ROBDD.successors(ROBDD)

successors

private ROBDD successors(TerminalNode n)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an terminal node.

Parameters:
n - the set for which the successors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
Returns:
the successors
See Also:
ROBDD.successors(ROBDD)

successors

public 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.

Specified by:
successors in class ROBDD
Parameters:
n - the set, this ROBDD may not refer to primed variables
changeset - variables that may change in the transition relation
Returns:
the set of successors of the set
Throws:
IncorrectUseException - if the set n contains a primed variable

successors

public ROBDD successors(InnerNode n,
                        ChangeSet changeset)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an inner node.

Parameters:
n - the set for which the successors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
changeset - variables that may change in the transition relation
Returns:
the successors
See Also:
ROBDD.successors(ROBDD)

successors

private ROBDD successors(TerminalNode n,
                         ChangeSet changeset)
Returns the ROBBD with all the successors of a set n. This class itself plays the role of the transition relation. This method implements the case where the set is represented by an terminal node.

Parameters:
n - the set for which the successors should be calculated; it is illegal to have a primed variable in this ROBDD, but it will not result in an exception, here
changeset - variables that may change in the transition relation
Returns:
the successors
See Also:
ROBDD.successors(ROBDD)

isValid

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

Specified by:
isValid in class ROBDD
Returns:
true, if the ROBDD is valid.

getAssignment

public Assignment getAssignment()
Returns an assignment for which the ROBDD evaluates to true. It returns null, if no such assignment exists.

Specified by:
getAssignment in class ROBDD
Returns:
an assignment that evaluates to true for this ROBDD; null, if no such assignment exists
See Also:
ROBDD.getAssignment()

relProd

public 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. An invocation of this method with an ROBDD from a different context results in an exception. This method dispatches the call to the more specific private methods.

This method is not fully tested yet!

Specified by:
relProd in class ROBDD
Parameters:
n - the set second relation
Returns:
the product of the two relations

relProd

private ROBDD relProd(InnerNode 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 implements the case, where the second argument is an inner node (i.e. a non-empty relation).

This method is not fully tested yet!

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

relProd

private ROBDD relProd(TerminalNode 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 implements the case, where the second argument is a terminal node (i.e. it is either the full relation or the empty relation).

This method is not fully tested yet!

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

eval

public ROBDD eval(Assignment ass)
Evaluates the ROBDD in the given assignment, where the result is the ROBDD node at which the evaluation terminates. Here, the TerminalNode is immediately returned. It is an error, if the assignment is from a different context.

Specified by:
eval in class ROBDD
Parameters:
ass - for which the ROBDD should be evaluated
Returns:
this node (if the assignment is from the same context)