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

java.lang.Object
  edu.wis.jtlv.lib.mc.tl.LTLTester

public class LTLTester
extends java.lang.Object

Construct a tester for a given LTL specification.

Author:

yaniv sa'ar

Constructor Summary

LTLTester(Spec root_spec, boolean isWeak)
Constructor for the tester.

Method Summary

BDD	getSpec2BDD(Spec root) Returns a BDD variable representing the given specification in this tester.
SMVModule	getTester() Getter for the tester which where constructed from this specification.

Methods inherited from class java.lang.Object

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

Constructor Detail

LTLTester

public LTLTester(Spec root_spec,
                 boolean isWeak)
          throws ModelCheckAlgException

Constructor for the tester.

Parameters:

root_spec - The specification to construct tester for.

isWeak - Whether to add initial or not.

Throws:

ModelCheckAlgException

Method Detail

getTester

public SMVModule getTester()

Getter for the tester which where constructed from this specification.

Returns:

The tester which where constructed from this specification.

getSpec2BDD

public BDD getSpec2BDD(Spec root)
                throws ModelCheckAlgException

Returns a BDD variable representing the given specification in this tester.

Parameters:

root - The specification.

Returns:

A BDD variable representing the given specification in this tester.

Throws:

ModelCheckAlgException - When failed to find the cooresponding BDD variable.