edu.wis.jtlv.env.module
Class SMVModule

java.lang.Object
  edu.wis.jtlv.env.module.Module
      edu.wis.jtlv.env.module.ModuleWithWeakFairness
          edu.wis.jtlv.env.module.ModuleWithStrongFairness
              edu.wis.jtlv.env.module.SMVModule

public class SMVModule
extends ModuleWithStrongFairness

An object which represent an SMV module.

Version:

"1.2.0"

Author:

yaniv sa'ar.

See Also:

Env.loadModule(String)

Nested Class Summary

static class

SMVModule.SyncStatus Enum class to distinguish between synchronous and asynchronous sub module composition.

Constructor Summary

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

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)

Method Summary

void	___addDefine(java.lang.String addr) Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
void	___addDefineFromParam(java.lang.String addr) Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
void	___attachParamPointers() Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
edu.wis.jtlv.env.core.smv.schema.SMVModuleInfo	___getModuleInfo() Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.
void	addCompassion(net.sf.javabdd.BDD p, net.sf.javabdd.BDD q) Add strong (compassion) winning condition to the module.
void	addInitial(net.sf.javabdd.BDD to_add) Conjunct the initial condition with the given condition.
void	addInstanceVar(SMVModule inner, boolean is_sync) Add a module instance as a variable to this module.
void	addJustice(net.sf.javabdd.BDD to_add) Add weak (justice) winning condition to the module.
ModuleBDDField	addVar(java.lang.String new_var) Add a variable to the module.
ModuleBDDField	addVar(java.lang.String new_var, int range_start, int range_end) Add a range variable to this module.
ModuleBDDField	addVar(java.lang.String new_var, java.lang.String[] val_names) Add a set of values variable to this module.
void	asyncComposition(SMVModule inner)
int	compassionNum() Getter for the number of compassion condition defined in the module.
void	conjunctTrans(net.sf.javabdd.BDD to_add) Conjunct the transition relation with the given condition.
void	decompose(SMVModule inner)
void	disjunctTrans(net.sf.javabdd.BDD to_add) Disjunct the transition relation with the given condition.
ModuleBDDDefine[]	getAllDefines() Getter for all the defines declared in this module.
ModuleBDDField[]	getAllFields() Getter for all fields declared in this module.
java.util.Vector<net.sf.javabdd.BDD>	getAllIniRestrictions()
SMVModule[]	getAllInstances() Getter for all instances declared in this module.
SMVModule[]	getAllInstances(SMVModule.SyncStatus status) Getter for all synchronous or asynchronous instances declared in this module.
ModuleParamHolder[]	getAllParams() Getter for all declared parameters in this module signature.
java.util.Vector<net.sf.javabdd.BDD>	getAllTransRestrictions()
ModuleBDDDefine	getDefine(java.lang.String addr, boolean look_hard) Get the define declared in this module with the given name.
java.lang.String	getFullInstName() Getter for the instance string.
java.lang.String	getFullInstNameWithParams() Getter for the full instance name with the parameters.
SMVModule	getHolder() Getter for the module instance holds this instance.
SMVModule	getInstance(java.lang.String addr, boolean look_hard) Get the instances with the given name.
SMVModule[]	getInstanceArray(java.lang.String addr, boolean look_hard) Get the array of instances with the given name.
java.lang.String	getName() Getter for the declared field name which holds this instance.
ModuleParamHolder	getParam(int at_index) Getter for the declared parameter and the given index, in this module signature.
java.lang.String	getPath() The path leading to this module.
net.sf.javabdd.BDD	getValue(java.lang.String name) Get A BDD for the disjunct of all variables set to the given value.
ModuleBDDField	getVar(java.lang.String addr, boolean look_hard) Get the variable with the given name.
ModuleBDDField[]	getVarArray(java.lang.String addr, boolean look_hard) Get the array of variables with the given name.
boolean	hasDefine(java.lang.String addr, boolean look_hard) Check whether a define with the given name exists.
boolean	hasInstance(java.lang.String addr, boolean look_hard) Check whether an instance with the given name exists.
boolean	hasInstanceArray(java.lang.String addr, boolean look_hard) Check whether an instance array with the given name exists.
boolean	hasParam(java.lang.String addr, boolean look_hard) Check whether a parameter with the given name exists.
boolean	hasValue(java.lang.String name) Check whether a value with the given name exists in any of the variables of the system.
boolean	hasVar(java.lang.String addr, boolean look_hard) Check whether a variable with the given name exists.
boolean	hasVarArray(java.lang.String addr, boolean look_hard) Check whether a variable array with the given name exists.
net.sf.javabdd.BDD	idleStep() Construct a BDD representing the idle transition of this module.
net.sf.javabdd.BDD	initial() Getter for the initial states in the module.
static void	initModulesWithoutRunningVar()
static void	initModulesWithRunningVar()
net.sf.javabdd.BDD	justiceAt(int i) Getter for a justice condition defined at the given index in the module.
int	justiceNum() Getter for the number of justice condition defined in the module.
net.sf.javabdd.BDDVarSet	modulePrimeVars() Getter for the primed variable of this module.
net.sf.javabdd.BDDVarSet	moduleUnprimeVars() Getter for the unprimed variable of this module.
net.sf.javabdd.BDD	pCompassionAt(int i) Getter for a P part of the compassion condition defined at the given index in the module.
net.sf.javabdd.BDD[]	popLastCompassion() Removes the last compassion added to this module.
net.sf.javabdd.BDD	popLastJustice() Removes the last justice added to this module.
net.sf.javabdd.BDD	presStep()
net.sf.javabdd.BDD	qCompassionAt(int i) Getter for a Q part of the compassion condition defined at the given index in the module.
void	removeAllIniRestrictions()
void	removeAllTransRestrictions()
void	removeIniRestriction(int id)
void	removeInstanceVar(SMVModule inner)
void	removeRunningVar()
void	removeTransRestriction(int id)
int	restrictIni(net.sf.javabdd.BDD temp_ini)
int	restrictTrans(net.sf.javabdd.BDD temp_trans)
void	setAllIniRestrictions(java.util.Vector<net.sf.javabdd.BDD> toSet)
void	setAllTransRestrictions(java.util.Vector<net.sf.javabdd.BDD> toSet)
void	setFullPrintingMode(boolean to_set) Set the print mode for the toString procedure.
void	setInitial(net.sf.javabdd.BDD to_add) Set the initial condition with the given condition.
void	syncComposition(SMVModule inner)
java.lang.String	toString() Prepare a string describing the module, its variables, define, statement, etc.
net.sf.javabdd.BDD	trans() Getter for the transition relation of the module.
void	weakDecompose(SMVModule inner)

