envgen.spec.ltl2buchi
Class FSA

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

public class FSA

extends java.lang.Object

Implementation of a finite state automaton used for code generation of drivers.

Field Summary

(package private) int	actualSize
(package private) FSAState[]	fsaStates Automaton states that keep track of transitions and what states they lead to.
(package private) int	initialState
(package private) int	maxSize

Constructor Summary

FSA(MultiSet buchi, int numActions)
Takes a buchi automaton, throws away states that do not confrom to a single event condition, performs simple optimizations.

Method Summary

MultiSet	filter(MultiSet propositions, int numActions) Check whether propositions set conforms to single event condition and rewrites a set in terms of || (vs &&).
int	getInitialState()
int	getMaxSize()
FSAState[]	getStates()
void	makeInitial() Takes one of the initial states, marks it as a new initial state, removes the rest of the initial states, adding their transitions and propositions to the new initial state.
boolean	optimize(MultiSet[] propositions) Collapses states with similar incoming and similar outgoing transitions.
void	rearrange(MultiSet[] propositions) Makes numbering of states continuous, not implemented yet.
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

maxSize

int maxSize

fsaStates

FSAState[] fsaStates

Automaton states that keep track of transitions and what states they lead to.

actualSize

int actualSize

initialState

int initialState

Constructor Detail

FSA

public FSA(MultiSet buchi,
           int numActions)

Takes a buchi automaton, throws away states that do not confrom to a single event condition, performs simple optimizations.

Method Detail

filter

public MultiSet filter(MultiSet propositions,
                       int numActions)

Check whether propositions set conforms to single event condition and rewrites a set in terms of || (vs &&).

optimize

public boolean optimize(MultiSet[] propositions)

Collapses states with similar incoming and similar outgoing transitions.

rearrange

public void rearrange(MultiSet[] propositions)

Makes numbering of states continuous, not implemented yet.

makeInitial

public void makeInitial()

Takes one of the initial states, marks it as a new initial state, removes the rest of the initial states, adding their transitions and propositions to the new initial state.

getInitialState

public int getInitialState()

getStates

public FSAState[] getStates()

getMaxSize

public int getMaxSize()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object