edu.wis.jtlv.env.module
Class Module

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

Direct Known Subclasses:

ModuleWithWeakFairness

public abstract class Module
extends java.lang.Object

A general interface for modules. It is advise to load modules and manipulate them through the file itself, and then load it to the environment through Env. However, this is not the only way to create a new module. One can use whole set of manipulating procedures provided by this interface, to create a new module.
By default, The initial condition is TRUE, transition relation is TRUE.

Version:

"1.3.2"

Author:

yaniv sa'ar.

See Also:

Env.loadModule(String), Env.getAllModules(), Env.getModule(String)

Constructor Summary

Module()

Method Summary

abstract void	addInitial(BDD to_add) Conjunct the initial condition with the given condition.
abstract ModuleBDDField	addVar(java.lang.String new_var) Add a variable to the module.
BDD	allPred(BDD to) Given a set of state, this procedure return all states which can lead in any number of module steps to these states.
BDD	allSucc(BDD from) This procedure return all states which the module can reach in any number of steps from given a set of state.
abstract void	asyncComposition(Module inner) add asynchronous composition to this module.
abstract void	conjunctTrans(BDD to_add) Conjunct the transition relation with the given condition.
BDD	controlStates(Module responder, BDD to) A state s is included in the returning result if the this module can force the responder to reach a state in "to".
abstract void	decompose(Module inner) remove composition from this module.
abstract void	disjunctTrans(BDD to_add) Disjunct the transition relation with the given condition.
BDD	elimSuccChains(BDD scc) Eliminate states from scc which have no successors within scc.
BDD	feasible() This is essentially algorithm "FEASIBLE", from the article: Yonit Ketsen, Amir Pnueli, Li-on Raviv, Elad Shahar, "Model checking with strong fairness".
BDD	feasible2() Version which allows justice and compassion requirement to refer to the next state.
abstract ModuleBDDField[]	getAllFields() Getter for all fields declared in this module.
abstract java.util.Vector<BDD>	getAllIniRestrictions() Get all restrictions on the initial states.
abstract java.util.Vector<BDD>	getAllTransRestrictions() Get all restrictions on the transitions.
abstract java.lang.String	getFullInstName() Getter for the instance string.
abstract java.lang.String	getName() Getter for the declared field name which holds this instance.
abstract java.lang.String	getPath() The path leading to this module.
BDD	hasSuccessorsTo(BDD state, BDD to) Get the subset of states which has successor to the other given set of states.
abstract BDD	idleStep() Construct a BDD representing the idle transition of this module.
abstract BDD	initial() Getter for the initial states in the module.
abstract BDDVarSet	modulePrimeVars() Getter for the primed variable of this module.
abstract BDDVarSet	moduleUnprimeVars() Getter for the unprimed variable of this module.
BDDVarSet	moduleVars() Getter for all, primed and unprimed variable of this module.
BDD	pred(BDD to) Given a set of state, this procedure return all states which can lead in a single module step to these states.
BDD	reachable() Calculate all reachable states form the initial states.
abstract void	removeAllIniRestrictions() Remove all restrictions from the initial states.
abstract void	removeAllTransRestrictions() Remove all restrictions from the transitions.
abstract void	removeIniRestriction(int id) Remove a restriction from the initial states.
abstract void	removeTransRestriction(int id) Remove a restriction from the transitions.
abstract int	restrictIni(BDD temp_ini) Add a restriction to the initial states.
abstract int	restrictTrans(BDD temp_trans) Add a restriction to the transitions.
abstract void	setAllIniRestrictions(java.util.Vector<BDD> toSet) Set all restrictions for the initial states.
abstract void	setAllTransRestrictions(java.util.Vector<BDD> toSet) Set all restrictions for the transitions.
abstract void	setInitial(BDD to_add) Set the initial condition with the given condition.
BDD[]	shortestPath(BDD source, BDD dest) Compute the shortest path from source to destination.
BDD	succ(BDD from) This procedure return all states which the module can reach in a single step from given a set of state.
abstract void	syncComposition(Module inner) add synchronous composition to this module.
abstract java.lang.String	toString() Prepare a string describing the module, its variables, define, statement, etc.
abstract BDD	trans() Getter for the transition relation of the module.
BDD	yieldStates(Module responder, BDD to) A state s in included in the returning result if responder module can force this module to reach a state in "to". That is, regardless of how this module will move from the result, the responder module can choose an appropriate move into "to".