Methods inherited from class edu.wis.jtlv.env.module.ModuleWithStrongFairness

feasible, feasible2

Methods inherited from class edu.wis.jtlv.env.module.Module

allPred, allSucc, controlStates, elimSuccChains, hasSuccessorsTo, moduleVars, pred, reachable, shortestPath, succ, yieldStates

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

SMVModule

public SMVModule(java.lang.String player_name)

SMVModule

public SMVModule(edu.wis.jtlv.env.core.smv.schema.SMVModuleInfo a_module_info,
                 java.lang.String player_name)

An object representing SMV modules. For now, you are discourage from directly instantiating SMV modules. Please see the references.

Parameters:

a_module_info -

player_name -

Throws:

ModuleException

See Also:

Env.loadModule(String)

SMVModule

public 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)
          throws ModuleException

An object representing SMV modules. For now, you are discourage from directly instantiating SMV modules. Please see the references.

Parameters:

a_module_info -

player_name -

an_args -

a_params -

Throws:

ModuleException - If there was a problem with the parameters declared (i.e. duplicate names).

Method Detail

initModulesWithRunningVar

public static void initModulesWithRunningVar()

initModulesWithoutRunningVar

public static void initModulesWithoutRunningVar()

addVar

public ModuleBDDField addVar(java.lang.String new_var)
                      throws ModuleException,
                             ModuleVariableException

Description copied from class: Module

Add a variable to the module.

Specified by:

addVar in class Module

Parameters:

new_var - The name of the new variable to add.

Returns:

The newly created field.

Throws:

ModuleException - If there was a problem with adding the variable, e.g. a variable with this name already exists.

ModuleVariableException

addInitial

public void addInitial(net.sf.javabdd.BDD to_add)
                throws ModuleException

Description copied from class: Module

Conjunct the initial condition with the given condition.

Specified by:

addInitial in class Module

Parameters:

to_add - The condition to add to the module.

Throws:

ModuleException - If there was a problem with adding the condition, e.g. a there where primed variables in the condition.

See Also:

Module.initial(), Module.setInitial(BDD)

setInitial

public void setInitial(net.sf.javabdd.BDD to_add)
                throws ModuleException

Description copied from class: Module

Set the initial condition with the given condition.

Specified by:

setInitial in class Module

Parameters:

to_add - The condition to set to the module.

Throws:

ModuleException - If there was a problem with setting the condition, e.g. a there where primed variables in the condition.

See Also:

Module.initial(), Module.addInitial(BDD)

restrictIni

public int restrictIni(net.sf.javabdd.BDD temp_ini)

Specified by:

restrictIni in class Module

removeIniRestriction

public void removeIniRestriction(int id)

Specified by:

removeIniRestriction in class Module

removeAllIniRestrictions

public void removeAllIniRestrictions()

Specified by:

removeAllIniRestrictions in class Module

getAllIniRestrictions

public java.util.Vector<net.sf.javabdd.BDD> getAllIniRestrictions()

Specified by:

getAllIniRestrictions in class Module

setAllIniRestrictions

public void setAllIniRestrictions(java.util.Vector<net.sf.javabdd.BDD> toSet)

Specified by:

setAllIniRestrictions in class Module

conjunctTrans

public void conjunctTrans(net.sf.javabdd.BDD to_add)

Description copied from class: Module

Conjunct the transition relation with the given condition.

Specified by:

conjunctTrans in class Module

Parameters:

to_add - The transition to conjunct with the module's transitions.

See Also:

Module.trans(), Module.disjunctTrans(BDD)

disjunctTrans

public void disjunctTrans(net.sf.javabdd.BDD to_add)

Description copied from class: Module

Disjunct the transition relation with the given condition.

Specified by:

disjunctTrans in class Module

Parameters:

to_add - The transition disjunct with to the module's transitions.

See Also:

Module.trans(), Module.conjunctTrans(BDD)

restrictTrans

public int restrictTrans(net.sf.javabdd.BDD temp_trans)

Specified by:

restrictTrans in class Module

removeTransRestriction

public void removeTransRestriction(int id)

Specified by:

removeTransRestriction in class Module

removeAllTransRestrictions

public void removeAllTransRestrictions()

Specified by:

removeAllTransRestrictions in class Module

getAllTransRestrictions

public java.util.Vector<net.sf.javabdd.BDD> getAllTransRestrictions()

Specified by:

getAllTransRestrictions in class Module

setAllTransRestrictions

public void setAllTransRestrictions(java.util.Vector<net.sf.javabdd.BDD> toSet)

Specified by:

setAllTransRestrictions in class Module

addJustice

public void addJustice(net.sf.javabdd.BDD to_add)
                throws ModuleException

Description copied from class: ModuleWithWeakFairness

Add weak (justice) winning condition to the module.

Specified by:

addJustice in class ModuleWithWeakFairness

Parameters:

to_add - The winning condition to add to the module.

Throws:

ModuleException - If there was a problem with adding the condition.

See Also:

ModuleWithWeakFairness.justiceNum(), ModuleWithWeakFairness.justiceAt(int)

popLastJustice

public net.sf.javabdd.BDD popLastJustice()

Description copied from class: ModuleWithWeakFairness

Removes the last justice added to this module.

Specified by:

popLastJustice in class ModuleWithWeakFairness

Returns:

The removed justice.

addCompassion

public void addCompassion(net.sf.javabdd.BDD p,
                          net.sf.javabdd.BDD q)
                   throws ModuleException

Description copied from class: ModuleWithStrongFairness

