Uses of Class
edu.wis.jtlv.old_lib.mc.CounterExampleException

Packages that use CounterExampleException

edu.wis.jtlv.old_lib.mc

The old library containing model checking algorithms.

Uses of CounterExampleException in edu.wis.jtlv.old_lib.mc

Methods in edu.wis.jtlv.old_lib.mc that throw CounterExampleException

void	SimpleModelChecker.checkDeadlock() Deadlocked states are those whose only successor is them-self.
void	SimpleModelChecker.checkInvariance(Spec property) The invariance procedure check that a property holds on all reachable states.
void	SimpleModelChecker.checkReact(Spec p, Spec[] q, Spec r) Verify whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.
void	SimpleModelChecker.checkTempEntail(Spec p, Spec q) Verify whether [](p -> <>q) is valid.
void	CTLModelChecker.modelCheck(Spec property) 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.
void	LTLModelChecker.modelCheck(Spec property) 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.
void	LTLModelChecker.modelCheckTester(SMVModule user_tester) To compose a tester with the design, and perform model checking.