edu.wis.jtlv.env.spec
Class SpecCTLRange

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

All Implemented Interfaces:

Spec

public class SpecCTLRange
extends java.lang.Object
implements Spec

This node is a range node for the Real Time CTL operators.
Simple ranges are not assigned with such a node, and are evaluated as a smv expressions.
For consistency, this is not regarded as a temporal operator in the queries. Its holder should mark it as a temporal operator.

Version:

"1.3.2"

Author:

yaniv sa'ar.

Constructor Summary

SpecCTLRange(int from, int to)
A constructor for (Real Time) CTL range.

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.
int	getFrom() Get the range start.
int	getTo() Get the range end.
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

SpecCTLRange

public SpecCTLRange(int from,
                    int to)

A constructor for (Real Time) CTL range.

Parameters:

from - range start.

to - range end

Method Detail

getFrom

public int getFrom()

Get the range start.

Returns:

The range start.

getTo

public int getTo()

Get the range end.

Returns:

The range end.

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.

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.

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.

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.

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.