Add strong (compassion) winning condition to the module.

Specified by:

addCompassion in class ModuleWithStrongFairness

Parameters:

p - The p winning condition to add to the module.

q - The q winning condition to add to the module.

Throws:

ModuleException - If there was a problem with adding the condition.

See Also:

ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.qCompassionAt(int)

popLastCompassion

public net.sf.javabdd.BDD[] popLastCompassion()

Description copied from class: ModuleWithStrongFairness

Removes the last compassion added to this module.

Specified by:

popLastCompassion in class ModuleWithStrongFairness

Returns:

An array of two BDDs with the removed compassion.

modulePrimeVars

public net.sf.javabdd.BDDVarSet modulePrimeVars()

Description copied from class: Module

Getter for the primed variable of this module.

Specified by:

modulePrimeVars in class Module

Returns:

The primed variables of this module.

moduleUnprimeVars

public net.sf.javabdd.BDDVarSet moduleUnprimeVars()

Description copied from class: Module

Getter for the unprimed variable of this module.

Specified by:

moduleUnprimeVars in class Module

Returns:

The unprimed variables of this module.

getAllFields

public ModuleBDDField[] getAllFields()

Description copied from class: Module

Getter for all fields declared in this module.

Specified by:

getAllFields in class Module

Returns:

All fields declared in this module.

initial

public net.sf.javabdd.BDD initial()

Description copied from class: Module

Getter for the initial states in the module.

Specified by:

initial in class Module

Returns:

The initial states of the module.

See Also:

Module.addInitial(BDD), Module.setInitial(BDD)

trans

public net.sf.javabdd.BDD trans()

Description copied from class: Module

Getter for the transition relation of the module.

Specified by:

trans in class Module

Returns:

The transition relation of the module.

See Also:

Module.disjunctTrans(BDD), Module.conjunctTrans(BDD), Module.idleStep()

idleStep

public net.sf.javabdd.BDD idleStep()

Description copied from class: Module

Construct a BDD representing the idle transition of this module. If the process has a synchronously composed inner module (possible only in SMVModule), then it will also construct its idle step.

Specified by:

idleStep in class Module

Returns:

the idle transition of this module.

See Also:

Module.disjunctTrans(BDD), Module.conjunctTrans(BDD), Module.trans()

presStep

public net.sf.javabdd.BDD presStep()

justiceNum

public int justiceNum()

Description copied from class: ModuleWithWeakFairness

Getter for the number of justice condition defined in the module.

Specified by:

justiceNum in class ModuleWithWeakFairness

Returns:

The number of justice condition defined in the module.

See Also:

ModuleWithWeakFairness.addJustice(BDD), ModuleWithWeakFairness.justiceAt(int)

justiceAt

public net.sf.javabdd.BDD justiceAt(int i)

Description copied from class: ModuleWithWeakFairness

Getter for a justice condition defined at the given index in the module.

Specified by:

justiceAt in class ModuleWithWeakFairness

Parameters:

i - The index of the justice condition to return.

Returns:

The justice condition defined defined at the given index in the module.

See Also:

ModuleWithWeakFairness.addJustice(BDD), ModuleWithWeakFairness.justiceNum()

compassionNum

public int compassionNum()

Description copied from class: ModuleWithStrongFairness

Getter for the number of compassion condition defined in the module.

Specified by:

compassionNum in class ModuleWithStrongFairness

Returns:

The number of compassion condition defined in the module.

See Also:

ModuleWithStrongFairness.addCompassion(BDD, BDD), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.qCompassionAt(int)

pCompassionAt

public net.sf.javabdd.BDD pCompassionAt(int i)

Description copied from class: ModuleWithStrongFairness

Getter for a P part of the compassion condition defined at the given index in the module.

Specified by:

pCompassionAt in class ModuleWithStrongFairness

Parameters:

i - The index of the compassion condition to return.

Returns:

The P part of the compassion condition defined defined at the given index in the module.

See Also:

ModuleWithStrongFairness.addCompassion(BDD, BDD), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.qCompassionAt(int)

qCompassionAt

public net.sf.javabdd.BDD qCompassionAt(int i)

