|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectde.upb.swt.mcie.robdds.ROBDD
public abstract class ROBDD
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.
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
Constructor Detail |
---|
public ROBDD()
Method Detail |
---|
public abstract ROBDD negate()
public abstract ROBDD predecessors(ROBDD 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 packagepublic abstract ROBDD predecessors(ROBDD n, ChangeSet changeset)
n
- the ROBDD representing the set for which the
predecessors should be computed; this ROBDD must
not refer to primed variableschangeset
- set of variables that may change in the transition
relation; all other variables are not changed
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 packagepublic abstract ROBDD successors(ROBDD n)
n
- the ROBDD representing the set for which the successors
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 packagepublic abstract ROBDD successors(ROBDD n, ChangeSet changeset)
n
- the ROBDD representing the set for which the successors
should be computed; this ROBDD must not refer to primed
variableschangeset
- set of variables that may change in the transition
relation; all other variables are not changed
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 packagepublic abstract boolean isValid()
public abstract Assignment getAssignment()
public abstract ROBDD relProd(ROBDD n)
This method is not fully tested yet!
n
- the set second relation
public abstract 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.
ass
- for which the ROBDD should be evaluated
IncorrectUseException
- if the assignment is from
a context different from the context of the ROBDD
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |