edu.wis.jtlv.lib.mc
Class SimpleInvarianceAlg

java.lang.Object
  edu.wis.jtlv.lib.mc.ModelCheckAlgI
      edu.wis.jtlv.lib.mc.SimpleInvarianceAlg

All Implemented Interfaces:

AlgI

public class SimpleInvarianceAlg
extends ModelCheckAlgI

An algorithm for performing an invariance check.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

SimpleInvarianceAlg(Module design, Spec prop)
A constructor for the invariance algorithm.

Method Summary

AlgResultI	doAlgorithm() The invariance procedure check that a property holds on all reachable states.
AlgResultI	postAlgorithm() Does nothing.
AlgResultI	preAlgorithm() Does nothing.

Methods inherited from class java.lang.Object

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

Constructor Detail

SimpleInvarianceAlg

public SimpleInvarianceAlg(Module design,
                           Spec prop)

A constructor for the invariance algorithm.

Parameters:

design - The design to check the property for.

prop - The property.

Method Detail

preAlgorithm

public AlgResultI preAlgorithm()
                        throws AlgExceptionI

Does nothing.

Returns:

Nothing.

Throws:

AlgExceptionI - Never.

See Also:

AlgI.preAlgorithm()

doAlgorithm

public AlgResultI doAlgorithm()
                       throws AlgExceptionI

The invariance procedure check that a property holds on all reachable states.

Returns:

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

Throws:

AlgExceptionI - If the property is not a propositional spec, or if failed to parse the BDD in the spec.

postAlgorithm

public AlgResultI postAlgorithm()
                         throws AlgExceptionI

Does nothing.

Returns:

Nothing.

Throws:

AlgExceptionI - Never.

See Also:

AlgI.postAlgorithm()