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 _

L

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

Load a BDD from the file system.

loadModule(String, String) - Static method in class edu.wis.jtlv.env.Env

Load a given file into the system with a specified order given by the other file.

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

Load a given file into the system without a specified order (i.e.

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

Load any kind of specification from a file.

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

Load any kind of specification from a given input stream.

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

Load any kind of specification from a string.

local_index(RkGame.ImplicationEntity) - Method in class edu.wis.jtlv.old_lib.games.Memory

ltlCheck() - Static method in class AlgorithmRunnerMain

ltlCheck() - Static method in class ModelCheckingTest

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

There are two methods to use this algorithms:

LTLModelCheckAlg(Module, Spec) - Constructor for class edu.wis.jtlv.lib.mc.tl.LTLModelCheckAlg

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

LTLModelCheckAlg(Module, Module) - Constructor for class edu.wis.jtlv.lib.mc.tl.LTLModelCheckAlg

Constructor for composing a tester with the design, and perform model checking.

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

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

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

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

LTLModelChecker.LTLTesterBuilder - Class in edu.wis.jtlv.old_lib.mc

LTLModelChecker.LTLTesterBuilder(Spec, boolean) - Constructor for class edu.wis.jtlv.old_lib.mc.LTLModelChecker.LTLTesterBuilder

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

Construct a tester for a given LTL specification.

LTLTester(Spec, boolean) - Constructor for class edu.wis.jtlv.lib.mc.tl.LTLTester

Constructor for the tester.

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

Check validity of ltl formula on a given design (or without one).

LTLValidAlg(Spec) - Constructor for class edu.wis.jtlv.lib.mc.tl.LTLValidAlg

A constructor for checking a property without a design.

LTLValidAlg(SMVModule, Spec) - Constructor for class edu.wis.jtlv.lib.mc.tl.LTLValidAlg

A constructor for checking a property on a design.