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

Packages that use ModuleException

edu.wis.jtlv.env.module

All User interface to FDS and SMV modules.

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

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

class

ModuleVariableException An exception caused by wrong variable naming in a Module.

Methods in edu.wis.jtlv.env.module that throw ModuleException

void	SMVModule.___addDefine(java.lang.String addr) Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
void	SMVModule.___addDefineFromParam(java.lang.String addr) Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
void	SMVModule.___attachParamPointers() Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
void	ModuleParamHolder.___attachPointer() Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
void	SMVModule.addCompassion(net.sf.javabdd.BDD p, net.sf.javabdd.BDD q)
abstract void	ModuleWithStrongFairness.addCompassion(net.sf.javabdd.BDD p, net.sf.javabdd.BDD q) Add strong (compassion) winning condition to the module.
void	SMVModule.addInitial(net.sf.javabdd.BDD to_add)
void	FDSModule.addInitial(net.sf.javabdd.BDD to_add)
abstract void	Module.addInitial(net.sf.javabdd.BDD to_add) Conjunct the initial condition with the given condition.
void	SMVModule.addInstanceVar(SMVModule inner, boolean is_sync) Add a module instance as a variable to this module.
void	SMVModule.addJustice(net.sf.javabdd.BDD to_add)
void	FDSModule.addJustice(net.sf.javabdd.BDD to_add)
abstract void	ModuleWithWeakFairness.addJustice(net.sf.javabdd.BDD to_add) Add weak (justice) winning condition to the module.
ModuleBDDField	SMVModule.addVar(java.lang.String new_var)
ModuleBDDField	FDSModule.addVar(java.lang.String new_var)
abstract ModuleBDDField	Module.addVar(java.lang.String new_var) Add a variable to the module.
ModuleBDDField	SMVModule.addVar(java.lang.String new_var, int range_start, int range_end) Add a range variable to this module.
ModuleBDDField	SMVModule.addVar(java.lang.String new_var, java.lang.String[] val_names) Add a set of values variable to this module.
void	SMVModule.asyncComposition(SMVModule inner)
void	FDSModule.conjunctTrans(net.sf.javabdd.BDD to_add)
abstract void	Module.conjunctTrans(net.sf.javabdd.BDD to_add) Conjunct the transition relation with the given condition.
void	SMVModule.decompose(SMVModule inner)
void	FDSModule.disjunctTrans(net.sf.javabdd.BDD to_add)
abstract void	Module.disjunctTrans(net.sf.javabdd.BDD to_add) Disjunct the transition relation with the given condition.
void	SMVModule.removeInstanceVar(SMVModule inner)
void	SMVModule.setInitial(net.sf.javabdd.BDD to_add)
void	FDSModule.setInitial(net.sf.javabdd.BDD to_add)
abstract void	Module.setInitial(net.sf.javabdd.BDD to_add) Set the initial condition with the given condition.

Constructors in edu.wis.jtlv.env.module that throw ModuleException

SMVModule(edu.wis.jtlv.env.core.smv.schema.SMVModuleInfo a_module_info, java.lang.String player_name, java.lang.String[] an_args, java.lang.String[] a_params)
An object representing SMV modules.