Uses of Interface
edu.wis.jtlv.lib.AlgResultI

Packages that use AlgResultI

edu.wis.jtlv.lib	The main user library, with all published formal algorithm which where implemented through JTLV.
edu.wis.jtlv.lib.games	The library with all games algorithms which where implemented using JTLV.
edu.wis.jtlv.lib.mc	The library containing all implemented model checking algorithms.
edu.wis.jtlv.lib.mc.tl

Uses of AlgResultI in edu.wis.jtlv.lib

Classes in edu.wis.jtlv.lib that implement AlgResultI

class	AlgResultBDD BDD results.
class	AlgResultBoolean Boolean results.
class	AlgResultModule Module results.
class	AlgResultPath BDD array results (Path).
class	AlgResultString String results.

Methods in edu.wis.jtlv.lib that return AlgResultI

AlgResultI	AlgI.doAlgorithm() The main algorithm phase.
AlgResultI	AlgRunnerThread.getDoResult() Getter for the main run phase results.
AlgResultI	AlgRunnerThread.getPostResult() Getter for the post-run phase results.
AlgResultI	AlgRunnerThread.getPreResult() Getter for the pre-run phase results.
AlgResultI	AlgI.postAlgorithm() Post algorithm phase.
AlgResultI	AlgI.preAlgorithm() Pre algorithm phase.

Uses of AlgResultI in edu.wis.jtlv.lib.games

Methods in edu.wis.jtlv.lib.games that return AlgResultI

AlgResultI	GR1GameAlg.calculate_strategy(int kind) Extracting an implementation from the set of possible strategies with the given priority to the next step.
AlgResultI	GR1GameAlg.doAlgorithm() performing the GR 1 game itself, and collecting all memory.
AlgResultI	RkGameAlg.doAlgorithm() performing the GR 1 game itself, and collecting all memory.
AlgResultI	GR1GameAlg.postAlgorithm() The post algorithm calculate the synthesizing implementation.
AlgResultI	RkGameAlg.postAlgorithm() The post algorithm calculate the synthesizing implementation.
AlgResultI	GR1GameAlg.preAlgorithm() Does nothing.
AlgResultI	RkGameAlg.preAlgorithm() Does nothing.

Uses of AlgResultI in edu.wis.jtlv.lib.mc

Methods in edu.wis.jtlv.lib.mc that return AlgResultI

AlgResultI	SimpleInvarianceAlg.doAlgorithm() The invariance procedure check that a property holds on all reachable states.
AlgResultI	SimpleTempEntailAlg.doAlgorithm() Verify whether [](p -> <>q) is valid.
AlgResultI	SimpleReactAlg.doAlgorithm() Check whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
AlgResultI	SimpleDeadlockAlg.doAlgorithm() Deadlocked states are those whose only successor is them-self.
AlgResultI	SimpleInvarianceAlg.postAlgorithm() Does nothing.
AlgResultI	SimpleTempEntailAlg.postAlgorithm() Does nothing.
AlgResultI	SimpleReactAlg.postAlgorithm() Does Nothing.
AlgResultI	SimpleDeadlockAlg.postAlgorithm() Does nothing.
AlgResultI	SimpleInvarianceAlg.preAlgorithm() Does nothing.
AlgResultI	SimpleTempEntailAlg.preAlgorithm() Does nothing.
AlgResultI	SimpleReactAlg.preAlgorithm() Does Nothing.
AlgResultI	SimpleDeadlockAlg.preAlgorithm() Does nothing.

Uses of AlgResultI in edu.wis.jtlv.lib.mc.tl

Methods in edu.wis.jtlv.lib.mc.tl that return AlgResultI

AlgResultI	LTLValidAlg.doAlgorithm() Check validity for a given LTL property.
AlgResultI	LTLModelCheckAlg.doAlgorithm() Compose the design with the tester (user's or the one built from the LTL specification), and check feasible states.
AlgResultI	CTLModelCheckAlg.doAlgorithm() 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.
AlgResultI	LTLValidAlg.postAlgorithm() Does nothing.
AlgResultI	LTLModelCheckAlg.postAlgorithm() If instantiated with a user tester, then returning it to its previous state.
AlgResultI	CTLModelCheckAlg.postAlgorithm() Does nothing.
AlgResultI	LTLValidAlg.preAlgorithm() Preparing the LTL tester.
AlgResultI	LTLModelCheckAlg.preAlgorithm() Preparing the LTL tester.
AlgResultI	CTLModelCheckAlg.preAlgorithm() Check that the property is a CTL property.