Description copied from class: ModuleWithStrongFairness

Getter for a Q part of the compassion condition defined at the given index in the module.

Specified by:

qCompassionAt in class ModuleWithStrongFairness

Parameters:

i - The index of the compassion condition to return.

Returns:

The Q part of the compassion condition defined defined at the given index in the module.

See Also:

ModuleWithStrongFairness.addCompassion(BDD, BDD), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.pCompassionAt(int)

addVar

public ModuleBDDField addVar(java.lang.String new_var,
                             java.lang.String[] val_names)
                      throws ModuleException

Add a set of values variable to this module.

Parameters:

new_var - The new variable name.

val_names - The set of values that this variable can be assigned with.

Returns:

The newly created field.

Throws:

ModuleException - If an illegal manipulation to the module had been done. e.g. duplicate variable names.

See Also:

addVar(String), addVar(String, int, int), hasVar(String, boolean), getVar(String, boolean), hasVarArray(String, boolean), getVarArray(String, boolean)

addVar

public ModuleBDDField addVar(java.lang.String new_var,
                             int range_start,
                             int range_end)
                      throws ModuleException

Add a range variable to this module.

Parameters:

new_var - The new variable name.

range_start - The starting range of the variable.

range_end - The ending range of the variable.

Returns:

The newly created field.

Throws:

ModuleException - If an illegal manipulation to the module had been done. e.g. duplicate variable names.

See Also:

addVar(String), addVar(String, String[]), hasVar(String, boolean), getVar(String, boolean), hasVarArray(String, boolean), getVarArray(String, boolean)

addInstanceVar

public void addInstanceVar(SMVModule inner,
                           boolean is_sync)
                    throws ModuleException

Add a module instance as a variable to this module.

Parameters:

inner - The inner instance to compose this module with.

is_sync - Is this a synchronous inner instance or asynchronous.

Throws:

ModuleException - If the name of the module does not fit the naming convention for internal modules. i.e. if this module name is not the longest prefix of the module to add name.

See Also:

hasInstance(String, boolean), hasInstanceArray(String, boolean), getInstance(String, boolean), getAllInstances(), getAllInstances(edu.wis.jtlv.env.module.SMVModule.SyncStatus), getInstanceArray(String, boolean)

removeInstanceVar

public void removeInstanceVar(SMVModule inner)
                       throws ModuleException

Throws:

ModuleException

removeRunningVar

public void removeRunningVar()

syncComposition

public void syncComposition(SMVModule inner)

asyncComposition

public void asyncComposition(SMVModule inner)
                      throws ModuleException

Throws:

ModuleException

decompose

public void decompose(SMVModule inner)
               throws ModuleException

Throws:

ModuleException

weakDecompose

public void weakDecompose(SMVModule inner)

hasVar

public boolean hasVar(java.lang.String addr,
                      boolean look_hard)

Check whether a variable with the given name exists.

Parameters:

addr - The variable full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

true if the variable field exists.

See Also:

addVar(String), addVar(String, String[]), addVar(String, int, int), getVar(String, boolean), hasVarArray(String, boolean), getVarArray(String, boolean)

hasVarArray

public boolean hasVarArray(java.lang.String addr,
                           boolean look_hard)

Check whether a variable array with the given name exists.

Parameters:

addr - The array full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

true if the variable field array exists.

See Also:

addVar(String), addVar(String, String[]), addVar(String, int, int), hasVar(String, boolean), hasVarArray(String, boolean), getVar(String, boolean)

hasDefine

public boolean hasDefine(java.lang.String addr,
                         boolean look_hard)

Check whether a define with the given name exists.

Parameters:

addr - The define full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

true if the define exists.

See Also:

getDefine(String, boolean), getAllDefines()

hasInstance

public boolean hasInstance(java.lang.String addr,
                           boolean look_hard)

Check whether an instance with the given name exists.

Parameters:

addr - The instance full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

true if the instance exists.

See Also:

addInstanceVar(SMVModule, boolean), hasInstanceArray(String, boolean), getInstance(String, boolean), getAllInstances(), getAllInstances(edu.wis.jtlv.env.module.SMVModule.SyncStatus), getInstanceArray(String, boolean)

