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

Author:

yaniv sa'ar.

Constructor Summary

ModuleWithStrongFairness()

Method Summary

abstract void	addCompassion(net.sf.javabdd.BDD p, net.sf.javabdd.BDD q) Add strong (compassion) winning condition to the module.
abstract int	compassionNum() Getter for the number of compassion condition defined in the module.
abstract net.sf.javabdd.BDD	pCompassionAt(int i) Getter for a P part of the compassion condition defined at the given index in the module.
abstract net.sf.javabdd.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, justiceAt, justiceNum

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

addInitial, addVar, allPred, allSucc, conjunctTrans, disjunctTrans, getAllFields, getFullInstName, getName, getPath, initial, pred, prime, primeVars, succ, toString, trans, unprime, unprimeVars

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(net.sf.javabdd.BDD p,
                                   net.sf.javabdd.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:

compassionNum(), pCompassionAt(int), qCompassionAt(int)

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), pCompassionAt(int), qCompassionAt(int)

pCompassionAt

public abstract net.sf.javabdd.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), compassionNum(), qCompassionAt(int)

qCompassionAt

public abstract net.sf.javabdd.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), compassionNum(), pCompassionAt(int)