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

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

All Implemented Interfaces:

AlgI

public class LTLValidAlg
extends ModelCheckAlgI

Check validity of ltl formula on a given design (or without one).

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

LTLValidAlg(SMVModule design, Spec property)
A constructor for checking a property on a design.

LTLValidAlg(Spec property)
A constructor for checking a property without a design.

Method Summary

AlgResultI	doAlgorithm() Check validity for a given LTL property.
AlgResultI	postAlgorithm() Does nothing.
AlgResultI	preAlgorithm() Preparing the LTL tester.

Methods inherited from class java.lang.Object

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

Constructor Detail

LTLValidAlg

public LTLValidAlg(Spec property)

A constructor for checking a property without a design.

Parameters:

property - The property to check.

LTLValidAlg

public LTLValidAlg(SMVModule design,
                   Spec property)

A constructor for checking a property on a design.

Parameters:

design - The design to check the property for.

property - The property to check.

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

Check validity for a given LTL property.

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()