edu.wis.jtlv.env.core.spec
Class InternalSpecCTLRange

java.lang.Object
  edu.wis.jtlv.env.core.spec.InternalSpec
      edu.wis.jtlv.env.core.spec.InternalSpecCTLRange

public class InternalSpecCTLRange
extends InternalSpec

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.

Field Summary

Fields inherited from class edu.wis.jtlv.env.core.spec.InternalSpec

evalBDDs, tend, tstart

Constructor Summary

InternalSpecCTLRange(int from, int to, org.antlr.runtime.Token start)

InternalSpecCTLRange(java.lang.String from, java.lang.String to, org.antlr.runtime.Token start)

Method Summary

void	evalBDDChildrenExp(org.antlr.runtime.TokenStream input)
int	getFrom()
int	getTo()
boolean	hasTemporalOperators()
boolean	isCTLSpec()
boolean	isCTLStarSpec()
boolean	isFutureLTLSpec()
boolean	isLTLSpec()
boolean	isPastLTLSpec()
boolean	isPropSpec()
boolean	isRealTimeCTLSpec()
java.lang.String	toString()

Methods inherited from class edu.wis.jtlv.env.core.spec.InternalSpec

setEndToken

Methods inherited from class java.lang.Object

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

Constructor Detail

InternalSpecCTLRange

public InternalSpecCTLRange(int from,
                            int to,
                            org.antlr.runtime.Token start)

InternalSpecCTLRange

public InternalSpecCTLRange(java.lang.String from,
                            java.lang.String to,
                            org.antlr.runtime.Token start)

Method Detail

getFrom

public int getFrom()

getTo

public int getTo()

evalBDDChildrenExp

public void evalBDDChildrenExp(org.antlr.runtime.TokenStream input)
                        throws SpecParseException

Specified by:

evalBDDChildrenExp in class InternalSpec

Throws:

SpecParseException

isPropSpec

public boolean isPropSpec()

Specified by:

isPropSpec in class InternalSpec

isCTLSpec

public boolean isCTLSpec()

Specified by:

isCTLSpec in class InternalSpec

isRealTimeCTLSpec

public boolean isRealTimeCTLSpec()

Specified by:

isRealTimeCTLSpec in class InternalSpec

isLTLSpec

public boolean isLTLSpec()

Specified by:

isLTLSpec in class InternalSpec

isFutureLTLSpec

public boolean isFutureLTLSpec()

Specified by:

isFutureLTLSpec in class InternalSpec

isPastLTLSpec

public boolean isPastLTLSpec()

Specified by:

isPastLTLSpec in class InternalSpec

isCTLStarSpec

public boolean isCTLStarSpec()

Specified by:

isCTLStarSpec in class InternalSpec

hasTemporalOperators

public boolean hasTemporalOperators()

Specified by:

hasTemporalOperators in class InternalSpec

toString

public java.lang.String toString()

Specified by:

toString in class InternalSpec