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.1.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.
void	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.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	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.
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.Module

allPred, allSucc, pred, prime, primeVars, succ, unprime, unprimeVars

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

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

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)

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)

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)

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)

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.