edu.wis.jtlv.env.module
Class FDSModule

java.lang.Object
  edu.wis.jtlv.env.module.Module
      edu.wis.jtlv.env.module.ModuleWithWeakFairness
          edu.wis.jtlv.env.module.FDSModule

public class FDSModule
extends ModuleWithWeakFairness

An object which represent an FDS module.

Version:

"1.2.0"

Author:

yaniv sa'ar.

See Also:

Env.loadModule(String)

Constructor Summary

FDSModule(java.lang.String player_name)
The main constructor for this kind of module, which creates an empty module.

FDSModule(java.lang.String player_name, java.lang.String[] var_names)
A constructor which receive an array of variables to be declared with initiation.

Method Summary

void	addInitial(net.sf.javabdd.BDD to_add) Conjunct the initial condition with the given condition.
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.
void	conjunctTrans(net.sf.javabdd.BDD to_add) Conjunct the transition relation with the given condition.
void	disjunctTrans(net.sf.javabdd.BDD to_add) Disjunct the transition relation with the given condition.
ModuleBDDField[]	getAllFields() Getter for all fields declared in this module.
java.util.Vector<net.sf.javabdd.BDD>	getAllIniRestrictions()
java.util.Vector<net.sf.javabdd.BDD>	getAllTransRestrictions()
java.lang.String	getFullInstName() Getter for the instance string.
java.lang.String	getName() Getter for the declared field name which holds this instance.
java.lang.String	getPath() The path leading to this module.
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.
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	popLastJustice() Removes the last justice added to this module.
void	removeAllIniRestrictions()
void	removeAllTransRestrictions()
void	removeIniRestriction(int id)
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	setInitial(net.sf.javabdd.BDD to_add) Set the initial condition with the given condition.
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.

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

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

FDSModule

public FDSModule(java.lang.String player_name)

The main constructor for this kind of module, which creates an empty module.

Parameters:

player_name - The player name.

FDSModule

public FDSModule(java.lang.String player_name,
                 java.lang.String[] var_names)

A constructor which receive an array of variables to be declared with initiation.

Parameters:

player_name - The player name.

var_names - An array of variables.

Throws:

ModuleException - If there is a duplicate variable name.

See Also:

FDSModule(String)

Method Detail

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)

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

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)

conjunctTrans

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

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.

Throws:

ModuleException - If there was a problem with adding relation.

See Also:

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

disjunctTrans

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

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.

Throws:

ModuleException - If there was a problem with adding relation.

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.

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

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

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.

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.

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.

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.

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.