|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
Packages that use ModuleException | |
---|---|
edu.wis.jtlv.env.module | Package dedicated to the user's modules interface. |
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(BDD p,
BDD q)
|
abstract void |
ModuleWithStrongFairness.addCompassion(BDD p,
BDD q)
Add strong (compassion) winning condition to the module. |
void |
SMVModule.addInitial(BDD to_add)
|
void |
FDSModule.addInitial(BDD to_add)
|
abstract void |
Module.addInitial(BDD to_add)
Conjunct the initial condition with the given condition. |
void |
SMVModule.addJustice(BDD to_add)
|
void |
FDSModule.addJustice(BDD to_add)
|
abstract void |
ModuleWithWeakFairness.addJustice(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 |
FDSModule.conjunctTrans(BDD to_add)
|
abstract void |
Module.conjunctTrans(BDD to_add)
Conjunct the transition relation with the given condition. |
void |
FDSModule.disjunctTrans(BDD to_add)
|
abstract void |
Module.disjunctTrans(BDD to_add)
Disjunct the transition relation with the given condition. |
void |
SMVModule.setInitial(BDD to_add)
|
void |
FDSModule.setInitial(BDD to_add)
|
abstract void |
Module.setInitial(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. |
|
SMVModule(java.lang.String player_name,
java.lang.String[] params,
java.lang.String[] instantiate_str)
A constructor for an object representing SMV modules. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |