edu.wis.jtlv.old_lib.mc
Class LTLModelChecker.LTLTesterBuilder

java.lang.Object
  edu.wis.jtlv.old_lib.mc.LTLModelChecker.LTLTesterBuilder

Enclosing class:

LTLModelChecker

public static class LTLModelChecker.LTLTesterBuilder
extends java.lang.Object

Constructor Summary

LTLModelChecker.LTLTesterBuilder(Spec root_spec, boolean isWeak)

Method Summary

BDD	getSpec2BDD(Spec root)
SMVModule	getTester()

Methods inherited from class java.lang.Object

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

Constructor Detail

LTLModelChecker.LTLTesterBuilder

public LTLModelChecker.LTLTesterBuilder(Spec root_spec,
                                        boolean isWeak)
                                 throws ModelCheckException

Throws:

ModelCheckException

Method Detail

getTester

public SMVModule getTester()

getSpec2BDD

public BDD getSpec2BDD(Spec root)
                throws ModelCheckException

Throws:

ModelCheckException