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 _

C

calculate_strategy(int) - Method in class edu.wis.jtlv.lib.games.GR1GameAlg

Extracting an implementation from the set of possible strategies with the given priority to the next step.

calculate_strategy(int) - Method in class edu.wis.jtlv.old_lib.games.GR1Game

Extracting an implementation from the set of possible strategies with the given priority to the next step.

checkDeadlock() - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

Deadlocked states are those whose only successor is them-self.

checkDeadlockStrandardOutput() - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

Deadlocked states are those whose only successor is them-self.

checkInvariance(Spec) - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

The invariance procedure check that a property holds on all reachable states.

checkInvarianceStrandardOutput(Spec) - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

The invariance procedure check that a property holds on all reachable states.

checkReact(Spec, Spec[], Spec) - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.

checkReactStrandardOutput(Spec, Spec[], Spec) - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.

checkTempEntail(Spec, Spec) - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

Verify whether [](p -> <>q) is valid.

checkTempEntailStrandardOutput(Spec, Spec) - Method in class edu.wis.jtlv.old_lib.mc.SimpleModelChecker

Verify whether [](p -> <>q) is valid.

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

Clears the entire listeners queue.

comparable(ModuleBDDField) - Method in class edu.wis.jtlv.env.module.ModuleBDDField

Check whether this object's domain is comparable to the give object domain.

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

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

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

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

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

Conjunct the transition relation with the given condition.

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

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

Check whether the given BDD contains a prime version of some field.

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

Check whether the given BDD contains an unprime version of some field.

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

A state s is included in the returning result if the this module can force the responder to reach a state in "to".

copy(Memory.Permutation) - Method in class edu.wis.jtlv.old_lib.games.Memory.Permutation

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

Copy a given BDD into the base BDD manager.

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

Copy a given BDD into a given BDD manager.

copyBDDVarSetIntoBaseManager(BDDVarSet) - Static method in class edu.wis.jtlv.env.Env

Copy a given BDDVarSet into the base BDD manager.

copyBDDVarSetIntoManager(int, BDDVarSet) - Static method in class edu.wis.jtlv.env.Env

Copy a given BDDVarSet into a given BDD manager.

CounterExampleException - Exception in edu.wis.jtlv.old_lib.mc

An exception dedicated for counter examples.

CounterExampleException(String, BDD[]) - Constructor for exception edu.wis.jtlv.old_lib.mc.CounterExampleException

ctlCheck() - Static method in class AlgorithmRunnerMain

ctlCheck() - Static method in class ModelCheckingTest

CTLModelCheckAlg - Class in edu.wis.jtlv.lib.mc.tl

An implementation for CTL model checking.

CTLModelCheckAlg(ModuleWithStrongFairness, Spec) - Constructor for class edu.wis.jtlv.lib.mc.tl.CTLModelCheckAlg

CTLModelChecker - Class in edu.wis.jtlv.old_lib.mc

A wrapper to a SMVModule which knows how to check CTL properties for the given module.

CTLModelChecker(SMVModule) - Constructor for class edu.wis.jtlv.old_lib.mc.CTLModelChecker

CTLModelChecker(SMVModule, boolean) - Constructor for class edu.wis.jtlv.old_lib.mc.CTLModelChecker

CTLOp - Static variable in enum edu.wis.jtlv.env.spec.Operator