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

Author:

yaniv sa'ar.

Constructor Summary

SpecExp(Operator op, Spec e1)
Constructor for an unary specification.

SpecExp(Operator op, Spec[] el)
A general purpose constructor.

SpecExp(Operator op, Spec e1, Spec e2)
Constructor for a binary specification.

SpecExp(Operator op, Spec e1, Spec e2, Spec e3)
Constructor for a triplet specification.

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.
Spec[]	getChildren() Get the children specification of this node.
Operator	getOperator() The operator representing this node.
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

SpecExp

public SpecExp(Operator op,
               Spec[] el)
        throws SpecException

A general purpose constructor.

Parameters:

op - The operator.

el - An array of children specification

Throws:

SpecException

SpecExp

public SpecExp(Operator op,
               Spec e1)

Constructor for an unary specification.

Parameters:

op - The operator.

e1 - The sub specification.

SpecExp

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

Constructor for a binary specification.

Parameters:

op - The operator.

e1 - The first sub specification.

e2 - The second sub specification.

SpecExp

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

Constructor for a triplet specification.

Parameters:

op - The operator.

e1 - The first sub specification.

e2 - The second sub specification.

e3 - The third sub specification.

Method Detail

getOperator

public Operator getOperator()

The operator representing this node.

Returns:

An operator representing this node.

getChildren

public Spec[] getChildren()

Get the children specification of this node.

Returns:

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

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.

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.