edu.wis.jtlv.lib.mc
Class SimpleDeadlockAlg

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

All Implemented Interfaces:

AlgI

public class SimpleDeadlockAlg
extends ModelCheckAlgI

An algorithm for performing deadlock check.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

SimpleDeadlockAlg(Module design)
A constructor for the deadlock algorithm.

Method Summary

AlgResultI	doAlgorithm() Deadlocked states are those whose only successor is them-self.
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

SimpleDeadlockAlg

public SimpleDeadlockAlg(Module design)

A constructor for the deadlock algorithm.

Parameters:

design - The design to check the property for.

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

Deadlocked states are those whose only successor is them-self. This method checks for the absence of deadlocks in the module.

Returns:

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

Throws:

AlgExceptionI - Never.

postAlgorithm

public AlgResultI postAlgorithm()
                         throws AlgExceptionI

Does nothing.

Returns:

Nothing.

Throws:

AlgExceptionI - Never.

See Also:

AlgI.postAlgorithm()