edu.wis.jtlv.old_lib.mc
Class CTLModelChecker

java.lang.Object
  edu.wis.jtlv.old_lib.mc.ModelChecker
      edu.wis.jtlv.old_lib.mc.CTLModelChecker

public class CTLModelChecker
extends ModelChecker

A wrapper to a SMVModule which knows how to check CTL properties for the given module.

checking CTL with fairness based on Li-On's algorithm. These have been checked (with TLV) on the dining philosophers problem for various number of philosophers (up to 9).

Fairness:
ce_fair_g(p): handles both justice and compassion using Lions algorithm
EfX(p), EfU(,q), EfG(p), EfF(p), AfX(p), AfU(p,q), AfG(p), AfF(p) ( justice only )
agptoafq(p,q): states satisfying AG(p --> AF q) over fair paths

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

CTLModelChecker(SMVModule design)

CTLModelChecker(SMVModule design, boolean removeRunningVar)

Method Summary

void	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	modelCheckStandardOutput(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.

Methods inherited from class edu.wis.jtlv.old_lib.mc.ModelChecker

getDesign

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

CTLModelChecker

public CTLModelChecker(SMVModule design)
                throws ModelCheckException

Throws:

ModelCheckException

CTLModelChecker

public CTLModelChecker(SMVModule design,
                       boolean removeRunningVar)
                throws ModelCheckException

Throws:

ModelCheckException

Method Detail

modelCheckStandardOutput

public void modelCheckStandardOutput(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. whether all the computations of the design satisfy \phi. This variant of implementation, prints the results to the standard streams.

Parameters:

property - The property to check.

See Also:

modelCheck(Spec)

modelCheck

public void modelCheck(Spec property)
                throws ModelCheckException,
                       CounterExampleException

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. whether all the computations of the design satisfy \phi.

Parameters:

property - The property to check.

Throws:

ModelCheckException - When the method is initiated with other then CTL property.

CounterExampleException - When the property is not valid, a counter example is thrown.

See Also:

modelCheckStandardOutput(Spec)