hasInstanceArray

public boolean hasInstanceArray(java.lang.String addr,
                                boolean look_hard)

Check whether an instance array with the given name exists.

Parameters:

addr - The array full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

true if the instance array exists.

See Also:

addInstanceVar(SMVModule, boolean), getInstanceArray(String, boolean), hasInstance(String, boolean), getInstance(String, boolean)

hasValue

public boolean hasValue(java.lang.String name)

Check whether a value with the given name exists in any of the variables of the system.

Parameters:

name - The value name.

Returns:

true if the value exists.

See Also:

getValue(String)

hasParam

public boolean hasParam(java.lang.String addr,
                        boolean look_hard)

Check whether a parameter with the given name exists.

Parameters:

addr - The parameter full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

true if the parameter exists.

See Also:

getParam(int), getAllParams()

getVar

public ModuleBDDField getVar(java.lang.String addr,
                             boolean look_hard)

Get the variable with the given name.

Parameters:

addr - The variable full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

The variable field.

See Also:

addVar(String), addVar(String, String[]), addVar(String, int, int), hasVar(String, boolean), hasVarArray(String, boolean), getVarArray(String, boolean)

getVarArray

public ModuleBDDField[] getVarArray(java.lang.String addr,
                                    boolean look_hard)

Get the array of variables with the given name. i.e., for an array of variables,
var_arr : array 0..3 of boolean;
This procedure with the parameter "var_arr", will return all 4 fields of this array. To get an exact field, for example "var_arr[3]", you can use getVar(String, boolean), with the parameter "inst_arr[3]".

Parameters:

addr - The array full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

The variable field.

See Also:

addVar(String), addVar(String, String[]), addVar(String, int, int), hasVar(String, boolean), hasVarArray(String, boolean), getVar(String, boolean)

getDefine

public ModuleBDDDefine getDefine(java.lang.String addr,
                                 boolean look_hard)

Get the define declared in this module with the given name.

Parameters:

addr - The define full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

The instance.

See Also:

hasDefine(String, boolean), getAllDefines()

getInstance

public SMVModule getInstance(java.lang.String addr,
                             boolean look_hard)

Get the instances with the given name.

Parameters:

addr - The instance full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

The instance.

See Also:

addInstanceVar(SMVModule, boolean), hasInstanceArray(String, boolean), hasInstance(String, boolean), getAllInstances(), getAllInstances(edu.wis.jtlv.env.module.SMVModule.SyncStatus), getInstanceArray(String, boolean)

getInstanceArray

public SMVModule[] getInstanceArray(java.lang.String addr,
                                    boolean look_hard)

Get the array of instances with the given name. i.e., for an array of instances,
inst_arr : array 0..7 of some_module;
This procedure with the parameter "inst_arr", will return all 8 instances of this array. To get an exact instance, for example "inst_arr[3]", you can use getInstance(String, boolean), with the parameter "inst_arr[3]".

Parameters:

addr - The array full name relative to this module.

look_hard - Whether to go into sub modules and keep on looking.

Returns:

The array of instances.

See Also:

addInstanceVar(SMVModule, boolean), hasInstanceArray(String, boolean), hasInstance(String, boolean), getInstance(String, boolean)

getValue

public net.sf.javabdd.BDD getValue(java.lang.String name)

Get A BDD for the disjunct of all variables set to the given value. i.e., if a variable does not have the given string value, it is set to false.

Parameters:

name - The value name.

Returns:

A BDD with all variables set to the given string value.

See Also:

hasValue(String)

getParam

public ModuleParamHolder getParam(int at_index)

Getter for the declared parameter and the given index, in this module signature.

Parameters:

at_index - The index of the param to return.

Returns:

The parameter at the given index.

See Also:

hasDefine(String, boolean), getAllParams()

getAllDefines

public ModuleBDDDefine[] getAllDefines()

Getter for all the defines declared in this module.

Returns:

All defines declared in this module.

See Also:

hasDefine(String, boolean), getDefine(String, boolean)

getAllInstances

