edu.wis.jtlv.lib.mc.tl
Class CTLModelCheckAlg

java.lang.Object
  edu.wis.jtlv.lib.mc.ModelCheckAlgI
      edu.wis.jtlv.lib.mc.tl.CTLModelCheckAlg

All Implemented Interfaces:

AlgI

public class CTLModelCheckAlg
extends ModelCheckAlgI

An implementation for CTL model checking.

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

CTLModelCheckAlg(ModuleWithStrongFairness design, Spec property)

Method Summary

AlgResultI	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	postAlgorithm() Does nothing.
AlgResultI	preAlgorithm() Check that the property is a CTL property.

Methods inherited from class java.lang.Object

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

Constructor Detail

CTLModelCheckAlg

public CTLModelCheckAlg(ModuleWithStrongFairness design,
                        Spec property)

Method Detail

preAlgorithm

public AlgResultI preAlgorithm()
                        throws AlgExceptionI

Check that the property is a CTL property.

Returns:

Nothing.

Throws:

AlgExceptionI - If The specification is not a CTL specification.

See Also:

AlgI.preAlgorithm()

doAlgorithm

public AlgResultI doAlgorithm()
                       throws AlgExceptionI

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.

Returns:

a string result with "VALID", or "NOT VALID" (i.e. AlgResultString).

Throws:

ModelCheckAlgException - When cannot identify one of the operators.

AlgExceptionI - Wherever the algorithm implementor choose to.

See Also:

AlgI.postAlgorithm()

postAlgorithm

public AlgResultI postAlgorithm()
                         throws AlgExceptionI

Does nothing.

Returns:

Nothing.

Throws:

AlgExceptionI - Never.

See Also:

AlgI.postAlgorithm()