edu.wis.jtlv.env
Class Env

java.lang.Object
  edu.wis.jtlv.env.Env

public final class Env
extends java.lang.Object

The main JTLV environment Facade, which supplies all API to basic functionalities through delegators to the private internal managers. The environment is somewhat corresponding to the java "System" environment.

The two main field which Env is delegating with are: The JTLVBDDManager, which is responsible of communicating with the actual BDD implementation (through JavaBDD package). The JTLVBDDManagerPairing, which is responsible of all BDD naming and coupling operations (i.e. prime and unprime versions of all fields).

Version:

"1.2.0"

Author:

yaniv sa'ar.

Nested Class Summary

static class

Env.JTLVBDDToString TBD.

Field Summary

static java.util.LinkedList<ErrorListener>	all_error_listeners A list of all error listeners which are invoked on any kind of error in the system.
static Env.JTLVBDDToString	stringer An object responsible for associating BDD variables to their names.
static java.lang.String	version JTLV version count.

Method Summary

static net.sf.javabdd.BDD	allPred(net.sf.javabdd.BDD trans, net.sf.javabdd.BDD to) Given a set of state and a transitions, this procedure return all states which can lead in any number of steps to these states.
static net.sf.javabdd.BDD	allSucc(net.sf.javabdd.BDD trans, net.sf.javabdd.BDD from) Given a set of state and a transitions, this procedure return all states which can be reached in a any number of steps from these states.
static int	assignDedicatedBDDManagerIdx(JTLVThread new_thread) A procedure called from within JTLVThread which allocates and assign a manager to the given thread.
static void	beQuiet() Turning off the garbage collection verbosity.
static void	clearErrorListener() Clears the entire listeners queue.
static boolean	containPrimeVars(net.sf.javabdd.BDD set) Check whether the given BDD contains prime version of the fields.
static boolean	containUnprimeVars(net.sf.javabdd.BDD set) Check whether the given BDD contains unprime version of the fields.
static net.sf.javabdd.BDD	copyBDDIntoBaseManager(net.sf.javabdd.BDD b) Copy any given BDD into the base BDD manager.
static net.sf.javabdd.BDD	copyBDDIntoManager(int idx, net.sf.javabdd.BDD b) Copy any given BDD into the a given BDD manager.
static net.sf.javabdd.BDDVarSet	copyBDDVarSetIntoBaseManager(net.sf.javabdd.BDDVarSet b) Copy any given BDDVarSet into the base BDD manager.
static net.sf.javabdd.BDDVarSet	copyBDDVarSetIntoManager(int idx, net.sf.javabdd.BDDVarSet b) Copy any given BDDVarSet into the a given BDD manager.
static Module[]	debugParseModule(java.lang.String filename) This procedure parse the given file, add it to the system, and pops a window browser with the parsing tree which the parser read.
static void	doError(java.lang.Exception e, java.lang.String msg) Invoke the listeners queue with the given exception.
static void	doOnGC(java.lang.reflect.Method m_gc) Register a procedure to be done at every garbage collection.
static void	doOnResize(java.lang.reflect.Method m_resize) Register a procedure to be done at every resize to the BDD table.
static net.sf.javabdd.BDD	FALSE() The constant FALSE BDD.
static Module[]	getAllModules() Get all module objects currently loaded into the environment.
static int	getCurrentThreadManagerIdx() Get the current running thread BDD manager index.
static net.sf.javabdd.BDDVarSet	getEmptySet() The empty set of fields.
static java.lang.String	getFactoryName() The factory package which is currently used by the environment to allocate new BDD fields.
static Module	getModule(java.lang.String full_inst_name) Get a module instance by its associated full path string.
static java.util.Set<java.lang.String>	getModuleNames() The set of all names which are associated with the modules loaded to the environment.
static int	getModuleNum() Get the number of modules currently loaded into the environment.
static int	getThreadPoolSize() The number of BDD managers in this environment.
static ModuleBDDField	getVar(java.lang.String preface, java.lang.String name) Search and retrieve the BDD field by the given path and field name.
static net.sf.javabdd.BDDVarSet	globalPrimeVars() Get all primed variables in the system.
static net.sf.javabdd.BDDVarSet	globalPrimeVarsMinus(net.sf.javabdd.BDDVarSet primeMinus)
static net.sf.javabdd.BDDVarSet	globalUnprimeVars() Get all unprimed variables in the system.
static net.sf.javabdd.BDDVarSet	globalUnprimeVarsMinus(net.sf.javabdd.BDDVarSet unprimeMinus)
static net.sf.javabdd.BDDVarSet	globalVarsMinus(net.sf.javabdd.BDDVarSet minus)
static net.sf.javabdd.BDDVarSet	intersect(net.sf.javabdd.BDDVarSet a, net.sf.javabdd.BDDVarSet b)
static net.sf.javabdd.BDD	loadBDD(java.lang.String filename) Load a BDD from the file system.
static Module[]	loadModule(java.lang.String filename) The main procedure for loading a given file into the system.
static Spec[]	loadSpecFile(java.lang.String filename) Load any kind of specification from a file.
static Spec[]	loadSpecInputStream(java.io.InputStream is) Load any kind of specification from a given input stream.
static Spec[]	loadSpecString(java.lang.String to_parse) Load any kind of specification from a string.
static ModuleBDDField	newVar(java.lang.String preface, java.lang.String name) Create and allocate a new BDD FIELD with 2 values domain.
static ModuleBDDField	newVar(java.lang.String preface, java.lang.String name, int values_size) Create and allocate a new BDD FIELD with the given domain size, i.e.
static void	NOP() An empty procedure for shutting down the Garbage collection verbosity.
static Module[]	parseModule(java.lang.String filename) This procedure only parse the given file and add it to the system.
static net.sf.javabdd.BDD	pred(net.sf.javabdd.BDD trans, net.sf.javabdd.BDD to) Given a set of state and a transitions, this procedure return all states which can lead in a single step to these states.
static net.sf.javabdd.BDD	prime(net.sf.javabdd.BDD unp_bdd) Given an unprimed BDD, returns the exact same BDD with the primed version of the variables.
static net.sf.javabdd.BDD	prime(net.sf.javabdd.BDD unp_bdd, ModuleBDDField[] couples) Given a BDD, returns the exact same BDD with the primed version of the given fields array.
static void	putModule(java.lang.String full_inst_name, Module to_add) Add a new module to the collection of all modules, and associate it with the given string.
static boolean	registerErrorListener(ErrorListener lis) Register an error listener to be invoked on every error which is thrown in the JTLV environment.
static boolean	removeErrorListener(ErrorListener lis) Remove an error listener from the queue of listeners.
static void	resetEnv() Reset the environment.
static void	saveBDD(java.lang.String filename, net.sf.javabdd.BDD to_save) Save a BDD to the file system.
static net.sf.javabdd.BDD	succ(net.sf.javabdd.BDD trans, net.sf.javabdd.BDD from) Given a set of state and a transitions, this procedure return all states which can be reached in a single step from these states.
static java.lang.String	toNiceSignleLineString(net.sf.javabdd.BDD b)
static java.lang.String	toNiceSignleLineString(Module con, net.sf.javabdd.BDD b) Prepare a string representing the If-Then-Else form of the given BDD.
static java.lang.String	toNiceString(net.sf.javabdd.BDD b)
static java.lang.String	toNiceString(net.sf.javabdd.BDD b, java.lang.String startIndent)
static java.lang.String	toNiceString(Module con, net.sf.javabdd.BDD b) Prepare a string representing the If-Then-Else form of the given BDD.
static java.lang.String	toNiceString(Module con, net.sf.javabdd.BDD b, java.lang.String startIndent) Prepare a string representing the If-Then-Else form of the given BDD.
static net.sf.javabdd.BDD	TRUE() The constant TRUE BDD.
static net.sf.javabdd.BDD	unprime(net.sf.javabdd.BDD p_bdd) Given a primed BDD, returns the exact same BDD with the unprimed version of the fields.
static net.sf.javabdd.BDD	unprime(net.sf.javabdd.BDD p_bdd, ModuleBDDField[] couples) Given a BDD, returns the exact same BDD with the unprimed version of the given fields array.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

