envgen.spec.ltl2buchi
Class Graph

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

public class Graph

extends java.lang.Object

This class implements costruction of a buchi automaton from an LTL formula.

Field Summary

(package private) MultiSet	buchi Set of nodes that represent a buchi automaton.
(package private) int	nodeID Unique node identification.
(package private) int	numActions Number of operations in the system.

Constructor Summary

Graph(int num)

Method Summary

MultiSet	createGraph(LTLNode f) Creates the first node of the buchi automaton that has node 0 in incoming set and f in a set of new (not yet processed) formulas; expands the first node.
MultiSet	expand(Node cnd, MultiSet set) Expands node cnd and adds processed nodes into the buchi automaton set.
Node	find(Node nd, MultiSet set)
MultiSet	getFSA(MultiSet buchi)
MultiSet	getInitial(MultiSet buchi)
boolean	searchNeg(LTLNode f, MultiSet set)
void	setAccepting(MultiSet buchi)
void	setNodeID(int n)
void	setOutgoing(MultiSet buchi)

Methods inherited from class java.lang.Object

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

Field Detail

nodeID

int nodeID

Unique node identification.

buchi

MultiSet buchi

Set of nodes that represent a buchi automaton.

numActions

int numActions

Number of operations in the system.

Constructor Detail

Graph

public Graph(int num)

Method Detail

createGraph

public MultiSet createGraph(LTLNode f)

Creates the first node of the buchi automaton that has node 0 in incoming set and f in a set of new (not yet processed) formulas; expands the first node.

expand

public MultiSet expand(Node cnd,
                       MultiSet set)

Expands node cnd and adds processed nodes into the buchi automaton set.

find

public Node find(Node nd,
                 MultiSet set)

searchNeg

public boolean searchNeg(LTLNode f,
                         MultiSet set)

getInitial

public MultiSet getInitial(MultiSet buchi)

setOutgoing

public void setOutgoing(MultiSet buchi)

setAccepting

public void setAccepting(MultiSet buchi)

getFSA

public MultiSet getFSA(MultiSet buchi)

setNodeID

public void setNodeID(int n)