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.3.2"

Author:

yaniv sa'ar.

Constructor Summary

SpecBDD(BDD v)
A constructor for a leaf BDD specification, without a string representation.

SpecBDD(java.lang.String identifying_expr, BDD v)
A constructor for a leaf BDD specification, with a string representation.

Method Summary

boolean	equals(java.lang.Object other) Implementors are required to provide the equals since two (syntactically) identical specifications, which are different object will return false to the usual equals.
BDD	getVal() Getter for the BDD value.
boolean	hasTemporalOperators() Does this specification has a temporal operator.
boolean	isCTLSpec() Is this a CTL specification.
boolean	isCTLStarSpec() Is this a CTL* specification.
boolean	isFutureLTLSpec() Is this a Future LTL specification.
boolean	isLTLSpec() Is this a LTL specification.
boolean	isPastLTLSpec() Is this a Past LTL specification.
boolean	isPropSpec() Is this a first order specification.
boolean	isRealTimeCTLSpec() Is this a Real Time CTL specification.
BDDVarSet	releventVars() Get the domain of this specification.
BDD	toBDD() Get the BDD representing this specification.
java.lang.String	toString() The usual 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,
               BDD v)

A constructor for a leaf BDD specification, with a string representation.

Parameters:

identifying_expr - The string from which this leaf was constructed.

v - The BDD value (if already evaluated).

SpecBDD

public SpecBDD(BDD v)

A constructor for a leaf BDD specification, without a string representation.

Parameters:

v - The evaluated BDD.

Method Detail

getVal

public BDD getVal()

Getter for the BDD value.

Returns:

The BDD value.

See Also:

toBDD()

isCTLSpec

public boolean isCTLSpec()

Description copied from interface: Spec

Is this a CTL specification.

Specified by:

isCTLSpec in interface Spec

Returns:

true, if this a CTL specification.

isRealTimeCTLSpec

public boolean isRealTimeCTLSpec()

Description copied from interface: Spec

Is this a Real Time CTL specification.

Specified by:

isRealTimeCTLSpec in interface Spec

Returns:

true, if this a Real Time CTL specification.

isCTLStarSpec

public boolean isCTLStarSpec()

Description copied from interface: Spec

Is this a CTL* specification.

Specified by:

isCTLStarSpec in interface Spec

Returns:

true, if this a CTL* specification.

isLTLSpec

public boolean isLTLSpec()

Description copied from interface: Spec

Is this a LTL specification.

Specified by:

isLTLSpec in interface Spec

Returns:

true, if this a LTL specification.

isFutureLTLSpec

public boolean isFutureLTLSpec()

Description copied from interface: Spec

Is this a Future LTL specification.

Specified by:

isFutureLTLSpec in interface Spec

Returns:

true, if this a Future LTL specification.

isPastLTLSpec

public boolean isPastLTLSpec()

Description copied from interface: Spec

Is this a Past LTL specification.

Specified by:

isPastLTLSpec in interface Spec

Returns:

true, if this a Past LTL specification.

isPropSpec

public boolean isPropSpec()

Description copied from interface: Spec

Is this a first order specification.

Specified by:

isPropSpec in interface Spec

Returns:

true, if this a first order specification.

hasTemporalOperators

public boolean hasTemporalOperators()

Description copied from interface: Spec

Does this specification has a temporal operator.

Specified by:

hasTemporalOperators in interface Spec

Returns:

true, if this specification has a temporal operator.

toString

public java.lang.String toString()

Description copied from interface: Spec

The usual toString.

Specified by:

toString in interface Spec

Overrides:

toString in class java.lang.Object

Returns:

A string representation of this object.

equals

public boolean equals(java.lang.Object other)

Description copied from interface: Spec

Implementors are required to provide the equals since two (syntactically) identical specifications, which are different object will return false to the usual equals.

Specified by:

equals in interface Spec

Overrides:

equals in class java.lang.Object

Parameters:

other - The other object to check equality with.

Returns:

true, if the given object is identical to the given.

releventVars

public BDDVarSet releventVars()

Description copied from interface: Spec

Get the domain of this specification.

Specified by:

releventVars in interface Spec

Returns:

The BDDVarSet with all the variable in this specification.

toBDD

public BDD toBDD()
          throws SpecException

Description copied from interface: Spec

Get the BDD representing this specification. Note that only first order specifications can get their toBDD, other kind of specification will throw an exception.

Specified by:

toBDD in interface Spec

Returns:

The BDD representing this specification.

Throws:

SpecException - When the specification is temporal.