edu.wis.jtlv.lib.mc
Class SimpleTempEntailAlg

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

All Implemented Interfaces:

AlgI

Direct Known Subclasses:

SimpleReactAlg

public class SimpleTempEntailAlg
extends ModelCheckAlgI

An algorithm for performing the temp entailment check.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

SimpleTempEntailAlg(Module design, Spec p, Spec q)
A constructor for the temp entailment algorithm.

Method Summary

AlgResultI	doAlgorithm() Verify whether [](p -> <>q) is valid.
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

SimpleTempEntailAlg

public SimpleTempEntailAlg(Module design,
                           Spec p,
                           Spec q)

A constructor for the temp entailment algorithm.

Parameters:

design - The design to check the property for.

p - The first property.

q - The second 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

Verify whether [](p -> <>q) is valid.

Returns:

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

Throws:

AlgExceptionI - If one of the properties 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()