version

public static final java.lang.String version

JTLV version count.

See Also:

Constant Field Values

stringer

public static Env.JTLVBDDToString stringer

An object responsible for associating BDD variables to their names.

all_error_listeners

public static java.util.LinkedList<ErrorListener> all_error_listeners

A list of all error listeners which are invoked on any kind of error in the system.

See Also:

registerErrorListener(ErrorListener), removeErrorListener(ErrorListener), clearErrorListener(), activateErrorListeners(Exception, String), doError(Exception, String), ErrorListener

Method Detail

resetEnv

public static void resetEnv()

Reset the environment. In particular reset the bdd factory and all fields declared in the environment.

getThreadPoolSize

public static int getThreadPoolSize()

The number of BDD managers in this environment. The number is set by the System.property key "pool_size" (plus one additional manager to the main thread) during the time of the last reset.

Returns:

The number of BDD managers.

See Also:

JTLVThread

assignDedicatedBDDManagerIdx

public static int assignDedicatedBDDManagerIdx(JTLVThread new_thread)

A procedure called from within JTLVThread which allocates and assign a manager to the given thread. Be aware that instantiating and assigning more JTLVThread then the number of managers, will lock this thread until a manager will be freed. (e.g. might lead to a deadlock.)

Parameters:

new_thread - The thread to assign a manager to.