Methods inherited from class java.lang.Object

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

Constructor Detail

Module

public Module()

Method Detail

addVar

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

Add a variable to the 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.

addInitial

public abstract void addInitial(BDD to_add)
                         throws ModuleException

Conjunct the initial condition with the given condition.

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:

initial(), setInitial(BDD)

setInitial

public abstract void setInitial(BDD to_add)
                         throws ModuleException

Set the initial condition with the given condition.

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:

initial(), addInitial(BDD)

conjunctTrans

public abstract void conjunctTrans(BDD to_add)
                            throws ModuleException

Conjunct the transition relation with the given condition.

Parameters:

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

Throws:

ModuleException - If there was a problem with adding relation.

See Also:

trans(), disjunctTrans(BDD)

disjunctTrans

public abstract void disjunctTrans(BDD to_add)
                            throws ModuleException

Disjunct the transition relation with the given condition.

Parameters:

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

Throws:

ModuleException - If there was a problem with adding relation.

See Also:

trans(), conjunctTrans(BDD)

getAllFields

public abstract ModuleBDDField[] getAllFields()

Getter for all fields declared in this module.

Returns:

All fields declared in this module.

modulePrimeVars

public abstract BDDVarSet modulePrimeVars()

Getter for the primed variable of this module.

Returns:

The primed variables of this module.

moduleUnprimeVars

public abstract BDDVarSet moduleUnprimeVars()

Getter for the unprimed variable of this module.

Returns:

The unprimed variables of this module.

moduleVars

public BDDVarSet moduleVars()

Getter for all, primed and unprimed variable of this module.

Returns:

The unprimed variables of this module.

initial

public abstract BDD initial()

Getter for the initial states in the module.

Returns:

The initial states of the module.

See Also:

addInitial(BDD), setInitial(BDD)

trans

public abstract BDD trans()

Getter for the transition relation of the module.

Returns:

The transition relation of the module.

See Also:

disjunctTrans(BDD), conjunctTrans(BDD), idleStep()

idleStep

public abstract BDD idleStep()

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.

Returns:

the idle transition of this module.

See Also:

disjunctTrans(BDD), conjunctTrans(BDD), trans()

pred

public BDD pred(BDD to)

Given a set of state, this procedure return all states which can lead in a single module step to these states.

Parameters:

to - The set of state to be reach.

Returns:

The set of states which can lead in a single module step to the given states.

See Also:

allPred(BDD), trans(), succ(BDD)

allPred

public BDD allPred(BDD to)

Given a set of state, this procedure return all states which can lead in any number of module steps to these states.

Parameters:

to - The set of state to be reach.

Returns:

The set of states which can lead in any number of module step to the given states.

See Also:

pred(BDD), trans(), allSucc(BDD)

succ

public BDD succ(BDD from)

This procedure return all states which the module can reach in a single step from given a set of state.

Parameters:

from - The set of state to start from.

Returns:

The set of states which the module can reach in a single module step from the given states.

See Also:

allSucc(BDD), trans(), pred(BDD)

allSucc

public BDD allSucc(BDD from)

This procedure return all states which the module can reach in any number of steps from given a set of state.

Parameters:

from - The set of state to start from.

Returns:

The set of states which the module can reach in any number of module steps from the given states.

See Also:

allPred(BDD), trans(), succ(BDD)

syncComposition

public abstract void syncComposition(Module inner)

add synchronous composition to this module.

Parameters:

inner - The module to compose this instance with.

asyncComposition

public abstract void asyncComposition(Module inner)

add asynchronous composition to this module.

Parameters:

inner - The module to compose this instance with.

decompose

public abstract void decompose(Module inner)

remove composition from this module.

Parameters:

inner - The module to remove from this instance.

restrictIni

public abstract int restrictIni(BDD temp_ini)

Add a restriction to the initial states.

Parameters:

temp_ini - The BDD to restrict with.

Returns:

The restriction index.

removeIniRestriction

