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

Author:

yaniv sa'ar.

Constructor Summary

ModuleWithWeakFairness()

Method Summary

abstract void	addJustice(net.sf.javabdd.BDD to_add) Add weak (justice) winning condition to the module.
abstract net.sf.javabdd.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.

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

ModuleWithWeakFairness

public ModuleWithWeakFairness()

Method Detail

addJustice

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

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)

justiceAt

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