edu.wis.jtlv.env.spec
Class SpecBDD

java.lang.Object
  edu.wis.jtlv.env.spec.SpecBDD

All Implemented Interfaces:

Spec

public class SpecBDD
extends java.lang.Object
implements Spec

First order specification which is parsed as an SMV expression.

Version:

"1.2.0"

Author:

yaniv sa'ar.

Constructor Summary

SpecBDD(net.sf.javabdd.BDD v)

SpecBDD(java.lang.String identifying_expr, net.sf.javabdd.BDD v)

Method Summary

boolean	equals(java.lang.Object other)
net.sf.javabdd.BDD	getVal()
boolean	hasTemporalOperators()
boolean	isCTLSpec()
boolean	isCTLStarSpec()
boolean	isFutureLTLSpec()
boolean	isLTLSpec()
boolean	isPastLTLSpec()
boolean	isPropSpec()
boolean	isRealTimeCTLSpec()
net.sf.javabdd.BDDVarSet	releventVars()
net.sf.javabdd.BDD	toBDD()
java.lang.String	toString()

Methods inherited from class java.lang.Object

getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

SpecBDD

public SpecBDD(java.lang.String identifying_expr,
               net.sf.javabdd.BDD v)

SpecBDD

public SpecBDD(net.sf.javabdd.BDD v)

Method Detail

getVal

public net.sf.javabdd.BDD getVal()

isCTLSpec

public boolean isCTLSpec()

Specified by:

isCTLSpec in interface Spec

isRealTimeCTLSpec

public boolean isRealTimeCTLSpec()

Specified by:

isRealTimeCTLSpec in interface Spec

isCTLStarSpec

public boolean isCTLStarSpec()

Specified by:

isCTLStarSpec in interface Spec

isLTLSpec

public boolean isLTLSpec()

Specified by:

isLTLSpec in interface Spec

isFutureLTLSpec

public boolean isFutureLTLSpec()

Specified by:

isFutureLTLSpec in interface Spec

isPastLTLSpec

public boolean isPastLTLSpec()

Specified by:

isPastLTLSpec in interface Spec

isPropSpec

public boolean isPropSpec()

Specified by:

isPropSpec in interface Spec

hasTemporalOperators

public boolean hasTemporalOperators()

Specified by:

hasTemporalOperators in interface Spec

toString

public java.lang.String toString()

Specified by:

toString in interface Spec

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object other)

Specified by:

equals in interface Spec

Overrides:

equals in class java.lang.Object

releventVars

public net.sf.javabdd.BDDVarSet releventVars()

Specified by:

releventVars in interface Spec

toBDD

public net.sf.javabdd.BDD toBDD()
                         throws SpecException

Specified by:

toBDD in interface Spec

Throws:

SpecException