de.upb.swt.mcie.robdds
Class Context

java.lang.Object
  extended by de.upb.swt.mcie.robdds.Context

public class Context
extends java.lang.Object

Implements the context for an ROBDD, which comprises the set of variables and the order on these variables. In addition, the context maintains all hash tables for ROBBDs and its operations.

This class provides a public method createVariable, which can be used for instantiating new variables in this context. Each variable is assigned a unique number in ascending order. This is the variable order used in ROBDDs as defined in package robdds. When a variable is created, the variable as well as its primed version are instantiated (where the unprimed version is created first).

From outside this package, variables can only be generated by method createVariable, which returns the unprimed version. The corresponding primed version can be obtained by the method Variable.getPartner().

Author:
Ekkart Kindler, kindler@upb.de

Field Summary
 BinOp and
          The and operation in this context.
 BinOp equiv
          The equivalence operation (equality) in this context.
 TerminalNode high
          The (in this context) unique terminal node representing true (1).
 BinOp impl
          The implication operation in this context.
(package private)  java.util.Map innerNodesTable
          This hash table holds references to all existing inner nodes.
 TerminalNode low
          The (in this context) unique terminal node representing false (0).
 BinOp or
          The or operation in this context.
(package private)  java.util.Map predecessorTable
          This table is used during the calculation of the predecessors of a set with respect to a transition relation.
(package private)  java.util.Map relationTable
          This table is used during the calculation of the relation product of two relations.
(package private)  java.util.Map successorTable
          This table is used during the calculation of the successors of a set with respect to a transition relation.
private  int variablesCounter
          The number of variables (primed and unprimed) instantiated so far in this context.
private  java.util.Map variablesTable
          The table keeping track of all variables in this context.
 BinOp xor
          The xor operation in this context.
 
Constructor Summary
Context()
           
 
Method Summary
 void clearHashTables()
          Clears the hash tables of all operations in this context.
(package private)  ROBDD createInnerNode(Variable variable, ROBDD low, ROBDD high)
          Creates the inner node, provided that it is not duplicate and not redundant.
 Variable createVariable(java.lang.String name)
          Creates a pair of new variables for the given name and returns the unprimed version of this pair as a result.
 int getSize()
          Returns the number of internal nodes currently in use.
 Variable getVariable(java.lang.String name)
          For the given name, returns the associated variable, if the variable exists.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

variablesTable

private java.util.Map variablesTable
The table keeping track of all variables in this context.


variablesCounter

private int variablesCounter
The number of variables (primed and unprimed) instantiated so far in this context.


low

public final TerminalNode low
The (in this context) unique terminal node representing false (0).


high

public final TerminalNode high
The (in this context) unique terminal node representing true (1).


innerNodesTable

java.util.Map innerNodesTable
This hash table holds references to all existing inner nodes. This table is necessary for avoiding duplicates of inner nodes (one of the requirements of ROBDDs). But, inner nodes no longer in use can be removed from the table. In order to do this fully automatically, we use WeakHashMaps and WeakReferences in this table. Note that most inner nodes will be referenced from other hash tables too; therefore, garbage collection will be effective only after these tables have been cleared. TODO: Much fine tuning could be done at this point, but this depends on the particular application.

BTW: The other two requirements on ROBDDs, variable order and exclusion of redundant nodes are guaranteed by the implementation of the different algorithms on ROBDDs. The API should be such that these properties cannot be compromised from outside the package.


predecessorTable

java.util.Map predecessorTable
This table is used during the calculation of the predecessors of a set with respect to a transition relation. It significantly improves the efficiency of the computation, by not calculating the result for the same pair of nodes twice. It is not necessary for correctness and can be cleared any time. But, it should be cleared only when necessary (i.e. when the system runs out of memory).


successorTable

java.util.Map successorTable
This table is used during the calculation of the successors of a set with respect to a transition relation. It significantly improves the efficiency of the computation, by not calculating the same operation for a pair of nodes twice. It is not necessary for correctness and can be cleared any time. But, it should be cleared only when necessary (i.e. when the system runs out of memory).


relationTable

java.util.Map relationTable
This table is used during the calculation of the relation product of two relations. It significantly improves the efficiency of the computation, by not calculating the same operation for a pair of nodes twice. It is not necessary for correctness and can be cleared any time. But, it should be cleared only when necessary (i.e. when the system runs out of memory).


and

public final BinOp and
The and operation in this context.


or

public final BinOp or
The or operation in this context.


xor

public final BinOp xor
The xor operation in this context.


equiv

public final BinOp equiv
The equivalence operation (equality) in this context.


impl

public final BinOp impl
The implication operation in this context.

Constructor Detail

Context

public Context()
Method Detail

createVariable

public Variable createVariable(java.lang.String name)
Creates a pair of new variables for the given name and returns the unprimed version of this pair as a result. If the variable exists already, it will not be newly created, but the existing copy is returned. The primed version can be obtained by the method Variable.getPartner(). In principle, the name could contain special characters and symbols other than letters or digits. These variables, however, cannot be parsed, and should be used for special purposes only, when directly generating formulas in the code.

Parameters:
name - the name of the variable
Returns:
the corresponding unprimed variable

getVariable

public Variable getVariable(java.lang.String name)
For the given name, returns the associated variable, if the variable exists. The primed version can be obtained by the method Variable.getPartner(). In principle, the name could contain special characters and symbols other than letters or digits. These variables, however, cannot be parsed, and should be used for special purposes only, when directly generating formulas in the code.

Parameters:
name - a String
Returns:
the variable with the name, if it exists

createInnerNode

ROBDD createInnerNode(Variable variable,
                      ROBDD low,
                      ROBDD high)
Creates the inner node, provided that it is not duplicate and not redundant. When newly created, it is put to the hash table of all inner nodes. The arguments for the successor nodes should not be null; if they are inner nodes, the variables of these nodes must succeed the variable of this node in this context. It is an error, if the context of the variable or the successor nodes are different from the this context.

Parameters:
variable - the variable of this node
low - the successor for 0
high - the successor for 1
Returns:
the inner node
Throws:
IncorrectUseException - if the contexts of the variable and the successor nodes do not coincide
InternalError - if for some reason the requirements of ROBDDs are compromised

getSize

public int getSize()
Returns the number of internal nodes currently in use. Due to the use of WeakHashMap, it returns an upper bound only.

Returns:
number of inner nodes currently in use

clearHashTables

public void clearHashTables()
Clears the hash tables of all operations in this context. This method can be called any time without compromising the correctness. But, calling it can significantly reduce the efficiency of subsequent applications of binary operations. Note that applications could create their own binary operations. This method does NOT clear the hash tables of these binary operations.

See Also:
BinOp.clearHashtable()