edu.wis.jtlv.env.module
Class ModuleWithWeakFairness

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

Direct Known Subclasses:

FDSModule, ModuleWithStrongFairness

public abstract class ModuleWithWeakFairness
extends Module

A general interface for module with weak fairness (justice).
I.e. every computation sigma contains infinite many justice states.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

ModuleWithWeakFairness()

Method Summary

abstract void	addJustice(BDD to_add) Add weak (justice) winning condition to the module.
abstract BDD[]	allJustice() Getter for all the justice requirements of the module.
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 BDD	justiceAt(int i) Getter for a justice condition defined at the given index in the module.
abstract int	justiceNum() Getter for the number of justice condition defined in the module.
abstract BDD	popLastJustice() Removes the last justice added to this module.

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

addInitial, addVar, allPred, allSucc, asyncComposition, conjunctTrans, controlStates, decompose, disjunctTrans, elimSuccChains, getAllFields, getAllIniRestrictions, getAllTransRestrictions, getFullInstName, getName, getPath, hasSuccessorsTo, idleStep, initial, modulePrimeVars, moduleUnprimeVars, moduleVars, pred, reachable, removeAllIniRestrictions, removeAllTransRestrictions, removeIniRestriction, removeTransRestriction, restrictIni, restrictTrans, setAllIniRestrictions, setAllTransRestrictions, setInitial, shortestPath, succ, syncComposition, toString, trans, yieldStates

Methods inherited from class java.lang.Object

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

Constructor Detail

ModuleWithWeakFairness

public ModuleWithWeakFairness()

Method Detail

addJustice

public abstract void addJustice(BDD to_add)
                         throws ModuleException

Add weak (justice) winning condition to the module.

Parameters:

to_add - The winning condition to add to the module.

Throws:

ModuleException - If there was a problem with adding the condition.

See Also:

justiceNum(), justiceAt(int), popLastJustice(), allJustice()

popLastJustice

public abstract BDD popLastJustice()

Removes the last justice added to this module.

Returns:

The removed justice.

See Also:

addJustice(BDD), justiceNum(), justiceAt(int), allJustice()

justiceNum

public abstract int justiceNum()

Getter for the number of justice condition defined in the module.

Returns:

The number of justice condition defined in the module.

See Also:

addJustice(BDD), justiceAt(int), popLastJustice(), allJustice()

justiceAt

public abstract BDD justiceAt(int i)

Getter for a justice condition defined at the given index in the module.

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:

addJustice(BDD), justiceNum(), popLastJustice(), allJustice()

allJustice

public abstract BDD[] allJustice()

Getter for all the justice requirements of the module.

Returns:

The justice requirements.

See Also:

addJustice(BDD), justiceNum(), justiceAt(int), popLastJustice()

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 with only weak fairness requirements.

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

Overrides:

feasible in class Module

Returns:

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

See Also:

Module.feasible(), ModuleWithStrongFairness.feasible()

feasible2

public BDD feasible2()

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

Overrides:

feasible2 in class Module

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(), Module.feasible2(), ModuleWithStrongFairness.feasible2()