Returns:

The index manager assigned to the given thread.

See Also:

JTLVThread, getThreadPoolSize()

getCurrentThreadManagerIdx

public static int getCurrentThreadManagerIdx()

Get the current running thread BDD manager index.

Returns:

The current running thread BDD manager index.

See Also:

JTLVThread.getDedicatedBDDManagerIdx()

copyBDDIntoBaseManager

public static net.sf.javabdd.BDD copyBDDIntoBaseManager(net.sf.javabdd.BDD b)

Copy any given BDD into the base BDD manager.

Parameters:

b - The BDD to copy.

Returns:

The new identical BDD in the base BDD manager.

See Also:

JTLVThread.adjustBDDToBase(BDD), JTLVThread.adjustBDDToManager(BDD)

copyBDDIntoManager

public static net.sf.javabdd.BDD copyBDDIntoManager(int idx,
                                                    net.sf.javabdd.BDD b)

Copy any given BDD into the a given BDD manager.

Parameters:

idx - The given BDD manager index.

b - The BDD to copy.

Returns:

The new identical BDD in the given BDD manager.

See Also:

JTLVThread.adjustBDDToBase(BDD), JTLVThread.adjustBDDToManager(BDD)

copyBDDVarSetIntoBaseManager

public static net.sf.javabdd.BDDVarSet copyBDDVarSetIntoBaseManager(net.sf.javabdd.BDDVarSet b)

Copy any given BDDVarSet into the base BDD manager.

Parameters:

b - The BDDVarSet to copy.

Returns:

The new identical BDDVarSet in the base BDD manager.

See Also:

JTLVThread.adjustBDDVarSetToBase(BDDVarSet), JTLVThread.adjustBDDVarSetToManager(BDDVarSet)

copyBDDVarSetIntoManager

public static net.sf.javabdd.BDDVarSet copyBDDVarSetIntoManager(int idx,
                                                                net.sf.javabdd.BDDVarSet b)

Copy any given BDDVarSet into the a given BDD manager.

Parameters:

idx - The given BDD manager index.

b - The BDDVarSet to copy.

Returns:

The new identical BDDVarSet in the given BDD manager.

See Also:

JTLVThread.adjustBDDVarSetToBase(BDDVarSet), JTLVThread.adjustBDDVarSetToManager(BDDVarSet)

getAllModules

public static Module[] getAllModules()

Get all module objects currently loaded into the environment.

Returns:

an array of modules.

See Also:

putModule(String, Module), getModule(String), Module, FDSModule, SMVModule

getModule

public static Module getModule(java.lang.String full_inst_name)

Get a module instance by its associated full path string.

Parameters:

full_inst_name - the full path string to the instance.

Returns:

the module object or null if not existing.

See Also:

putModule(String, Module), getAllModules(), Module, FDSModule, SMVModule

putModule

public static void putModule(java.lang.String full_inst_name,
                             Module to_add)

Add a new module to the collection of all modules, and associate it with the given string.

Parameters:

full_inst_name - the string to associate this module with.

to_add - the module to add.

See Also:

getAllModules(), getModule(String), Module, FDSModule, SMVModule

getModuleNum

public static int getModuleNum()

Get the number of modules currently loaded into the environment.

Returns:

The number of modules currently loaded into the environment.

getModuleNames

public static java.util.Set<java.lang.String> getModuleNames()

The set of all names which are associated with the modules loaded to the environment.

Returns:

The set of all names.

See Also:

getAllModules(), getModule(String)

