edu.wis.jtlv.env.module
Class ModuleWithStrongFairness

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

Direct Known Subclasses:

SMVModule

public abstract class ModuleWithStrongFairness
extends ModuleWithWeakFairness

A general interface for module with strong fairness (compassion).
I.e. for every computation sigma, if sigma contains infinite many p, then it also contains infinite many q states

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

ModuleWithStrongFairness()

Method Summary

abstract void	addCompassion(BDD p, BDD q) Add strong (compassion) winning condition to the module.
abstract BDD[]	allPCompassion() Getter for all the p's, of the compassion requirements of the module.
abstract BDD[]	allQCompassion() Getter for all the q's, of the compassion requirements of the module.
abstract int	compassionNum() Getter for the number of compassion condition defined in 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	pCompassionAt(int i) Getter for a P part of the compassion condition defined at the given index in the module.
abstract BDD[]	popLastCompassion() Removes the last compassion added to this module.
abstract BDD	qCompassionAt(int i) Getter for a Q part of the compassion condition defined at the given index in the module.

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

addJustice, allJustice, justiceAt, justiceNum, popLastJustice

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

ModuleWithStrongFairness

public ModuleWithStrongFairness()

Method Detail

addCompassion

public abstract void addCompassion(BDD p,
                                   BDD q)
                            throws ModuleException

Add strong (compassion) winning condition to the module.

Parameters:

p - The p winning condition to add to the module.

q - The q winning condition to add to the module.

Throws:

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

See Also:

popLastCompassion(), compassionNum(), pCompassionAt(int), qCompassionAt(int), allPCompassion(), allQCompassion()

popLastCompassion

public abstract BDD[] popLastCompassion()

Removes the last compassion added to this module.

Returns:

An array of two BDDs with the removed compassion.

See Also:

addCompassion(BDD, BDD), compassionNum(), pCompassionAt(int), qCompassionAt(int), allPCompassion(), allQCompassion()

compassionNum

public abstract int compassionNum()

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

Returns:

The number of compassion condition defined in the module.

See Also:

addCompassion(BDD, BDD), popLastCompassion(), pCompassionAt(int), qCompassionAt(int), allPCompassion(), allQCompassion()

pCompassionAt

public abstract BDD pCompassionAt(int i)

Getter for a P part of the compassion condition defined at the given index in the module.

Parameters:

i - The index of the compassion condition to return.

Returns:

The P part of the compassion condition defined defined at the given index in the module.

See Also:

addCompassion(BDD, BDD), popLastCompassion(), compassionNum(), qCompassionAt(int), allPCompassion(), allQCompassion()

qCompassionAt

public abstract BDD qCompassionAt(int i)

Getter for a Q part of the compassion condition defined at the given index in the module.

Parameters:

i - The index of the compassion condition to return.

Returns:

The Q part of the compassion condition defined defined at the given index in the module.

See Also:

addCompassion(BDD, BDD), popLastCompassion(), compassionNum(), pCompassionAt(int), allPCompassion(), allQCompassion()

allPCompassion

public abstract BDD[] allPCompassion()

Getter for all the p's, of the compassion requirements of the module.

Returns:

The p's part of the compassion requirements.

See Also:

addCompassion(BDD, BDD), popLastCompassion(), compassionNum(), pCompassionAt(int), qCompassionAt(int), allQCompassion()

allQCompassion

public abstract BDD[] allQCompassion()

Getter for all the q's, of the compassion requirements of the module.

Returns:

The q's part of the compassion requirements.

See Also:

addCompassion(BDD, BDD), popLastCompassion(), compassionNum(), pCompassionAt(int), qCompassionAt(int), allPCompassion()

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

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

Overrides:

feasible in class ModuleWithWeakFairness

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(), ModuleWithWeakFairness.feasible()

feasible2

public BDD feasible2()

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

Overrides:

feasible2 in class ModuleWithWeakFairness

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