envgen.spec
Class LTLNode

java.lang.Object
  |
  +--envgen.spec.SpecNode
        |
        +--envgen.spec.LTLNode

public class LTLNode

extends SpecNode

Data structure to hold an LTL formula.

Field Summary

(package private) char	kind Kinds of node: 'P' atomic proposition, 'G' globally, 'E' eventually (finally), '!' negation, 'X' next, 'T' true, 'F' false, '&' and, '|' or, 'U' until, 'V' dual of until.
(package private) LTLNode	left Left operand, used for binary operators such as &, |, etc.
(package private) LTLNode	right Right operand, used for binary operators such as &, |, etc.

Fields inherited from class envgen.spec.SpecNode

proposition, val

Constructor Summary

LTLNode()
Default constructor.

LTLNode(char op, int v, LTLNode l, LTLNode r)

LTLNode(LTLNode f)
Copy constructor.

Method Summary

boolean	equals(java.lang.Object f)
char	getKind()
LTLNode	getLeft()
LTLNode	getRight()
static LTLNode	pushNot(LTLNode f, boolean b) Pushes negations inside the formula, until they appear only in front of atomic propositions.
void	setKind(char c)
void	setLeft(LTLNode f)
void	setRight(LTLNode f)
static LTLNode	singleEventCondition(java.util.List propositions) Builds an LTL formuls that corresponds to the single event condition, takes as an input a universe of propositions, and builds a formula that states that no two propositions from the universe can hold at the same time.
java.lang.String	toString()

Methods inherited from class envgen.spec.SpecNode

getProposition, getVal, setProposition

Methods inherited from class java.lang.Object

clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

kind

char kind

Kinds of node: 'P' atomic proposition, 'G' globally, 'E' eventually (finally), '!' negation, 'X' next, 'T' true, 'F' false, '&' and, '|' or, 'U' until, 'V' dual of until.

left

LTLNode left

Left operand, used for binary operators such as &, |, etc.

right

LTLNode right

Right operand, used for binary operators such as &, |, etc.

Constructor Detail

LTLNode

public LTLNode(char op,
               int v,
               LTLNode l,
               LTLNode r)

LTLNode

public LTLNode()

Default constructor.

LTLNode

public LTLNode(LTLNode f)

Copy constructor.

Method Detail

singleEventCondition

public static LTLNode singleEventCondition(java.util.List propositions)

Builds an LTL formuls that corresponds to the single event condition, takes as an input a universe of propositions, and builds a formula that states that no two propositions from the universe can hold at the same time.

equals

public boolean equals(java.lang.Object f)

Overrides:

equals in class java.lang.Object

pushNot

public static LTLNode pushNot(LTLNode f,
                              boolean b)

Pushes negations inside the formula, until they appear only in front of atomic propositions.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getRight

public LTLNode getRight()

setRight

public void setRight(LTLNode f)

getLeft

public LTLNode getLeft()

setLeft

public void setLeft(LTLNode f)

getKind

public char getKind()

setKind

public void setKind(char c)