edu.wis.jtlv.env.spec
Class SpecExp

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

All Implemented Interfaces:

Spec

public class SpecExp
extends java.lang.Object
implements Spec

Specification expression.

Version:

"1.2.0"

Author:

yaniv sa'ar.

Constructor Summary

SpecExp(Operator op, Spec e1)

SpecExp(Operator op, Spec[] el)

SpecExp(Operator op, Spec e1, Spec e2)

SpecExp(Operator op, Spec e1, Spec e2, Spec e3)

Method Summary

boolean	equals(java.lang.Object other)
Spec[]	getChildren()
Operator	getOperator()
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

SpecExp

public SpecExp(Operator op,
               Spec[] el)

SpecExp

public SpecExp(Operator op,
               Spec e1)

SpecExp

public SpecExp(Operator op,
               Spec e1,
               Spec e2)

SpecExp

public SpecExp(Operator op,
               Spec e1,
               Spec e2,
               Spec e3)

Method Detail

getOperator

public Operator getOperator()

getChildren

public Spec[] getChildren()

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

isPropSpec

public boolean isPropSpec()

Specified by:

isPropSpec 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