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 _

M

m_Streett(BDD, BDD) - Method in class edu.wis.jtlv.old_lib.games.RkGame

Macro - Interface in edu.wis.jtlv.env.spec

A NOT YET IMPLEMENTED, general Macro interface for converting specifications.

main(String[]) - Static method in class AlgorithmRunnerMain

main(String[]) - Static method in class FDSFileConstructionTest

main run for the game.

main(String[]) - Static method in class FileConstructionTest

main run for the game.

main(String[]) - Static method in class GR1GameMain

main run for the game.

main(String[]) - Static method in class ManualConstructionTest

main(String[]) - Static method in class ModelCheckingTest

main(String[]) - Static method in class SpecManualTest

ManualConstructionTest - Class in <Unnamed>

ManualConstructionTest() - Constructor for class ManualConstructionTest

mem - Variable in class edu.wis.jtlv.old_lib.games.MyPair

Memory - Class in edu.wis.jtlv.old_lib.games

This class is intended to serve as the data structure for holding BDDs in the recursive game (Streett game).

Memory() - Constructor for class edu.wis.jtlv.old_lib.games.Memory

Memory(Set<RkGame.ImplicationEntity>) - Constructor for class edu.wis.jtlv.old_lib.games.Memory

Memory.Permutation - Class in edu.wis.jtlv.old_lib.games

Memory.Permutation(int) - Constructor for class edu.wis.jtlv.old_lib.games.Memory.Permutation

modelCheck(Spec) - Method in class edu.wis.jtlv.old_lib.mc.CTLModelChecker

Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.

modelCheck(Spec) - Method in class edu.wis.jtlv.old_lib.mc.LTLModelChecker

Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.

ModelCheckAlgCounterExampleException - Exception in edu.wis.jtlv.lib.mc

An exception dedicated for counter examples.

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

ModelCheckAlgException - Exception in edu.wis.jtlv.lib.mc

An exception dedicated for all kind of model checking issues.

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

ModelCheckAlgI - Class in edu.wis.jtlv.lib.mc

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

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

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

An exception dedicated for all kind of model checking issues.

ModelCheckException(String) - Constructor for exception edu.wis.jtlv.old_lib.mc.ModelCheckException

ModelCheckingTest - Class in <Unnamed>

ModelCheckingTest() - Constructor for class ModelCheckingTest

modelCheckStandardOutput(Spec) - Method in class edu.wis.jtlv.old_lib.mc.CTLModelChecker

Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.

modelCheckStandardOutput(Spec) - Method in class edu.wis.jtlv.old_lib.mc.LTLModelChecker

Given a specification \phi (as a formula in temporal logic) we want to decide whether \phi is valid over finite state program P , i.e.

modelCheckTester(SMVModule) - Method in class edu.wis.jtlv.old_lib.mc.LTLModelChecker

To compose a tester with the design, and perform model checking.

modelCheckTesterStandardOutput(SMVModule) - Method in class edu.wis.jtlv.old_lib.mc.LTLModelChecker

To compose a tester with the design, and perform model checking.

modelCheckWithNoCounterExample(Spec) - Method in class edu.wis.jtlv.old_lib.mc.LTLModelChecker

Module - Class in edu.wis.jtlv.env.module

A general interface for modules.

Module() - Constructor for class edu.wis.jtlv.env.module.Module

ModuleBDDDefine - Class in edu.wis.jtlv.env.module

This object represents a define declaration field.

ModuleBDDDefine(String, String) - Constructor for class edu.wis.jtlv.env.module.ModuleBDDDefine

The main public constructor.

ModuleBDDField - Class in edu.wis.jtlv.env.module

JTLVBDDField is an object representing a field variable in JTLV environment.

ModuleBDDField(BDDDomain, BDDDomain, String, String) - Constructor for class edu.wis.jtlv.env.module.ModuleBDDField

The main public constructor for JTLVBDDField.

ModuleEntity - Class in edu.wis.jtlv.env.module

A common interface from a module BDD entity.

ModuleEntity() - Constructor for class edu.wis.jtlv.env.module.ModuleEntity

ModuleException - Exception in edu.wis.jtlv.env.module

An exception caused by wrong manipulation to a Module.

ModuleException(String) - Constructor for exception edu.wis.jtlv.env.module.ModuleException

ModuleParamHolder - Class in edu.wis.jtlv.env.module

An object representing a parameter to a module.

ModuleParamHolder(SMVModule, String, String) - Constructor for class edu.wis.jtlv.env.module.ModuleParamHolder

The constructor takes as arguments the instance to which he is parameter to, its local name in that instance, and its instantiating (unparsed) string.

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

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

Getter for the primed variable of this module.

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

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

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

Getter for the unprimed variable of this module.

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

ModuleVariableException - Exception in edu.wis.jtlv.env.module

An exception caused by wrong variable naming in a Module.

ModuleVariableException(String) - Constructor for exception edu.wis.jtlv.env.module.ModuleVariableException

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

Getter for all, primed and unprimed variable of this module.

ModuleWithStrongFairness - Class in edu.wis.jtlv.env.module

A general interface for module with strong fairness (compassion).
I.e.

ModuleWithStrongFairness() - Constructor for class edu.wis.jtlv.env.module.ModuleWithStrongFairness

ModuleWithWeakFairness - Class in edu.wis.jtlv.env.module

A general interface for module with weak fairness (justice).
I.e.

ModuleWithWeakFairness() - Constructor for class edu.wis.jtlv.env.module.ModuleWithWeakFairness

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

Do not call the standard copy procedure.

MyPair - Class in edu.wis.jtlv.old_lib.games

MyPair(BDD, Memory) - Constructor for class edu.wis.jtlv.old_lib.games.MyPair