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

Author:

yaniv sa'ar.

Constructor Summary

SpecCTLRange(int from, int to)

Method Summary

boolean	equals(java.lang.Object other)
int	getFrom()
int	getTo()
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

SpecCTLRange

public SpecCTLRange(int from,
                    int to)

Method Detail

getFrom

public int getFrom()

getTo

public int getTo()

isPropSpec

public boolean isPropSpec()

Specified by:

isPropSpec in interface Spec

isCTLSpec

public boolean isCTLSpec()

Specified by:

isCTLSpec in interface Spec

isRealTimeCTLSpec

public boolean isRealTimeCTLSpec()

Specified by:

isRealTimeCTLSpec 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

isCTLStarSpec

public boolean isCTLStarSpec()

Specified by:

isCTLStarSpec 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