Uses of Class
edu.wis.jtlv.lib.AlgExceptionI

Packages that use AlgExceptionI

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 AlgExceptionI in edu.wis.jtlv.lib

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

AlgExceptionI	AlgRunnerThread.getDoException() Getter for the main run phase exception.
AlgExceptionI	AlgRunnerThread.getPostException() Getter for the post-run phase exception.
AlgExceptionI	AlgRunnerThread.getPreException() Getter for the pre-run phase exception.

Methods in edu.wis.jtlv.lib that throw AlgExceptionI

AlgResultI	AlgI.doAlgorithm() The main algorithm phase.
AlgResultI	AlgI.postAlgorithm() Post algorithm phase.
AlgResultI	AlgI.preAlgorithm() Pre algorithm phase.

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

Subclasses of AlgExceptionI in edu.wis.jtlv.lib.games

class

GameAlgException A general framework for games exception.

Methods in edu.wis.jtlv.lib.games that throw AlgExceptionI

AlgResultI	RkGameAlg.doAlgorithm() performing the GR 1 game itself, and collecting all memory.
AlgResultI	RkGameAlg.postAlgorithm() The post algorithm calculate the synthesizing implementation.
AlgResultI	RkGameAlg.preAlgorithm() Does nothing.

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

Subclasses of AlgExceptionI in edu.wis.jtlv.lib.mc

class	ModelCheckAlgCounterExampleException An exception dedicated for counter examples.
class	ModelCheckAlgException An exception dedicated for all kind of model checking issues.

Methods in edu.wis.jtlv.lib.mc that throw AlgExceptionI

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 AlgExceptionI in edu.wis.jtlv.lib.mc.tl

Methods in edu.wis.jtlv.lib.mc.tl that throw AlgExceptionI

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.