public SMVModule[] getAllInstances()

Getter for all instances declared in this module.

Returns:

All instances declared in this module.

See Also:

addInstanceVar(SMVModule, boolean), hasInstance(String, boolean), getInstance(String, boolean), getHolder(), getAllInstances(edu.wis.jtlv.env.module.SMVModule.SyncStatus)

getAllInstances

public SMVModule[] getAllInstances(SMVModule.SyncStatus status)

Getter for all synchronous or asynchronous instances declared in this module.

Parameters:

status - The type of modules to fetch.

Returns:

All synchronous or asynchronous instances declared in this module.

See Also:

addInstanceVar(SMVModule, boolean), hasInstance(String, boolean), hasInstanceArray(String, boolean), getInstance(String, boolean), getHolder(), getAllInstances(), SMVModule.SyncStatus

getAllParams

public ModuleParamHolder[] getAllParams()

Getter for all declared parameters in this module signature.

Returns:

All declared parameters in this module signature.

See Also:

hasParam(String, boolean), getParam(int)

getHolder

public SMVModule getHolder()

Getter for the module instance holds this instance.

Returns:

The module instance holds this instance.

See Also:

getAllInstances(), getAllInstances(edu.wis.jtlv.env.module.SMVModule.SyncStatus)

getFullInstName

public java.lang.String getFullInstName()

Description copied from class: Module

Getter for the instance string.

Specified by:

getFullInstName in class Module

Returns:

The instance string.

getFullInstNameWithParams

public java.lang.String getFullInstNameWithParams()

Getter for the full instance name with the parameters.

Returns:

The full instance name with the parameters.

setFullPrintingMode

public void setFullPrintingMode(boolean to_set)

Set the print mode for the toString procedure. If printing mode is set to full, then all BDDs and winning conditions will also be printed.

Parameters:

to_set - Set or reset the printing mode.

toString

public java.lang.String toString()

Description copied from class: Module

Prepare a string describing the module, its variables, define, statement, etc.

Specified by:

toString in class Module

Returns:

A string describing the module.

getName

public java.lang.String getName()

Description copied from class: Module

Getter for the declared field name which holds this instance.

Specified by:

getName in class Module

Returns:

The declared field name which holds this instance.

getPath

public java.lang.String getPath()

Description copied from class: Module

The path leading to this module.

Specified by:

getPath in class Module

Returns:

The path leading to this module.

___addDefine

public void ___addDefine(java.lang.String addr)
                  throws ModuleException

Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.

Add a new define variable to this module. This procedure only creates an entity and does not attach a value. To attach a value, the user most obtain the newly created define entity, using getDefine(String, boolean) or getAllDefines(), and attach a value using ModuleBDDDefine.attachStmt(edu.wis.jtlv.env.core.smv.eval.StmtDefineOperator)

Parameters:

addr - The name for the newly created define entity.

Throws:

ModuleException - If an illegal manipulation to the module had been done. e.g. duplicate variable names.

See Also:

___addDefineFromParam(String)

___addDefineFromParam

public void ___addDefineFromParam(java.lang.String addr)
                           throws ModuleException

Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.

Add a new define variable from a lower instance to this module. This procedure only creates an entity and does not attach a value. To attach a value, the user most obtain the newly created define entity, using getDefine(String, boolean) or getAllDefines(), and attach a value using ModuleBDDDefine.attachStmt(edu.wis.jtlv.env.core.smv.eval.StmtDefineOperator)

Parameters:

addr - The name for the newly created define entity.

Throws:

ModuleException - If an illegal manipulation to the module had been done. e.g. duplicate variable names.

See Also:

___addDefine(String)

___getModuleInfo

public edu.wis.jtlv.env.core.smv.schema.SMVModuleInfo ___getModuleInfo()

Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.

The the module parsing information.

Returns:

Parsing info.

___attachParamPointers

public void ___attachParamPointers()
                            throws ModuleException

Deprecated. INTERNAL PROCEDURE - will be encapsulated and removed from the external API in the following few releases.

Attach the module signature variables to their values.

Throws:

ModuleException - If there was a problem evaluating defines.