edu.wis.jtlv.lib.mc
Class SimpleReactAlg

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

All Implemented Interfaces:

AlgI

public class SimpleReactAlg
extends SimpleTempEntailAlg

An algorithm for performing the react check.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

SimpleReactAlg(ModuleWithWeakFairness design, Spec p, Spec[] q, Spec r)
A constructor for the react algorithm.

Method Summary

AlgResultI	doAlgorithm() Check whether []((p /\_{forall i} []<>q[i]) -> <>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

SimpleReactAlg

public SimpleReactAlg(ModuleWithWeakFairness design,
                      Spec p,
                      Spec[] q,
                      Spec r)

A constructor for the react algorithm.

Parameters:

design - The design to check the property for.

p - The first property.

q - An array of mediate properties.

r - The last property.

Method Detail

preAlgorithm

public AlgResultI preAlgorithm()
                        throws AlgExceptionI

Does Nothing.

Specified by:

preAlgorithm in interface AlgI

Overrides:

preAlgorithm in class SimpleTempEntailAlg

Returns:

Nothing.

Throws:

AlgExceptionI - Never.

See Also:

AlgI.preAlgorithm()

doAlgorithm

public AlgResultI doAlgorithm()
                       throws AlgExceptionI

Check whether []((p /\_{forall i} []<>q[i]) -> <>q) is valid.

Specified by:

doAlgorithm in interface AlgI

Overrides:

doAlgorithm in class SimpleTempEntailAlg

Returns:

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

Throws:

ModelCheckAlgException - When the checkReact method is initiated with other then propositional properties.

ModelCheckAlgCounterExampleException - When the checkReact fails, a counter example is thrown.

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

See Also:

SimpleModelChecker.checkReactStrandardOutput(Spec, Spec[], Spec)

postAlgorithm

public AlgResultI postAlgorithm()
                         throws AlgExceptionI

Does Nothing.

Specified by:

postAlgorithm in interface AlgI

Overrides:

postAlgorithm in class SimpleTempEntailAlg

Returns:

Nothing.

Throws:

AlgExceptionI - Never.

See Also:

AlgI.postAlgorithm()