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

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(BDD to_add) Conjunct the initial condition with the given condition.
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.
BDD[]	allJustice() Getter for all the justice requirements of the module.
void	asyncComposition(Module inner) This functionality is not implemented for FDSModule yet.
void	conjunctTrans(BDD to_add) Conjunct the transition relation with the given condition.
void	decompose(Module inner) This functionality is not implemented for FDSModule yet.
void	disjunctTrans(BDD to_add) Disjunct the transition relation with the given condition.
ModuleBDDField[]	getAllFields() Getter for all fields declared in this module.
java.util.Vector<BDD>	getAllIniRestrictions() Get all restrictions on the initial states.
java.util.Vector<BDD>	getAllTransRestrictions() Get all restrictions on the transitions.
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.
BDD	idleStep() Construct a BDD representing the idle transition of this module.
BDD	initial() Getter for the initial states in the module.
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	popLastJustice() Removes the last justice added to this 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	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	setInitial(BDD to_add) Set the initial condition with the given condition.
void	syncComposition(Module inner) This functionality is not implemented for FDSModule yet.
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.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(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(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.

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)

conjunctTrans

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

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

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

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

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

asyncComposition

public void asyncComposition(Module inner)

This functionality is not implemented for FDSModule yet.

Specified by:

asyncComposition in class Module

Parameters:

inner - The module to compose this instance with.

Throws:

java.lang.RuntimeException - Always.

See Also:

Module.asyncComposition(edu.wis.jtlv.env.module.Module)

decompose

public void decompose(Module inner)

This functionality is not implemented for FDSModule yet.

Specified by:

decompose in class Module

Parameters:

inner - The module to remove from this instance.

Throws:

java.lang.RuntimeException - Always.

See Also:

Module.decompose(edu.wis.jtlv.env.module.Module)

syncComposition

public void syncComposition(Module inner)

This functionality is not implemented for FDSModule yet.

Specified by:

syncComposition in class Module

Parameters:

inner - The module to compose this instance with.

Throws:

java.lang.RuntimeException - Always.

See Also:

Module.syncComposition(edu.wis.jtlv.env.module.Module)