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 _

D

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

Parse the given file, add it to the system, and pops a window browser with the parsing tree which the parser read.

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

This functionality is not implemented for FDSModule yet.

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

remove composition from this module.

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

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

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

Disjunct the transition relation with the given condition.

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

doAlgorithm() - Method in interface edu.wis.jtlv.lib.AlgI

The main algorithm phase.

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

performing the GR 1 game itself, and collecting all memory.

doAlgorithm() - Method in class edu.wis.jtlv.lib.games.RkGameAlg

performing the GR 1 game itself, and collecting all memory.

doAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleDeadlockAlg

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

doAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleInvarianceAlg

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

doAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleReactAlg

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

doAlgorithm() - Method in class edu.wis.jtlv.lib.mc.SimpleTempEntailAlg

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

doAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.CTLModelCheckAlg

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.

doAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.LTLModelCheckAlg

Compose the design with the tester (user's or the one built from the LTL specification), and check feasible states.

doAlgorithm() - Method in class edu.wis.jtlv.lib.mc.tl.LTLValidAlg

Check validity for a given LTL property.

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

Invoke the listeners queue with the given exception.

doError(Exception, String) - Method in interface edu.wis.jtlv.env.ErrorListener

domain_has_module_value(SMVModule, BDDDomain, String) - Method in class edu.wis.jtlv.env.Env.JTLVBDDToString

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

Register a procedure to be done at every garbage collection.

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

Register a procedure to be done at every reorder to the BDD table.

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

Register a procedure to be done at every resize to the BDD table.