loadSpecInputStream

public static Spec[] loadSpecInputStream(java.io.InputStream is)
                                  throws java.io.IOException

Load any kind of specification from a given input stream.

Parameters:

is - The input stream to parse.

Returns:

An array of Specifications.

Throws:

java.io.IOException

See Also:

loadSpecString(String), loadSpecFile(String)

loadSpecString

public static Spec[] loadSpecString(java.lang.String to_parse)

Load any kind of specification from a string.

Parameters:

to_parse - The string to parse.

Returns:

An array of Specifications.

See Also:

loadSpecInputStream(InputStream), loadSpecFile(String)

loadSpecFile

public static Spec[] loadSpecFile(java.lang.String filename)
                           throws java.io.IOException

Load any kind of specification from a file.

Parameters:

filename - The file to load from.

Returns:

An array of Specifications.

Throws:

java.io.IOException - When there where problems reading the file.

See Also:

loadSpecInputStream(InputStream), loadSpecString(String)

loadModule

public static Module[] loadModule(java.lang.String filename)
                           throws java.io.IOException

The main procedure for loading a given file into the system. Currently two file extensions are supported, *.fds an *.smv. The procedure will load according to the file extension. The modules loaded are returned. Alternatively, The modules can also be found through the modules facilities here: getAllModules() or getModule(String).

All paring and interpreting exceptions are thrown through the Env error mechanism. (i.e. registerErrorListener(ErrorListener) activateErrorListeners(Exception, String) doError(Exception, String))

Parameters:

filename - The file to load with file extension *.fds, or *.smv .

Returns:

Array of module which were loaded from the given file.

Throws:

java.io.IOException - If there was a problem with the file.

See Also:

parseModule(String), debugParseModule(String), getAllModules(), getModule(String), registerErrorListener(ErrorListener), activateErrorListeners(Exception, String), doError(Exception, String)

parseModule

public static Module[] parseModule(java.lang.String filename)
                            throws java.io.IOException

This procedure only parse the given file and add it to the system. Currently two file extensions are supported, *.fds an *.smv. The procedure will parse according to the file extension. The modules parsed are returned. (BUT NOT FILLED WITH THEIR VARIABLES AND STATEMENT, SINCE THIS IS DONE IN THE INTERPRETATION STAGE.) Alternatively, The modules can also be found through the modules facilities here: getAllModules() or getModule(String).

All paring and interpreting exceptions are thrown through the Env error mechanism. (i.e. registerErrorListener(ErrorListener) activateErrorListeners(Exception, String) doError(Exception, String))

Parameters:

filename - The file to load with file extension *.fds, or *.smv .

Returns:

Array of module which were loaded from the given file.

Throws:

java.io.IOException - If there was a problem with the file.

See Also:

loadModule(String), debugParseModule(String), getAllModules(), getModule(String), registerErrorListener(ErrorListener), activateErrorListeners(Exception, String), doError(Exception, String)

debugParseModule

public static Module[] debugParseModule(java.lang.String filename)
                                 throws java.io.IOException

This procedure parse the given file, add it to the system, and pops a window browser with the parsing tree which the parser read. Currently two file extensions are supported, *.fds an *.smv. The procedure will parse according to the file extension. The modules parsed are returned. (BUT NOT FILLED WITH THEIR VARIABLES AND STATEMENT, SINCE THIS IS DONE IN THE INTERPRETATION STAGE.) Alternatively, The modules can also be found through the modules facilities here: getAllModules() or getModule(String).

All paring and interpreting exceptions are thrown through the Env error mechanism. (i.e. registerErrorListener(ErrorListener) activateErrorListeners(Exception, String) doError(Exception, String))

Parameters:

filename - The file to load with file extension *.fds, or *.smv .

Returns:

Array of module which were loaded from the given file.

Throws:

java.io.IOException - If there was a problem with the file.

See Also:

loadModule(String), parseModule(String), getAllModules(), getModule(String), registerErrorListener(ErrorListener), activateErrorListeners(Exception, String), doError(Exception, String)

getFactoryName

public static java.lang.String getFactoryName()

The factory package which is currently used by the environment to allocate new BDD fields.

Returns:

The BDD factory name.

doOnGC

public static void doOnGC(java.lang.reflect.Method m_gc)

Register a procedure to be done at every garbage collection.

Parameters:

m_gc - The method to perform.

