|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectde.upb.swt.mcie.robdds.ROBDD
de.upb.swt.mcie.robdds.InnerNode
class InnerNode
Represents the inner nodes of an ROBDD. An inner node is represented by a reference to the corresponding variable and its two successor nodes low and high.
Field Summary | |
---|---|
(package private) ROBDD |
high
Outgoing arc for value 1. |
(package private) ROBDD |
low
Outgoing arc for value 0. |
private InnerNode |
negation
If defined, this attribute refers to the complement of this ROBDD. |
(package private) Variable |
variable
The variable associated with this inner node. |
Fields inherited from class de.upb.swt.mcie.robdds.ROBDD |
---|
context |
Constructor Summary | |
---|---|
InnerNode(Variable variable,
ROBDD low,
ROBDD high)
Creates a new inner node. |
Method Summary | |
---|---|
boolean |
equals(java.lang.Object o)
Checks whether this inner node is equal to an other node. |
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. |
int |
hashCode()
Returns the hash code of this inner node. |
boolean |
isValid()
Returns true, if the ROBDD is valid (i.e. if it evaluates to true for any assignment). |
ROBDD |
negate()
Returns the negation of this ROBDD. |
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. |
private ROBDD |
successors(InnerNode n)
Returns the ROBBD with all the successors of a set n. |
private 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, finalize, getClass, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
Variable variable
ROBDD low
ROBDD high
private InnerNode negation
Constructor Detail |
---|
InnerNode(Variable variable, ROBDD low, ROBDD high)
Context.createInnerNode(Variable,ROBDD,ROBDD)
.
This method also maintains a hash table for all inner nodes.
variable
- the variable associated with this inner nodelow
- outgoing arc for value 0high
- outgoing arc for value 1
IncorrectUseException
- if context of the variables
and successor nodes do not coincideMethod Detail |
---|
public ROBDD negate()
negate
in class ROBDD
public ROBDD predecessors(ROBDD n)
predecessors
in class ROBDD
n
- the ROBDD representing the set for which the predecessors
should be computed; this ROBDD must not refer to primed
variables
IncorrectUseException
- if the set n contains a primed
variable
InternalError
- can occur only, if somebody messed up
the implementation of the ROBDD packageROBDD.predecessors(ROBDD)
,
predecessors(InnerNode)
,
predecessors(TerminalNode)
private ROBDD predecessors(InnerNode n)
n
- the ROBDD representing the set for which the predecessors
should be computed; this ROBDD must not refer to primed
variables
IncorrectUseException
- if the set n contains a primed
variable
InternalError
- can occur only, if somebody messed up
the implementation of the ROBDD packageROBDD.predecessors(ROBDD)
private ROBDD predecessors(TerminalNode n)
n
- the ROBDD representing the set for which the predecessors
should be computed
ROBDD.predecessors(ROBDD)
public ROBDD predecessors(ROBDD n, ChangeSet changeset)
predecessors
in class ROBDD
n
- the ROBDD representing the set for which the
predecessors should be computedchangeset
- the set of variables that can change
IncorrectUseException
- if the set n contains a primed
variable or the transition relation contains a primed
variable that is not in the changeset
InternalError
- can occur only, if somebody messed up
the implementation of the ROBDD packageROBDD.predecessors(ROBDD, ChangeSet)
,
predecessors(InnerNode, ChangeSet)
,
predecessors(TerminalNode, ChangeSet)
private ROBDD predecessors(InnerNode n, ChangeSet changeset)
n
- the ROBDD representing the set for which the
predecessors should be computedchangeset
- the set of variables that can change
IncorrectUseException
- if the set n contains a primed
variable or the transition relation contains a primed
variable that is not in the changesetROBDD.predecessors(ROBDD, ChangeSet)
private ROBDD predecessors(TerminalNode n, ChangeSet changeset)
n
- the ROBDD representing the set for which the
predecessors should be computedchangeset
- the set of variables that can change
IncorrectUseException
- if the transition relation
contains a primed variable that is not in the changesetROBDD.predecessors(ROBDD, ChangeSet)
public ROBDD successors(ROBDD n)
successors
in class ROBDD
n
- the set, this ROBDD must not refer to primed variables
IncorrectUseException
- if the set n contains a primed
variable
InternalError
- if somebody messed up the implementation
of this packageROBDD.successors(ROBDD)
,
successors(InnerNode)
,
successors(TerminalNode)
private ROBDD successors(InnerNode n)
n
- the set, this ROBDD must not refer to primed variables
IncorrectUseException
- if the set n contains a primed
variableROBDD.successors(ROBDD)
private ROBDD successors(TerminalNode n)
n
- the set
ROBDD.successors(ROBDD)
public ROBDD successors(ROBDD n, ChangeSet changeset)
successors
in class ROBDD
n
- the set, this ROBDD must not refer to primed variableschangeset
- variables that may change in the transition
relation
IncorrectUseException
- if the set n contains a primed
variable or the transition relation contains a primed
variable that is not in the changeset
InternalError
- if somebody messed up the implementation
of this packageROBDD.successors(ROBDD, ChangeSet)
,
successors(InnerNode, ChangeSet)
,
successors(TerminalNode, ChangeSet)
private ROBDD successors(InnerNode n, ChangeSet changeset)
n
- the set, this ROBDD may not refer to primed variableschangeset
- variables that may change in the transition
relation
IncorrectUseException
- if the set n contains a primed
variable or the transition relation contains a primed
variable that is not in the changesetROBDD.successors(ROBDD, ChangeSet)
private ROBDD successors(TerminalNode n, ChangeSet changeset)
n
- the setchangeset
- variables that may change in the transition
relation
IncorrectUseException
- if the transition relation
contains a primed variable that is not in the changesetROBDD.successors(ROBDD, ChangeSet)
public boolean isValid()
isValid
in class ROBDD
public Assignment getAssignment()
getAssignment
in class ROBDD
public int hashCode()
HashMap
and WeakHashMap
). Here,
we use a simple minded calculation that tries not to compromise the
randomness of the hash codes of its parts. Moreover, the calculation
guarantees that a symmetric pair has a different hash code.
But, there may be better ways to calculate the hash code.
hashCode
in class java.lang.Object
public boolean equals(java.lang.Object o)
HashMap
and
WeakHashMap
).
equals
in class java.lang.Object
o
- object to be compared with
public ROBDD relProd(ROBDD n)
This method is not fully tested yet!
relProd
in class ROBDD
n
- the set second relation
private ROBDD relProd(InnerNode n)
This method is not fully tested yet!
n
- the set second relation
private ROBDD relProd(TerminalNode n)
This method is not fully tested yet!
n
- the set second relation
public ROBDD eval(Assignment ass)
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.
eval
in class ROBDD
ass
- for which the ROBDD should be evaluated
IncorrectUseException
- if the assignment and the
ROBDD are from a different context
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |