envgen.spec.ltl2buchi
Class Node

java.lang.Object
  |
  +--envgen.spec.ltl2buchi.Node

public class Node

extends java.lang.Object

Implementation of a buchi automaton node. A buchi automaton is a set of nodes.

Field Summary

(package private) int	id Unique node id.
(package private) MultiSet	incoming The incoming edges represented by ids of nodes with outgoing edges leading to this node.
(package private) MultiSet	newF A set of formulas that must be true in this state and have not yet been processed.
(package private) MultiSet	nextF Formulas that must be true in all states that are immediate successors of states satisfying formulas in oldF.
(package private) MultiSet	oldF Formulas that must be true in this state and have been processed.
(package private) MultiSet	outgoing Outgoing edges represented by ids of successor nodes.
(package private) MultiSet	propositions Set of atomic propositions that must be true in this state.

Constructor Summary

Node(int pid, MultiSet pincoming, MultiSet pnewF, MultiSet poldF, MultiSet pnextF, MultiSet ppropositions)
Creates a node.

Method Summary

int	getID() True if this is an accepting state.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

id

int id

Unique node id.

incoming

MultiSet incoming

The incoming edges represented by ids of nodes with outgoing edges leading to this node.

newF

MultiSet newF

A set of formulas that must be true in this state and have not yet been processed.

oldF

MultiSet oldF

Formulas that must be true in this state and have been processed.

nextF

MultiSet nextF

Formulas that must be true in all states that are immediate successors of states satisfying formulas in oldF.

outgoing

MultiSet outgoing

Outgoing edges represented by ids of successor nodes.

propositions

MultiSet propositions

Set of atomic propositions that must be true in this state.

Constructor Detail

Node

public Node(int pid,
            MultiSet pincoming,
            MultiSet pnewF,
            MultiSet poldF,
            MultiSet pnextF,
            MultiSet ppropositions)

Creates a node.

Method Detail

getID

public int getID()

True if this is an accepting state.

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object