See Also:

beQuiet(), doOnResize(Method)

doOnResize

public static void doOnResize(java.lang.reflect.Method m_resize)

Register a procedure to be done at every resize to the BDD table.

Parameters:

m_resize - The method to perform.

See Also:

beQuiet(), doOnGC(Method)

beQuiet

public static void beQuiet()

Turning off the garbage collection verbosity.

See Also:

doOnGC(Method), doOnResize(Method)

NOP

public static void NOP()

An empty procedure for shutting down the Garbage collection verbosity.

FALSE

public static net.sf.javabdd.BDD FALSE()

The constant FALSE BDD.

Returns:

The constant FALSE BDD.

See Also:

TRUE()

TRUE

public static net.sf.javabdd.BDD TRUE()

The constant TRUE BDD.

Returns:

The constant TRUE BDD.

See Also:

FALSE()

saveBDD

public static void saveBDD(java.lang.String filename,
                           net.sf.javabdd.BDD to_save)
                    throws java.io.IOException

Save a BDD to the file system.

Parameters:

filename - The file to save the BDD to.

to_save - The BDD to save.

Throws:

java.io.IOException - If the was a problem with creating the file.

See Also:

loadBDD(String)

loadBDD

public static net.sf.javabdd.BDD loadBDD(java.lang.String filename)
                                  throws java.io.IOException

Load a BDD from the file system.

Make sure that the system is configured with the same BDD package which saved the BDD to the file!!

Parameters:

filename - The file to load the BDD from.

Returns:

The BDD which was loaded.

Throws:

java.io.IOException - If the was a problem with reading the file.

See Also:

saveBDD(String, BDD)

toNiceString

public static java.lang.String toNiceString(Module con,
                                            net.sf.javabdd.BDD b)

Prepare a string representing the If-Then-Else form of the given BDD. This kind of printing is better by an order of magnitude with respect to simple BDD.toString, which is exponential to the size of the BDD.
The naming is done respective to the given module, i.e. the path leading to the variable from the given module.
The print is done with line indentation.

It is advise to use this procedure for printing big BDDs!!

Parameters:

con - The module context of the BDD.

b - The BDD to prepare string to.

Returns:

The string representing the BDD.

See Also:

toNiceString(Module, BDD, String), toNiceSignleLineString(Module, BDD)

toNiceString

public static java.lang.String toNiceString(net.sf.javabdd.BDD b)

toNiceString

public static java.lang.String toNiceString(Module con,
                                            net.sf.javabdd.BDD b,
                                            java.lang.String startIndent)

Prepare a string representing the If-Then-Else form of the given BDD. This kind of printing is better by an order of magnitude with respect to simple BDD.toString, which is exponential to the size of the BDD.
The naming is done respective to the given module, i.e. the path leading to the variable from the given module.
The print is done with line indentation starting with the given initial indentation.

It is advise to use this procedure for printing big BDDs!!

Parameters:

con - The module context of the BDD.

b - The BDD to prepare string to.

startIndent - The initial indentation.

Returns:

The string representing the BDD.

See Also:

toNiceString(Module, BDD), toNiceSignleLineString(Module, BDD)

toNiceString

public static java.lang.String toNiceString(net.sf.javabdd.BDD b,
                                            java.lang.String startIndent)

toNiceSignleLineString

public static java.lang.String toNiceSignleLineString(Module con,
                                                      net.sf.javabdd.BDD b)

Prepare a string representing the If-Then-Else form of the given BDD. This kind of printing is better by an order of magnitude with respect to simple BDD.toString, which is exponential to the size of the BDD.
The naming is done respective to the given module, i.e. the path leading to the variable from the given module.
The print is done in a single line.

It is advise to use this procedure for printing big BDDs!!

Parameters:

con - The module context of the BDD.

b - The BDD to prepare string to.

Returns:

The string representing the BDD.

See Also:

toNiceString(Module, BDD), toNiceString(Module, BDD, String)

toNiceSignleLineString

public static java.lang.String toNiceSignleLineString(net.sf.javabdd.BDD b)

getVar

public static ModuleBDDField getVar(java.lang.String preface,
                                    java.lang.String name)

Search and retrieve the BDD field by the given path and field name.

Parameters:

preface - The path to the field.

name - The field name.

Returns:

The BDD field, null if not found.

newVar

