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.3.2"

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)
A constructor for 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)
A constructor for 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.

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(BDD p, BDD q) Add strong (compassion) winning condition to the module.
void	addInitial(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(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.
BDD[]	allJustice() Getter for all the justice requirements of the module.
BDD[]	allPCompassion() Getter for all the p's, of the compassion requirements of the module.
BDD[]	allQCompassion() Getter for all the q's, of the compassion requirements of the module.
void	asyncComposition(Module inner) add asynchronous composition to this module.
int	compassionNum() Getter for the number of compassion condition defined in the module.
void	conjunctTrans(BDD to_add) Conjunct the transition relation with the given condition.
void	decompose(Module inner) remove composition from this module.
void	disjunctTrans(BDD to_add) Disjunct the transition relation with the given condition.
java.util.Vector<BDD>	getAllConjunctTransElements()
ModuleBDDDefine[]	getAllDefines() Getter for all the defines declared in this module.
ModuleBDDField[]	getAllFields() Getter for all fields declared in this module.
java.util.Vector<BDD>	getAllIniRestrictions() Get all restrictions on the initial states.
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<BDD>	getAllTransRestrictions() Get all restrictions on the transitions.
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.
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.
BDD	idleStep() Construct a BDD representing the idle transition of this module.
BDD	initial() Getter for the initial states in the module.
static void	initModulesWithoutRunningVar() A static option which does not add "running" variable upon a creation of a new instance.
static void	initModulesWithRunningVar() For NuSMV format compatibility, a static option which adds a "running" variable upon a creation of a new instance.
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.
BDDVarSet	modulePrimeVars() Getter for the primed variable of this module.
BDDVarSet	moduleUnprimeVars() Getter for the unprimed variable of this module.
BDD	pCompassionAt(int i) Getter for a P part of the compassion condition defined at the given index in the module.
BDD[]	popLastCompassion() Removes the last compassion added to this module.
BDD	popLastJustice() Removes the last justice added to this module.
BDD	presStep() Construct a BDD representing the idle transition of this module and its synchronous sub modules.
BDD	qCompassionAt(int i) Getter for a Q part of the compassion condition defined at the given index in the module.
void	removeAllIniRestrictions() Remove all restrictions from the initial states.
void	removeAllTransRestrictions() Remove all restrictions from the transitions.
void	removeIniRestriction(int id) Remove a restriction from the initial states.
void	removeInstanceVar(SMVModule inner) Removes and inner composed module.
void	removeRunningVar() Remove the "running variable if is there (NuSMV compatibility)
void	removeTransRestriction(int id) Remove a restriction from the transitions.
int	restrictIni(BDD temp_ini) Add a restriction to the initial states.
int	restrictTrans(BDD temp_trans) Add a restriction to the transitions.
void	setAllIniRestrictions(java.util.Vector<BDD> toSet) Set all restrictions for the initial states.
void	setAllTransRestrictions(java.util.Vector<BDD> toSet) Set all restrictions for the transitions.
void	setFullPrintingMode(boolean to_set) Set the print mode for the toString procedure.
void	setInitial(BDD to_add) Set the initial condition with the given condition.
void	syncComposition(Module inner) add synchronous composition to this module.
java.lang.String	toString() Prepare a string describing the module, its variables, define, statement, etc.
BDD	trans() Getter for the transition relation of the module.

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)

A constructor for an object representing SMV modules.

Parameters:

player_name - The name of the this instance.

See Also:

SMVModule(String, String[], String[]), Env.loadModule(String)

SMVModule

public SMVModule(java.lang.String player_name,
                 java.lang.String[] params,
                 java.lang.String[] instantiate_str)
          throws ModuleException

A constructor for an object representing SMV modules. In This constructor you are allowed to add a set of parameters to the instance, and a matching set arguments (i.e. their actual values). Please

NOTE: this type of instantiation is still experimental, and not fully tested. please check to see that the result are as expected.

Parameters:

player_name - The name of the this instance.

params - The name of the parameter (inside the module)

instantiate_str - The string to instantiate then with (qualified field name)

Throws:

ModuleException

See Also:

SMVModule(String), Env.loadModule(String)

SMVModule

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

A constructor for an object representing SMV modules. You are discourage from directly instantiating SMV modules using this method. Please see the reference link.

Parameters:

a_module_info - An abstract info of the module.

player_name - The name of the this instance.

See Also:

SMVModule(String), SMVModule(String, String[], String[]), 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()

For NuSMV format compatibility, a static option which adds a "running" variable upon a creation of a new instance.

See Also:

initModulesWithoutRunningVar()

initModulesWithoutRunningVar

public static void initModulesWithoutRunningVar()

A static option which does not add "running" variable upon a creation of a new instance.

See Also:

initModulesWithRunningVar()

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(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(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(BDD temp_ini)

Description copied from class: Module

Add a restriction to the initial states.

Specified by:

restrictIni in class Module

Parameters:

temp_ini - The BDD to restrict with.

Returns:

The restriction index.

removeIniRestriction

public void removeIniRestriction(int id)

Description copied from class: Module

Remove a restriction from the initial states.

Specified by:

removeIniRestriction in class Module

Parameters:

id - The index of restriction to remove.

removeAllIniRestrictions

public void removeAllIniRestrictions()

Description copied from class: Module

Remove all restrictions from the initial states.

Specified by:

removeAllIniRestrictions in class Module

getAllIniRestrictions

public java.util.Vector<BDD> getAllIniRestrictions()

Description copied from class: Module

Get all restrictions on the initial states.

Specified by:

getAllIniRestrictions in class Module

Returns:

A vector of BDD restriction.

setAllIniRestrictions

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

Description copied from class: Module

Set all restrictions for the initial states.

Specified by:

setAllIniRestrictions in class Module

Parameters:

toSet - A vector of restrictions to set.

conjunctTrans

public void conjunctTrans(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(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(BDD temp_trans)

Description copied from class: Module

Add a restriction to the transitions.

Specified by:

restrictTrans in class Module

Parameters:

temp_trans - The BDD to restrict with.

Returns:

The restriction index.

removeTransRestriction

public void removeTransRestriction(int id)

Description copied from class: Module

Remove a restriction from the transitions.

Specified by:

removeTransRestriction in class Module

Parameters:

id - The index of restriction to remove.

removeAllTransRestrictions

public void removeAllTransRestrictions()

Description copied from class: Module

Remove all restrictions from the transitions.

Specified by:

removeAllTransRestrictions in class Module

getAllTransRestrictions

public java.util.Vector<BDD> getAllTransRestrictions()

Description copied from class: Module

Get all restrictions on the transitions.

Specified by:

getAllTransRestrictions in class Module

Returns:

A vector of BDD restriction.

setAllTransRestrictions

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

Description copied from class: Module

Set all restrictions for the transitions.

Specified by:

setAllTransRestrictions in class Module

Parameters:

toSet - A vector of restrictions to set.

addJustice

public void addJustice(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), ModuleWithWeakFairness.popLastJustice(), ModuleWithWeakFairness.allJustice()

popLastJustice

public 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.

See Also:

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

addCompassion

public void addCompassion(BDD p,
                          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.popLastCompassion(), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.qCompassionAt(int), ModuleWithStrongFairness.allPCompassion(), ModuleWithStrongFairness.allQCompassion()

popLastCompassion

public 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.

See Also:

ModuleWithStrongFairness.addCompassion(BDD, BDD), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.qCompassionAt(int), ModuleWithStrongFairness.allPCompassion(), ModuleWithStrongFairness.allQCompassion()

modulePrimeVars

public 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 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 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 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()

getAllConjunctTransElements

public java.util.Vector<BDD> getAllConjunctTransElements()

idleStep

public 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, 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 BDD presStep()

Construct a BDD representing the idle transition of this module and its synchronous sub modules. If the process has asynchronously inner module, then it will NOT be included.

Returns:

The idle transition of this module and its synchronous sub modules.

See Also:

idleStep()

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), ModuleWithWeakFairness.popLastJustice(), ModuleWithWeakFairness.allJustice()

justiceAt

public 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(), ModuleWithWeakFairness.popLastJustice(), ModuleWithWeakFairness.allJustice()

allJustice

public BDD[] allJustice()

Description copied from class: ModuleWithWeakFairness

Getter for all the justice requirements of the module.

Specified by:

allJustice in class ModuleWithWeakFairness

Returns:

The justice requirements.

See Also:

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

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.popLastCompassion(), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.qCompassionAt(int), ModuleWithStrongFairness.allPCompassion(), ModuleWithStrongFairness.allQCompassion()

pCompassionAt

public 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.popLastCompassion(), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.qCompassionAt(int), ModuleWithStrongFairness.allPCompassion(), ModuleWithStrongFairness.allQCompassion()

qCompassionAt

public 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.popLastCompassion(), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.allPCompassion(), ModuleWithStrongFairness.allQCompassion()

allPCompassion

public BDD[] allPCompassion()

Description copied from class: ModuleWithStrongFairness

Getter for all the p's, of the compassion requirements of the module.

Specified by:

allPCompassion in class ModuleWithStrongFairness

Returns:

The p's part of the compassion requirements.

See Also:

ModuleWithStrongFairness.addCompassion(BDD, BDD), ModuleWithStrongFairness.popLastCompassion(), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.qCompassionAt(int), ModuleWithStrongFairness.allQCompassion()

allQCompassion

public BDD[] allQCompassion()

Description copied from class: ModuleWithStrongFairness

Getter for all the q's, of the compassion requirements of the module.

Specified by:

allQCompassion in class ModuleWithStrongFairness

Returns:

The q's part of the compassion requirements.

See Also:

ModuleWithStrongFairness.addCompassion(BDD, BDD), ModuleWithStrongFairness.popLastCompassion(), ModuleWithStrongFairness.compassionNum(), ModuleWithStrongFairness.pCompassionAt(int), ModuleWithStrongFairness.qCompassionAt(int), ModuleWithStrongFairness.allPCompassion()

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)

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(SMVModule)

removeInstanceVar

public void removeInstanceVar(SMVModule inner)

Removes and inner composed module.

Parameters:

inner - The inner module to remove.

See Also:

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

removeRunningVar

public void removeRunningVar()

Remove the "running variable if is there (NuSMV compatibility)

syncComposition

public void syncComposition(Module inner)

Description copied from class: Module

add synchronous composition to this module.

Specified by:

syncComposition in class Module

Parameters:

inner - The module to compose this instance with.

asyncComposition

public void asyncComposition(Module inner)

Description copied from class: Module

add asynchronous composition to this module.

Specified by:

asyncComposition in class Module

Parameters:

inner - The module to compose this instance with.

decompose

public void decompose(Module inner)

Description copied from class: Module

remove composition from this module.

Specified by:

decompose in class Module

Parameters:

inner - The module to remove from this instance.

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 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.