edu.wis.jtlv.env.spec
Interface Spec

All Known Implementing Classes:

SpecBDD, SpecCTLRange, SpecExp

public interface Spec

A general interface for all kinds of specifications.

Version:

"1.3.2"

Author:

yaniv sa'ar.

See Also:

Env.loadSpecFile(String), Env.loadSpecString(String), Env.loadSpecInputStream(java.io.InputStream)

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

Method Detail

isPropSpec

boolean isPropSpec()

Is this a first order specification.

Returns:

true, if this a first order specification.

isCTLSpec

boolean isCTLSpec()

Is this a CTL specification.

Returns:

true, if this a CTL specification.

isRealTimeCTLSpec

boolean isRealTimeCTLSpec()

Is this a Real Time CTL specification.

Returns:

true, if this a Real Time CTL specification.

isLTLSpec

boolean isLTLSpec()

Is this a LTL specification.

Returns:

true, if this a LTL specification.

isFutureLTLSpec

boolean isFutureLTLSpec()

Is this a Future LTL specification.

Returns:

true, if this a Future LTL specification.

isPastLTLSpec

boolean isPastLTLSpec()

Is this a Past LTL specification.

Returns:

true, if this a Past LTL specification.

isCTLStarSpec

boolean isCTLStarSpec()

Is this a CTL* specification.

Returns:

true, if this a CTL* specification.

hasTemporalOperators

boolean hasTemporalOperators()

Does this specification has a temporal operator.

Returns:

true, if this specification has a temporal operator.

releventVars

BDDVarSet releventVars()

Get the domain of this specification.

Returns:

The BDDVarSet with all the variable in this specification.

toString

java.lang.String toString()

The usual toString.

Overrides:

toString in class java.lang.Object

Returns:

A string representation of this object.

equals

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.

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.

toBDD

BDD toBDD()
          throws SpecException

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

Returns:

The BDD representing this specification.

Throws:

SpecException - When the specification is temporal.