public static ModuleBDDField newVar(java.lang.String preface,
                                    java.lang.String name,
                                    int values_size)
                             throws ModuleVariableException

Create and allocate a new BDD FIELD with the given domain size, i.e. the domain size is exponential to the actual BDD size.

With this field instantiation The BDD is created with an associated facilities in the environment.
For creating a BDD without the environment field facilities, please refer to allocBDD(int, int).

Parameters:

preface - The path to the field.

name - The field name.

values_size - The size of the domain.

Returns:

The newly created BDD field.

Throws:

ModuleVariableException - If the given name for the new field to create is illegal.

See Also:

newVar(String, String), allocBDD(int, int)

newVar

public static ModuleBDDField newVar(java.lang.String preface,
                                    java.lang.String name)
                             throws ModuleVariableException

Create and allocate a new BDD FIELD with 2 values domain.

With this field instantiation The BDD is created with an associated facilities in the environment.
For creating a BDD without the environment field facilities, please refer to allocBDD(int,int).

Parameters:

preface - The path to the field.

name - The field name.

Returns:

The newly created BDD couple variable.

Throws:

ModuleVariableException - If the given name for the new field to create is illegal.

See Also:

newVar(String, String, int), allocBDD(int, int)

globalPrimeVars

public static net.sf.javabdd.BDDVarSet globalPrimeVars()

Get all primed variables in the system.

Returns:

All primed variables in the system.

globalUnprimeVars

public static net.sf.javabdd.BDDVarSet globalUnprimeVars()

Get all unprimed variables in the system.

Returns:

All unprimed variables in the system.

globalPrimeVarsMinus

public static net.sf.javabdd.BDDVarSet globalPrimeVarsMinus(net.sf.javabdd.BDDVarSet primeMinus)

globalUnprimeVarsMinus

public static net.sf.javabdd.BDDVarSet globalUnprimeVarsMinus(net.sf.javabdd.BDDVarSet unprimeMinus)

globalVarsMinus

public static net.sf.javabdd.BDDVarSet globalVarsMinus(net.sf.javabdd.BDDVarSet minus)

pred

public static net.sf.javabdd.BDD pred(net.sf.javabdd.BDD trans,
                                      net.sf.javabdd.BDD to)
                               throws net.sf.javabdd.BDDException

Given a set of state and a transitions, this procedure return all states which can lead in a single step to these states.

Parameters:

trans - The given transitions.

to - The set of state to be reach.

Returns:

The set of states which can lead in a single step to the given states.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

allPred(BDD, BDD), allSucc(BDD, BDD), succ(BDD, BDD)

succ

public static net.sf.javabdd.BDD succ(net.sf.javabdd.BDD trans,
                                      net.sf.javabdd.BDD from)
                               throws net.sf.javabdd.BDDException

Given a set of state and a transitions, this procedure return all states which can be reached in a single step from these states.

Parameters:

trans - The given transitions.

from - The given set of state.

Returns:

The set of states which can be reached in a single step from the given states.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

allPred(BDD, BDD), allSucc(BDD, BDD), pred(BDD, BDD)

allPred

public static net.sf.javabdd.BDD allPred(net.sf.javabdd.BDD trans,
                                         net.sf.javabdd.BDD to)
                                  throws net.sf.javabdd.BDDException

Given a set of state and a transitions, this procedure return all states which can lead in any number of steps to these states.

Parameters:

trans - The given transitions.

to - The set of state to be reach.

Returns:

The set of states which can lead in any number of steps to the given states.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

pred(BDD, BDD), allSucc(BDD, BDD), succ(BDD, BDD)

allSucc

public static net.sf.javabdd.BDD allSucc(net.sf.javabdd.BDD trans,
                                         net.sf.javabdd.BDD from)
                                  throws net.sf.javabdd.BDDException

Given a set of state and a transitions, this procedure return all states which can be reached in a any number of steps from these states.

Parameters:

trans - The given transitions.

from - The given set of state.

Returns:

The set of states which can be reached in any number of steps from the given states.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

allPred(BDD, BDD), succ(BDD, BDD), pred(BDD, BDD)

prime

public static net.sf.javabdd.BDD prime(net.sf.javabdd.BDD unp_bdd)
                                throws net.sf.javabdd.BDDException

Given an unprimed BDD, returns the exact same BDD with the primed version of the variables.

Parameters:

unp_bdd - The unprimed BDD.

Returns:

The primed version of the given BDD.

Throws:

net.sf.javabdd.BDDException - When trying to prime BDD with primed fields.

See Also:

prime(BDD, ModuleBDDField[]), unprime(BDD), unprime(BDD, ModuleBDDField[])

prime

public static net.sf.javabdd.BDD prime(net.sf.javabdd.BDD unp_bdd,
                                       ModuleBDDField[] couples)
                                throws net.sf.javabdd.BDDException

Given a BDD, returns the exact same BDD with the primed version of the given fields array.

Parameters:

unp_bdd - The given BDD.

couples - The fields to prime.

Returns:

A BDD with primed version of the given fields.

Throws:

net.sf.javabdd.BDDException - When trying to prime already primed fields.

See Also:

prime(BDD), unprime(BDD), unprime(BDD, ModuleBDDField[])

unprime

public static net.sf.javabdd.BDD unprime(net.sf.javabdd.BDD p_bdd)
                                  throws net.sf.javabdd.BDDException

Given a primed BDD, returns the exact same BDD with the unprimed version of the fields.

Parameters:

p_bdd - The primed BDD.

Returns:

The unprimed version of the given BDD.

Throws:

net.sf.javabdd.BDDException - When trying to unprime BDD with unprime fields.

See Also:

prime(BDD), prime(BDD, ModuleBDDField[]), unprime(BDD, ModuleBDDField[])

unprime

public static net.sf.javabdd.BDD unprime(net.sf.javabdd.BDD p_bdd,
                                         ModuleBDDField[] couples)
                                  throws net.sf.javabdd.BDDException

Given a BDD, returns the exact same BDD with the unprimed version of the given fields array.

Parameters:

p_bdd - The given BDD.

couples - The fields to unprime.

Returns:

A BDD with unprimed version of the given fields.

Throws:

net.sf.javabdd.BDDException - When trying to unprime already unprimed fields.

See Also:

prime(BDD), prime(BDD, ModuleBDDField[]), unprime(BDD)

containPrimeVars

public static boolean containPrimeVars(net.sf.javabdd.BDD set)

Check whether the given BDD contains prime version of the fields.

Parameters:

set - The BDD to check.

Returns:

true if the given BDD contains prime version of the fields, false otherwise.

containUnprimeVars

public static boolean containUnprimeVars(net.sf.javabdd.BDD set)

Check whether the given BDD contains unprime version of the fields.

Parameters:

set - The BDD to check.

Returns:

true if the given BDD contains unprime version of the variables, false otherwise.

getEmptySet

public static net.sf.javabdd.BDDVarSet getEmptySet()

The empty set of fields.

Returns:

The empty set of fields.

intersect

public static net.sf.javabdd.BDDVarSet intersect(net.sf.javabdd.BDDVarSet a,
                                                 net.sf.javabdd.BDDVarSet b)

registerErrorListener

public static boolean registerErrorListener(ErrorListener lis)

Register an error listener to be invoked on every error which is thrown in the JTLV environment.

Parameters:

lis - The new listener to add.

Returns:

true if the listeners queue has been changed.

See Also:

all_error_listeners, removeErrorListener(ErrorListener), clearErrorListener(), activateErrorListeners(Exception, String), doError(Exception, String), ErrorListener

removeErrorListener

public static boolean removeErrorListener(ErrorListener lis)

Remove an error listener from the queue of listeners.

Parameters:

lis - The listener to be removed.

Returns:

true if the listeners queue contained the specified element.

See Also:

all_error_listeners, registerErrorListener(ErrorListener), clearErrorListener(), activateErrorListeners(Exception, String), doError(Exception, String), ErrorListener

clearErrorListener

public static void clearErrorListener()

Clears the entire listeners queue.

See Also:

all_error_listeners, registerErrorListener(ErrorListener), removeErrorListener(ErrorListener), activateErrorListeners(Exception, String), doError(Exception, String), ErrorListener

doError

public static void doError(java.lang.Exception e,
                           java.lang.String msg)

Invoke the listeners queue with the given exception. This is the exact same procedure as activateErrorListeners(Exception, String)

Parameters:

e - The exception to invoke the listeners with.

msg - A text message describing the failure.

See Also:

all_error_listeners, registerErrorListener(ErrorListener), removeErrorListener(ErrorListener), clearErrorListener(), activateErrorListeners(Exception, String), ErrorListener