public abstract void removeIniRestriction(int id)

Remove a restriction from the initial states.

Parameters:

id - The index of restriction to remove.

removeAllIniRestrictions

public abstract void removeAllIniRestrictions()

Remove all restrictions from the initial states.

getAllIniRestrictions

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

Get all restrictions on the initial states.

Returns:

A vector of BDD restriction.

setAllIniRestrictions

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

Set all restrictions for the initial states.

Parameters:

toSet - A vector of restrictions to set.

restrictTrans

public abstract int restrictTrans(BDD temp_trans)

Add a restriction to the transitions.

Parameters:

temp_trans - The BDD to restrict with.

Returns:

The restriction index.

removeTransRestriction

public abstract void removeTransRestriction(int id)

Remove a restriction from the transitions.

Parameters:

id - The index of restriction to remove.

removeAllTransRestrictions

public abstract void removeAllTransRestrictions()

Remove all restrictions from the transitions.

getAllTransRestrictions

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

Get all restrictions on the transitions.

Returns:

A vector of BDD restriction.

setAllTransRestrictions

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

Set all restrictions for the transitions.

Parameters:

toSet - A vector of restrictions to set.

reachable

public BDD reachable()

Calculate all reachable states form the initial states.

Returns:

The reachable states.

shortestPath

public BDD[] shortestPath(BDD source,
                          BDD dest)

Compute the shortest path from source to destination.
Algorithm from: Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar, "Model Checking with Strong Fairness".

Parameters:

source - The states to start look for path.

dest - The states to reach in the path.

Returns:

An array representing a path, null if the algorithm could not find a path.

feasible

public BDD feasible()

This is essentially algorithm "FEASIBLE", from the article:
Yonit Ketsen, Amir Pnueli, Li-on Raviv, Elad Shahar, "Model checking with strong fairness". This implementation is reduced to a module without any fairness requirements.

The line numbers are the line numbers of that algorithm. Read the article for further details.

Returns:

Returns a set of states which induce a graph which contains all the fair SCS's reachable from an initial state.

See Also:

ModuleWithWeakFairness.feasible(), ModuleWithStrongFairness.feasible(), feasible2()

feasible2

public BDD feasible2()

Version which allows justice and compassion requirement to refer to the next state.

Returns:

Returns a set of states which induce a graph which contains all the fair SCS's reachable from an initial state.

See Also:

feasible(), ModuleWithWeakFairness.feasible2(), ModuleWithStrongFairness.feasible2()

yieldStates

public BDD yieldStates(Module responder,
                       BDD to)

A state s in included in the returning result if responder module can force this module to reach a state in "to".
That is, regardless of how this module will move from the result, the responder module can choose an appropriate move into "to".

Parameters:

responder - The module which moves (i.e. this is the responder).

to - The states to reach.

Returns:

The states which can be controlled by this module.

See Also:

allPred(BDD)

controlStates

public BDD controlStates(Module responder,
                         BDD to)

A state s is included in the returning result if the this module can force the responder to reach a state in "to".

Parameters:

responder - The module to check for.

to - The states to reach.

Returns:

The states which can be controlled by this module.

elimSuccChains

public BDD elimSuccChains(BDD scc)

Eliminate states from scc which have no successors within scc. scc is supposed to be a strongly connected component, however, it also contains chains of states which exit the scc, but are not in it. This procedure eliminates these chains.

Parameters:

scc - The set of states to find scc for.

Returns:

The scc of the given set of states.

hasSuccessorsTo

public BDD hasSuccessorsTo(BDD state,
                           BDD to)

Get the subset of states which has successor to the other given set of states.

Parameters:

state - The first set of states.

to - The second set of states.

Returns:

the subset of "state" which has successors to "to".

toString

public abstract java.lang.String toString()

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

Overrides:

toString in class java.lang.Object

Returns:

A string describing the module.

getPath

public abstract java.lang.String getPath()

The path leading to this module.

Returns:

The path leading to this module.

getName

public abstract java.lang.String getName()

Getter for the declared field name which holds this instance.

Returns:

The declared field name which holds this instance.

getFullInstName

public abstract java.lang.String getFullInstName()

Getter for the instance string.

Returns:

The instance string.