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

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

All Implemented Interfaces:

AlgI

public class LTLModelCheckAlg
extends ModelCheckAlgI

There are two methods to use this algorithms:

1. 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.

2. To compose a tester with the design, and perform model checking. If the composition is feasible then a counter example is thrown.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

LTLModelCheckAlg(Module design, Module user_tester)
Constructor for composing a tester with the design, and perform model checking.

LTLModelCheckAlg(Module design, Spec property)
Constructor for a given specification \phi (as a formula in temporal logic) which we want to decide whether \phi is valid over finite state program P, i.e.

Method Summary

AlgResultI	doAlgorithm() Compose the design with the tester (user's or the one built from the LTL specification), and check feasible states.
AlgResultI	postAlgorithm() If instantiated with a user tester, then returning it to its previous state.
AlgResultI	preAlgorithm() Preparing the LTL tester.

Methods inherited from class java.lang.Object

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

Constructor Detail

LTLModelCheckAlg

public LTLModelCheckAlg(Module design,
                        Spec property)

Constructor for a given specification \phi (as a formula in temporal logic) which 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:

design - The design to check.

property - The property to check.

LTLModelCheckAlg

public LTLModelCheckAlg(Module design,
                        Module user_tester)

Constructor for composing a tester with the design, and perform model checking. If the composition is feasible then a counter example is thrown.

Parameters:

design - The design to check.

user_tester - The user tester.

Method Detail

preAlgorithm

public AlgResultI preAlgorithm()
                        throws AlgExceptionI

Preparing the LTL tester.

Returns:

Nothing.

Throws:

AlgExceptionI - If The specification is not an LTL specification.

See Also:

AlgI.preAlgorithm()

doAlgorithm

public AlgResultI doAlgorithm()
                       throws AlgExceptionI

Compose the design with the tester (user's or the one built from the LTL specification), and check feasible states.

Returns:

A counter example if the algorithm fails (i.e. AlgResultPath), or a string with "VALID" (i.e. AlgResultString).

Throws:

Noting.

AlgExceptionI - Wherever the algorithm implementor choose to.

See Also:

AlgI.doAlgorithm()

postAlgorithm

public AlgResultI postAlgorithm()
                         throws AlgExceptionI

If instantiated with a user tester, then returning it to its previous state.

Returns:

Nothing.

Throws:

AlgExceptionI - Never.

See Also:

AlgI.postAlgorithm()