Uses of Class
edu.wis.jtlv.env.module.Module

Packages that use Module

edu.wis.jtlv.env	The main package of JTLV, most creational action are usually done through static procedures in object Env.
edu.wis.jtlv.env.module	All User interface to FDS and SMV modules.

Uses of Module in edu.wis.jtlv.env

Methods in edu.wis.jtlv.env that return Module

static Module[]	Env.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 Module[]	Env.getAllModules() Get all module objects currently loaded into the environment.
static Module	Env.getModule(java.lang.String full_inst_name) Get a module instance by its associated full path string.
static Module[]	Env.loadModule(java.lang.String filename) The main procedure for loading a given file into the system.
static Module[]	Env.parseModule(java.lang.String filename) This procedure only parse the given file and add it to the system.

Methods in edu.wis.jtlv.env with parameters of type Module

static void	Env.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 java.lang.String	Env.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	Env.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	Env.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.

Uses of Module in edu.wis.jtlv.env.module

Subclasses of Module in edu.wis.jtlv.env.module

class	FDSModule An object which represent an FDS module.
class	ModuleWithStrongFairness A general interface for module with strong fairness (compassion). I.e.
class	ModuleWithWeakFairness A general interface for module with weak fairness (justice). I.e.
class	SMVModule An object which represent an SMV module.

Methods in edu.wis.jtlv.env.module with parameters of type Module

net.sf.javabdd.BDD	Module.controlStates(Module responder, net.sf.javabdd.BDD to) A state s is included in the returning result if the this module can force the responder to reach a state in "to".
net.sf.javabdd.BDD	Module.yieldStates(Module responder, net.sf.javabdd.BDD to) A state s in included in the returning result if responder module can force this module to reach a state in "to". That is, regardless of how this module will move from the result, the responder module can choose an appropriate move into "to".