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

Packages that use SMVModule

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.mc.tl
edu.wis.jtlv.old_lib.mc	The old library containing model checking algorithms.

Uses of SMVModule in edu.wis.jtlv.env

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

boolean	Env.JTLVBDDToString.domain_has_module_value(SMVModule m, BDDDomain dom, java.lang.String value)
java.math.BigInteger	Env.JTLVBDDToString.get_module_value_loc(SMVModule m, BDDDomain dom, java.lang.String value)
void	Env.JTLVBDDToString.register_domain_module_values(SMVModule m, BDDDomain dom, int range_start, int range_size)
void	Env.JTLVBDDToString.register_domain_module_values(SMVModule m, BDDDomain dom, java.lang.String[] values)

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

Methods in edu.wis.jtlv.env.module that return SMVModule

SMVModule[]	SMVModule.getAllInstances() Getter for all instances declared in this module.
SMVModule[]	SMVModule.getAllInstances(SMVModule.SyncStatus status) Getter for all synchronous or asynchronous instances declared in this module.
SMVModule	ModuleParamHolder.getForInstance() Getter for the module to which this parameter belongs to.
SMVModule	SMVModule.getHolder() Getter for the module instance holds this instance.
SMVModule	ModuleParamHolder.getInstance() The module this pointer points to, if this is not a module, then null is returned.
SMVModule	SMVModule.getInstance(java.lang.String addr, boolean look_hard) Get the instances with the given name.
SMVModule[]	ModuleParamHolder.getInstanceArray() The module array this pointer points to, if this is not a module array, then null is returned.
SMVModule[]	SMVModule.getInstanceArray(java.lang.String addr, boolean look_hard) Get the array of instances with the given name.

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

void	SMVModule.addInstanceVar(SMVModule inner, boolean is_sync) Add a module instance as a variable to this module.
void	SMVModule.removeInstanceVar(SMVModule inner) Removes and inner composed module.

Constructors in edu.wis.jtlv.env.module with parameters of type SMVModule

ModuleParamHolder(SMVModule a_for_instance, java.lang.String a_local_name, java.lang.String an_init_string)
The constructor takes as arguments the instance to which he is parameter to, its local name in that instance, and its instantiating (unparsed) string.

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

Methods in edu.wis.jtlv.lib.mc.tl that return SMVModule

SMVModule

LTLTester.getTester() Getter for the tester which where constructed from this specification.

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

LTLValidAlg(SMVModule design, Spec property)
A constructor for checking a property on a design.

Uses of SMVModule in edu.wis.jtlv.old_lib.mc

Methods in edu.wis.jtlv.old_lib.mc that return SMVModule

SMVModule	ModelChecker.getDesign()
SMVModule	LTLModelChecker.LTLTesterBuilder.getTester()

Methods in edu.wis.jtlv.old_lib.mc with parameters of type SMVModule

void	LTLModelChecker.modelCheckTester(SMVModule user_tester) To compose a tester with the design, and perform model checking.
void	LTLModelChecker.modelCheckTesterStandardOutput(SMVModule user_tester) To compose a tester with the design, and perform model checking.

Constructors in edu.wis.jtlv.old_lib.mc with parameters of type SMVModule

CTLModelChecker(SMVModule design)

CTLModelChecker(SMVModule design, boolean removeRunningVar)

LTLModelChecker(SMVModule design)

LTLModelChecker(SMVModule design, boolean removeRunningVar)

ModelChecker(SMVModule design, boolean removeRunningVar)

SimpleModelChecker(SMVModule design)

SimpleModelChecker(SMVModule design, boolean removeRunningVar)