|
||||||||||
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.TerminalNode
class TerminalNode
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
.
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 |
---|
int value
Constructor Detail |
---|
TerminalNode(Context context, int t)
Method Detail |
---|
public ROBDD negate()
negate
in class ROBDD
Context
public ROBDD predecessors(ROBDD n)
predecessors
in class ROBDD
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
IncorrectUse
- if contexts do not coincide
InternalError
- if somebody messed up the implementation of this
packageROBDD.predecessors(ROBDD)
,
predecessors(TerminalNode)
,
predecessors(InnerNode)
private ROBDD predecessors(InnerNode n)
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
ROBDD.predecessors(ROBDD)
private ROBDD predecessors(TerminalNode n)
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
ROBDD.predecessors(ROBDD)
public ROBDD predecessors(ROBDD n, ChangeSet changeset)
predecessors
in class ROBDD
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, herechangeset
- the set of variables that may change
IncorrectUse
- if contexts do not coincide
InternalError
- if somebody messed up the implementation of this
packageROBDD.predecessors(ROBDD, ChangeSet)
,
predecessors(TerminalNode, ChangeSet)
,
predecessors(InnerNode, ChangeSet)
private ROBDD predecessors(InnerNode n, ChangeSet changeset)
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, herechangeset
- the set of variables that may change
ROBDD.predecessors(ROBDD, ChangeSet)
private ROBDD predecessors(TerminalNode n, ChangeSet changeset)
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, herechangeset
- the set of variables that may change
ROBDD.predecessors(ROBDD, ChangeSet)
public ROBDD successors(ROBDD n)
successors
in class ROBDD
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
IncorrectUse
- if contexts do not coincide
InternalError
- if somebody messed up the implementation of this
packageROBDD.successors(ROBDD)
,
successors(InnerNode)
,
successors(TerminalNode)
public ROBDD successors(InnerNode n)
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
ROBDD.successors(ROBDD)
private ROBDD successors(TerminalNode n)
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
ROBDD.successors(ROBDD)
public ROBDD successors(ROBDD n, ChangeSet changeset)
successors
in class ROBDD
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
variablepublic ROBDD successors(InnerNode n, ChangeSet changeset)
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, herechangeset
- variables that may change in the transition
relation
ROBDD.successors(ROBDD)
private ROBDD successors(TerminalNode n, ChangeSet changeset)
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, herechangeset
- variables that may change in the transition
relation
ROBDD.successors(ROBDD)
public boolean isValid()
isValid
in class ROBDD
public Assignment getAssignment()
getAssignment
in class ROBDD
ROBDD.getAssignment()
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
is immediately 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
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |