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	Package dedicated to the user's modules interface.
edu.wis.jtlv.lib	The main user library, with all published formal algorithm which where implemented through JTLV.
edu.wis.jtlv.lib.games	The library with all games algorithms which where implemented using JTLV.
edu.wis.jtlv.lib.mc	The library containing all implemented model checking algorithms.
edu.wis.jtlv.lib.mc.tl
edu.wis.jtlv.old_lib.games	The old library with games algorithms which where implemented through JTLV.

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) 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) Load a given file into the system without a specified order (i.e.
static Module[]	Env.loadModule(java.lang.String filename, java.lang.String ordfile) Load a given file into the system with a specified order given by the other file.
static Module[]	Env.parseModule(java.lang.String filename) 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, BDD b) Prepare a string representing the If-Then-Else form of the given BDD.
static java.lang.String	Env.toNiceString(Module con, BDD b) Prepare a string representing the If-Then-Else form of the given BDD.
static java.lang.String	Env.toNiceString(Module con, 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

void	SMVModule.asyncComposition(Module inner)
void	FDSModule.asyncComposition(Module inner) This functionality is not implemented for FDSModule yet.
abstract void	Module.asyncComposition(Module inner) add asynchronous composition to this module.
BDD	Module.controlStates(Module responder, 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".
void	SMVModule.decompose(Module inner)
void	FDSModule.decompose(Module inner) This functionality is not implemented for FDSModule yet.
abstract void	Module.decompose(Module inner) remove composition from this module.
void	SMVModule.syncComposition(Module inner)
void	FDSModule.syncComposition(Module inner) This functionality is not implemented for FDSModule yet.
abstract void	Module.syncComposition(Module inner) add synchronous composition to this module.
BDD	Module.yieldStates(Module responder, 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".

Uses of Module in edu.wis.jtlv.lib

Constructors in edu.wis.jtlv.lib with parameters of type Module

AlgResultModule(AlgResultI.ResultStatus fin_status, Module res)
A constructor for a module results, with a general flag is was successful.

AlgResultModule(boolean was_successful, Module res)
A constructor for a module results, with a general flag is was successful.

AlgResultModule(Module res)
A constructor for a module results, without successfulness status.

Uses of Module in edu.wis.jtlv.lib.games

Constructors in edu.wis.jtlv.lib.games with parameters of type Module

GR1GameAlg(Module env, Module sys, GeneralizedReactivePair gr_pair)

RkGameAlg(Module env, Module sys, java.util.Set<ReactivePair> pairs)
A constructor for the R[k] Game and synthesis.

Uses of Module in edu.wis.jtlv.lib.mc

Constructors in edu.wis.jtlv.lib.mc with parameters of type Module

SimpleDeadlockAlg(Module design)
A constructor for the deadlock algorithm.

SimpleInvarianceAlg(Module design, Spec prop)
A constructor for the invariance algorithm.

SimpleTempEntailAlg(Module design, Spec p, Spec q)
A constructor for the temp entailment algorithm.

Uses of Module in edu.wis.jtlv.lib.mc.tl

Constructors in edu.wis.jtlv.lib.mc.tl with parameters of type Module

LTLModelCheckAlg(Module design, Module user_tester)
Constructor for composing a tester with the design, and perform model checking.

LTLModelCheckAlg(Module design, Spec property)
Constructor for a given specification \phi (as a formula in temporal logic) which we want to decide whether \phi is valid over finite state program P, i.e.

Uses of Module in edu.wis.jtlv.old_lib.games

Methods in edu.wis.jtlv.old_lib.games that return Module

Module	RkGame.getEnvPlayer() Getter for the environment player.
Module	RkGame.getSysPlayer() Getter for the system player.

Constructors in edu.wis.jtlv.old_lib.games with parameters of type Module

RkGame(Module env, Module sys, java.util.Set<RkGame.ImplicationEntity> pairs)