A B C D E F G H I J K L M N O P Q R S T U V X Y Z _

A

addCompassion(BDD, BDD) - Method in class edu.wis.jtlv.env.module.ModuleWithStrongFairness

Add strong (compassion) winning condition to the module.

addCompassion(BDD, BDD) - Method in class edu.wis.jtlv.env.module.SMVModule

addInitial(BDD) - Method in class edu.wis.jtlv.env.module.FDSModule

addInitial(BDD) - Method in class edu.wis.jtlv.env.module.Module

Conjunct the initial condition with the given condition.

addInitial(BDD) - Method in class edu.wis.jtlv.env.module.SMVModule

addInstanceVar(SMVModule, boolean) - Method in class edu.wis.jtlv.env.module.SMVModule

Add a module instance as a variable to this module.

addJustice(BDD) - Method in class edu.wis.jtlv.env.module.FDSModule

addJustice(BDD) - Method in class edu.wis.jtlv.env.module.ModuleWithWeakFairness

Add weak (justice) winning condition to the module.

addJustice(BDD) - Method in class edu.wis.jtlv.env.module.SMVModule

addVar(String) - Method in class edu.wis.jtlv.env.module.FDSModule

addVar(String) - Method in class edu.wis.jtlv.env.module.Module

Add a variable to the module.

addVar(String) - Method in class edu.wis.jtlv.env.module.SMVModule

addVar(String, String[]) - Method in class edu.wis.jtlv.env.module.SMVModule

Add a set of values variable to this module.

addVar(String, int, int) - Method in class edu.wis.jtlv.env.module.SMVModule

Add a range variable to this module.

adjustBDDToBase(BDD) - Method in class edu.wis.jtlv.env.JTLVThread

Copy the BDD from this manager to the base manager.

adjustBDDToBase(BDD[]) - Method in class edu.wis.jtlv.env.JTLVThread

Copy an array of BDDs from this manager to the base manager.

adjustBDDToManager(BDD) - Method in class edu.wis.jtlv.env.JTLVThread

Copy the BDD to the manager assigned to this thread.

adjustBDDToManager(BDD[]) - Method in class edu.wis.jtlv.env.JTLVThread

Copy an array of BDDs to the manager assigned to this thread.

adjustBDDVarSetToBase(BDDVarSet) - Method in class edu.wis.jtlv.env.JTLVThread

Copy the BDDVarSet from this manager to the base manager.

adjustBDDVarSetToBase(BDDVarSet[]) - Method in class edu.wis.jtlv.env.JTLVThread

Copy an array of BDDVarSets from this manager to the base manager.

adjustBDDVarSetToManager(BDDVarSet) - Method in class edu.wis.jtlv.env.JTLVThread

Copy the BDDVarSet to the manager assigned to this thread.

adjustBDDVarSetToManager(BDDVarSet[]) - Method in class edu.wis.jtlv.env.JTLVThread

Copy an array of BDDVarSets to the manager assigned to this thread.

advance(T) - Method in class edu.wis.jtlv.lib.FixPoint

Given the element to fix-point on, determine whether it has changed since the last time a check was performed.

AlgExceptionI - Exception in edu.wis.jtlv.lib

A general abstract class for any kind of exception.

AlgExceptionI() - Constructor for exception edu.wis.jtlv.lib.AlgExceptionI

AlgExceptionI(String, Throwable) - Constructor for exception edu.wis.jtlv.lib.AlgExceptionI

AlgExceptionI(String) - Constructor for exception edu.wis.jtlv.lib.AlgExceptionI

AlgExceptionI(Throwable) - Constructor for exception edu.wis.jtlv.lib.AlgExceptionI

AlgI - Interface in edu.wis.jtlv.lib

Implement your algorithm, use or ignore what ever phases that you'd like.

AlgorithmRunnerMain - Class in <Unnamed>

AlgorithmRunnerMain() - Constructor for class AlgorithmRunnerMain

AlgResultBDD - Class in edu.wis.jtlv.lib

BDD results.

AlgResultBDD(boolean, BDD) - Constructor for class edu.wis.jtlv.lib.AlgResultBDD

A constructor for a BDD results, with a general flag is was successful.

AlgResultBDD(AlgResultI.ResultStatus, BDD) - Constructor for class edu.wis.jtlv.lib.AlgResultBDD

A constructor for a BDD results, with a general flag is was successful.

AlgResultBDD(BDD) - Constructor for class edu.wis.jtlv.lib.AlgResultBDD

A constructor for a BDD results, without successfulness status.

AlgResultBoolean - Class in edu.wis.jtlv.lib

Boolean results.

AlgResultBoolean(boolean, boolean) - Constructor for class edu.wis.jtlv.lib.AlgResultBoolean

A constructor for a Boolean results, with a general flag is was successful.

AlgResultBoolean(AlgResultI.ResultStatus, boolean) - Constructor for class edu.wis.jtlv.lib.AlgResultBoolean

A constructor for a Boolean results, with a general flag is was successful.

AlgResultBoolean(boolean) - Constructor for class edu.wis.jtlv.lib.AlgResultBoolean

A constructor for a Boolean results, without successfulness status.

AlgResultI - Interface in edu.wis.jtlv.lib

Implement the resulting object, as a string, and as what ever object that you'd like.

AlgResultI.ResultStatus - Enum in edu.wis.jtlv.lib

A general flag for the results status.

AlgResultModule - Class in edu.wis.jtlv.lib

Module results.

AlgResultModule(boolean, Module) - Constructor for class edu.wis.jtlv.lib.AlgResultModule

A constructor for a module results, with a general flag is was successful.

AlgResultModule(AlgResultI.ResultStatus, Module) - Constructor for class edu.wis.jtlv.lib.AlgResultModule

A constructor for a module results, with a general flag is was successful.

AlgResultModule(Module) - Constructor for class edu.wis.jtlv.lib.AlgResultModule

A constructor for a module results, without successfulness status.

AlgResultPath - Class in edu.wis.jtlv.lib

BDD array results (Path).

AlgResultPath(boolean, BDD[]) - Constructor for class edu.wis.jtlv.lib.AlgResultPath

A constructor for a path results, with a general flag is was successful.

AlgResultPath(AlgResultI.ResultStatus, BDD[]) - Constructor for class edu.wis.jtlv.lib.AlgResultPath

A constructor for a path results, with a general flag is was successful.

AlgResultPath(BDD[]) - Constructor for class edu.wis.jtlv.lib.AlgResultPath

A constructor for a path results, without successfulness status.

AlgResultString - Class in edu.wis.jtlv.lib

String results.

AlgResultString(boolean, String) - Constructor for class edu.wis.jtlv.lib.AlgResultString

A constructor for a String results, with a general flag is was successful.

AlgResultString(AlgResultI.ResultStatus, String) - Constructor for class edu.wis.jtlv.lib.AlgResultString

A constructor for a String results, with a general flag is was successful.

AlgResultString(String) - Constructor for class edu.wis.jtlv.lib.AlgResultString

A constructor for a String results, without successfulness status.

AlgRunnerThread - Class in edu.wis.jtlv.lib

A runner thread to execute any kind of algorithm, which implemented the AlgI scheme.

AlgRunnerThread(AlgI) - Constructor for class edu.wis.jtlv.lib.AlgRunnerThread

A constructor for an algorithm runner.

all_error_listeners - Static variable in class edu.wis.jtlv.env.Env

A list of all error listeners which are invoked on any kind of error in the system.

allDeltaPred(BDD, BDD) - Static method in class edu.wis.jtlv.env.Env

Given a set of state and a transitions, the procedure return all states which can lead in any number of steps to given states, excluding the given states themselves (in some cases this might be more efficient the allPred, and then conjuncting out the negation).

allDeltaSucc(BDD, BDD) - Static method in class edu.wis.jtlv.env.Env

Given a set of state and a transitions, the procedure return all states which can be reached in any number of steps from these states, excluding the given states themselves (in some cases this might be more efficient the allSucc, and then conjuncting out the negation).

allJustice() - Method in class edu.wis.jtlv.env.module.FDSModule

allJustice() - Method in class edu.wis.jtlv.env.module.ModuleWithWeakFairness

Getter for all the justice requirements of the module.

allJustice() - Method in class edu.wis.jtlv.env.module.SMVModule

allPCompassion() - Method in class edu.wis.jtlv.env.module.ModuleWithStrongFairness

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

allPCompassion() - Method in class edu.wis.jtlv.env.module.SMVModule

allPred(BDD, BDD) - Static method in class edu.wis.jtlv.env.Env

Given a set of state and a transitions, the procedure return all states which can lead in any number of steps to given states.

allPred(BDD) - Method in class edu.wis.jtlv.env.module.Module

Given a set of state, this procedure return all states which can lead in any number of module steps to these states.

allQCompassion() - Method in class edu.wis.jtlv.env.module.ModuleWithStrongFairness

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

allQCompassion() - Method in class edu.wis.jtlv.env.module.SMVModule

allSucc(BDD, BDD) - Static method in class edu.wis.jtlv.env.Env

Given a set of state and a transitions, the procedure return all states which can be reached in a any number of steps from these states.

allSucc(BDD) - Method in class edu.wis.jtlv.env.module.Module

This procedure return all states which the module can reach in any number of steps from given a set of state.

assignDedicatedBDDManagerIdx(JTLVThread) - Static method in class edu.wis.jtlv.env.Env

A procedure called from within JTLVThread which allocates and assign a manager to the given thread.

asyncComposition(Module) - Method in class edu.wis.jtlv.env.module.FDSModule

This functionality is not implemented for FDSModule yet.

asyncComposition(Module) - Method in class edu.wis.jtlv.env.module.Module

add asynchronous composition to this module.

asyncComposition(Module) - Method in class edu.wis.jtlv.env.module.SMVModule

attachStmt(StmtDefineOperator) - Method in class edu.wis.jtlv.env.module.ModuleBDDDefine

Attach an expression to the define.