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

M

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

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 GRGamesMain

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

modelCheck(Spec) - Method in class edu.wis.jtlv.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.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.

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

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

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

An exception dedicated for all kind of model checking issues.

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

ModelCheckingTest - Class in <Unnamed>

ModelCheckingTest() - Constructor for class ModelCheckingTest

modelCheckStandardOutput(Spec) - Method in class edu.wis.jtlv.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.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.lib.mc.LTLModelChecker

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

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

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

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