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

Author:

yaniv sa'ar.

See Also:

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

Constructor Summary

Module()

Method Summary

abstract void	addInitial(net.sf.javabdd.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.
net.sf.javabdd.BDD	allPred(net.sf.javabdd.BDD to) Given a set of state, this procedure return all states which can lead in any number of module steps to these states.
net.sf.javabdd.BDD	allSucc(net.sf.javabdd.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	conjunctTrans(net.sf.javabdd.BDD to_add) Conjunct the transition relation with the given condition.
net.sf.javabdd.BDD	controlStates(Module responder, net.sf.javabdd.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	disjunctTrans(net.sf.javabdd.BDD to_add) Disjunct the transition relation with the given condition.
net.sf.javabdd.BDD	elimSuccChains(net.sf.javabdd.BDD scc) Eliminate states from scc which have no successors within scc.
net.sf.javabdd.BDD	feasible() This is essentially algorithm "FEASIBLE", from the article: Yonit Ketsen, Amir Pnueli, Li-on Raviv, Elad Shahar, "Model checking with strong fairness".
net.sf.javabdd.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<net.sf.javabdd.BDD>	getAllIniRestrictions()
abstract java.util.Vector<net.sf.javabdd.BDD>	getAllTransRestrictions()
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.
net.sf.javabdd.BDD	hasSuccessorsTo(net.sf.javabdd.BDD state, net.sf.javabdd.BDD to)
abstract net.sf.javabdd.BDD	idleStep() Construct a BDD representing the idle transition of this module.
abstract net.sf.javabdd.BDD	initial() Getter for the initial states in the module.
abstract net.sf.javabdd.BDDVarSet	modulePrimeVars() Getter for the primed variable of this module.
abstract net.sf.javabdd.BDDVarSet	moduleUnprimeVars() Getter for the unprimed variable of this module.
net.sf.javabdd.BDDVarSet	moduleVars() Getter for all, primed and unprimed variable of this module.
net.sf.javabdd.BDD	pred(net.sf.javabdd.BDD to) Given a set of state, this procedure return all states which can lead in a single module step to these states.
net.sf.javabdd.BDD	reachable()
abstract void	removeAllIniRestrictions()
abstract void	removeAllTransRestrictions()
abstract void	removeIniRestriction(int id)
abstract void	removeTransRestriction(int id)
abstract int	restrictIni(net.sf.javabdd.BDD temp_ini)
abstract int	restrictTrans(net.sf.javabdd.BDD temp_trans)
abstract void	setAllIniRestrictions(java.util.Vector<net.sf.javabdd.BDD> toSet)
abstract void	setAllTransRestrictions(java.util.Vector<net.sf.javabdd.BDD> toSet)
abstract void	setInitial(net.sf.javabdd.BDD to_add) Set the initial condition with the given condition.
net.sf.javabdd.BDD[]	shortestPath(net.sf.javabdd.BDD source, net.sf.javabdd.BDD dest) Compute the shortest path from source to destination.
net.sf.javabdd.BDD	succ(net.sf.javabdd.BDD from) This procedure return all states which the module can reach in a single step from given a set of state.
abstract java.lang.String	toString() Prepare a string describing the module, its variables, define, statement, etc.
abstract net.sf.javabdd.BDD	trans() Getter for the transition relation of the module.
net.sf.javabdd.BDD	yieldStates(Module responder, net.sf.javabdd.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(net.sf.javabdd.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(net.sf.javabdd.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(net.sf.javabdd.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(net.sf.javabdd.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 net.sf.javabdd.BDDVarSet modulePrimeVars()

Getter for the primed variable of this module.

Returns:

The primed variables of this module.

moduleUnprimeVars

public abstract net.sf.javabdd.BDDVarSet moduleUnprimeVars()

Getter for the unprimed variable of this module.

Returns:

The unprimed variables of this module.

moduleVars

public net.sf.javabdd.BDDVarSet moduleVars()

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

Returns:

The unprimed variables of this module.

initial

public abstract net.sf.javabdd.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 net.sf.javabdd.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 net.sf.javabdd.BDD idleStep()

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.

Returns:

the idle transition of this module.

See Also:

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

pred

public net.sf.javabdd.BDD pred(net.sf.javabdd.BDD to)
                        throws net.sf.javabdd.BDDException

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.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

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

allPred

public net.sf.javabdd.BDD allPred(net.sf.javabdd.BDD to)
                           throws net.sf.javabdd.BDDException

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.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

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

succ

public net.sf.javabdd.BDD succ(net.sf.javabdd.BDD from)
                        throws net.sf.javabdd.BDDException

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.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

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

allSucc

public net.sf.javabdd.BDD allSucc(net.sf.javabdd.BDD from)
                           throws net.sf.javabdd.BDDException

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.

Throws:

net.sf.javabdd.BDDException - If there was a problem with the BDD operation.

See Also:

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

restrictIni

public abstract int restrictIni(net.sf.javabdd.BDD temp_ini)

removeIniRestriction

public abstract void removeIniRestriction(int id)

removeAllIniRestrictions

public abstract void removeAllIniRestrictions()

getAllIniRestrictions

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

setAllIniRestrictions

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

restrictTrans

public abstract int restrictTrans(net.sf.javabdd.BDD temp_trans)

removeTransRestriction

public abstract void removeTransRestriction(int id)

removeAllTransRestrictions

public abstract void removeAllTransRestrictions()

getAllTransRestrictions

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

setAllTransRestrictions

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

reachable

public net.sf.javabdd.BDD reachable()

shortestPath

public net.sf.javabdd.BDD[] shortestPath(net.sf.javabdd.BDD source,
                                         net.sf.javabdd.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

feasible

public net.sf.javabdd.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 net.sf.javabdd.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 net.sf.javabdd.BDD yieldStates(Module responder,
                                      net.sf.javabdd.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 net.sf.javabdd.BDD controlStates(Module responder,
                                        net.sf.javabdd.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 net.sf.javabdd.BDD elimSuccChains(net.sf.javabdd.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 net.sf.javabdd.BDD hasSuccessorsTo(net.sf.javabdd.BDD state,
                                          net.sf.javabdd.BDD to)

Parameters:

state -

to -

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.