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

Packages that use ModelCheckException

edu.wis.jtlv.old_lib.mc

The old library containing model checking algorithms.

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

Subclasses of ModelCheckException in edu.wis.jtlv.old_lib.mc

class

CounterExampleException An exception dedicated for counter examples.

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

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.
BDD	LTLModelChecker.LTLTesterBuilder.getSpec2BDD(Spec root)
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.
static void	LTLModelChecker.standAloneValid(Spec property) Check validity for a given LTL property without any design attached.
void	LTLModelChecker.valid(Spec property) Check validity for a given LTL property.

Constructors in edu.wis.jtlv.old_lib.mc that throw ModelCheckException

CTLModelChecker(SMVModule design)

CTLModelChecker(SMVModule design, boolean removeRunningVar)

LTLModelChecker.LTLTesterBuilder(Spec root_spec, boolean isWeak)

LTLModelChecker(SMVModule design)

LTLModelChecker(SMVModule design, boolean removeRunningVar)

ModelChecker(SMVModule design, boolean removeRunningVar)

SimpleModelChecker(SMVModule design)

SimpleModelChecker(SMVModule design, boolean removeRunningVar)