core
Class FiniteStateMachine

java.lang.Object
  extended by core.FiniteStateMachine

public class FiniteStateMachine
extends java.lang.Object

This class represents a finite state machine (E,S,I,T,F) where

The class is very similar to the mathematical construct. The set of states S, I and F are represented Collections. The transitions are not globally defined in a transition relation, but locally in the transitioning states themselves. The alphabet is implicitely defined through the used transition symbols.

Author:
Leopold Haller

Field Summary
static int OUTPUT_NORMAL
           
static int OUTPUT_OFF
           
static int OUTPUT_VERBOSE
           
 
Constructor Summary
FiniteStateMachine()
          Creates an empty finite state machine
FiniteStateMachine(FiniteStateMachine fsm)
          Copy constructor.
 
Method Summary
 boolean accepts(java.lang.String... s)
          Checks whether the FSM accepts the given input.
 void addTransition(java.lang.String stateName, java.lang.String symbol, java.lang.String... successors)
           
 java.lang.Object clone()
          Makes a deep copy of the FSM
 FiniteStateMachine complementLanguage()
          Inverts all final states (all non-final states become final, all final states become non-final) If the given fsm is not deterministic or not complete, the complement of the power fsm will be returned.
 State createAnonymousState()
          Creates a normal state that is automatically named.
 State createState(java.lang.String name, StateType type)
          Creates a new state of the specified type in the fsm.
 java.util.Set<java.lang.String> determineAlphabet()
          Returns a set of all transition symbols of the FSM.
 java.util.Collection<State> getFinalStates()
           
 java.util.Collection<State> getInitialStates()
           
static int getOutputMode()
          Returns the output mode
 State getState(java.lang.String stateName)
           
 java.util.Collection<State> getStates()
           
 StateType getType(State s)
           
 boolean hasReachableFinalState()
           
 boolean isComplete()
           
 boolean isDeterministic()
           
 FiniteStateMachine link(java.lang.String... symbols)
          Creates an fsm where some symbols are replaced by other symbols.
 FiniteStateMachine makeAllStatesFinal()
          Returns a clone of the fsm whose states are all final.
 FiniteStateMachine makeComplete()
          Adds a non-final error state to the fsm.
 FiniteStateMachine makeInvariantTo(FiniteStateMachine... fsm)
          Tries to make the "checker"-FSM invariant to the alphabet of all other fsms given as arguments in the array "fsm".
 FiniteStateMachine minimize()
          Minimizes the FSM.
 FiniteStateMachine parallel(FiniteStateMachine fsm)
          Constructs a FiniteStateMachine that is the asynchronous composition of the two FSMs.
static FiniteStateMachine partialOrderReduction(FiniteStateMachine checker, FiniteStateMachine... fsm)
          The partial order reduction constructs a reduced state graph of the parallel composition of all FSMs given in the array "fsm".
 FiniteStateMachine power()
          Returns the power-fsm of the finite state machine.
 FiniteStateMachine product(FiniteStateMachine fsm)
          Creates a product machine which accepts as a language the intersection of the two languages of the given finite state machines.
 boolean removeState(State toRemove)
          Removes a state (also initial state and final state) from the FSM.
static void setOutputMode(int outputMode)
          Sets the output mode
 void setType(State s, StateType type)
          Sets the state to the specified type.
 java.lang.String toString()
           
 void visualize()
           
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

OUTPUT_NORMAL

public static final int OUTPUT_NORMAL
See Also:
Constant Field Values

OUTPUT_OFF

public static final int OUTPUT_OFF
See Also:
Constant Field Values

OUTPUT_VERBOSE

public static final int OUTPUT_VERBOSE
See Also:
Constant Field Values
Constructor Detail

FiniteStateMachine

public FiniteStateMachine()
Creates an empty finite state machine


FiniteStateMachine

public FiniteStateMachine(FiniteStateMachine fsm)
Copy constructor. Creates an fsm that is a deep copy of the supplied fsm.

Parameters:
fsm -
Method Detail

getOutputMode

public static int getOutputMode()
Returns the output mode

Returns:
OUTPUT_OFF, OUTPUT_NORMAL or OUTPUT_VERBOSE

partialOrderReduction

public static FiniteStateMachine partialOrderReduction(FiniteStateMachine checker,
                                                       FiniteStateMachine... fsm)
The partial order reduction constructs a reduced state graph of the parallel composition of all FSMs given in the array "fsm". This reduced state graph should behave equivalently to the full state graph when checking the conformity to a specification using a checker- If a "checker" != null is specified, the synchronous product (see product()) of the reduced state graph and the checker is constructed on the fly. Else ("checker" == null) an invariant checker is assumed, and only the reduced state graph is constructed. Note that if the checker is not invariant to the local symbols of the parallel components, the reduced state graph gets bigger. If the function is called with "checker"==null an invariant checker is assumed, therefore doing a synchronous product with the reduced state graph and a non-invariant checker afterwards can easily lead to wrong results. An explanation of the algorithm is given in the paper "FSMCalc" accompanying this program.

Parameters:
checker - The fsm that's acting as the checker. May be null if no checker is needed.
fsm - The parallel components
Returns:

setOutputMode

public static void setOutputMode(int outputMode)
Sets the output mode

Parameters:
outputMode - OUTPUT_OFF, OUTPUT_NORMAL or OUTPUT_VERBOSE

accepts

public boolean accepts(java.lang.String... s)
Checks whether the FSM accepts the given input.

Parameters:
s - the input in varargs or array form
Returns:
True if the given sequence of transformations ends at a final state, false otherwise

addTransition

public void addTransition(java.lang.String stateName,
                          java.lang.String symbol,
                          java.lang.String... successors)

clone

public java.lang.Object clone()
Makes a deep copy of the FSM

Overrides:
clone in class java.lang.Object

complementLanguage

public FiniteStateMachine complementLanguage()
Inverts all final states (all non-final states become final, all final states become non-final) If the given fsm is not deterministic or not complete, the complement of the power fsm will be returned.

Returns:
A clone of the FiniteStateMachine with inverted final states

createAnonymousState

public State createAnonymousState()
Creates a normal state that is automatically named. Created names are of the form AnX where X is an integer.

Returns:
A new anonymous state.

createState

public State createState(java.lang.String name,
                         StateType type)
Creates a new state of the specified type in the fsm. States are identified based on their name, no two states of the same name can be added.
If a state of that name already exists an exception is thrown.
State names may not start with a lower-case letter

Parameters:
name - The name of the state to add (may not start with lower-case letter
type - An enumeration giving the type of the State, either NORMAL_STATE,INITIAL_STATE,FINAL_STATE or INITIAL_FINAL_STATE
Returns:
The state that was created

determineAlphabet

public java.util.Set<java.lang.String> determineAlphabet()
Returns a set of all transition symbols of the FSM. Changes of the FSM are not reflected in the returned set. The FSM has to be traversed every time determineAlphabet() is called.

Returns:
The alphabet of the FSM

getFinalStates

public java.util.Collection<State> getFinalStates()

getInitialStates

public java.util.Collection<State> getInitialStates()

getState

public State getState(java.lang.String stateName)

getStates

public java.util.Collection<State> getStates()

getType

public StateType getType(State s)

isComplete

public boolean isComplete()

isDeterministic

public boolean isDeterministic()

hasReachableFinalState

public boolean hasReachableFinalState()
Returns:
true if a reachable final-state exists

link

public FiniteStateMachine link(java.lang.String... symbols)
Creates an fsm where some symbols are replaced by other symbols.

Parameters:
symbols - An array of symbols. Each even symbol symbols[i] (i=0,2,4,...) is replaced by its successor-symbol symbols[i+1]. The array must be even sized.
Returns:
A clone of the fsm where some symbols have been replaced by others.

makeAllStatesFinal

public FiniteStateMachine makeAllStatesFinal()
Returns a clone of the fsm whose states are all final. Such an fsm is in effect a labelled transition system.

Returns:
A clone of the fsm where all states are final

makeComplete

public FiniteStateMachine makeComplete()
Adds a non-final error state to the fsm. If one of the fsm's states does not transition with a symbol contained in the fsm's alphabet, a transition with the symbol to the error state is added.

Returns:
A clone of the FiniteStateMachine which has been made complete

makeInvariantTo

public FiniteStateMachine makeInvariantTo(FiniteStateMachine... fsm)
Tries to make the "checker"-FSM invariant to the alphabet of all other fsms given as arguments in the array "fsm". This means that in every state s of the "checker"-fsm a reflexive transition s --sym-->s with the symbol sym is added, if s previously had no transition with sym and sym is an element of one of the FSMs given in the array "fsm". This method can be used as preparation for the partial order reduction, as an invariant checker results in a better reduction of the state graph. Note that this operation changes the language of the finite state machine.

Parameters:
fsm - The fsms containing the alphabets, the resulting machine should be invariant to.
Returns:
A clone of the current fsm which is invariant to all transitions in the alphabets of the arguments, except for those non-invariant transitions which already existed.

minimize

public FiniteStateMachine minimize()
Minimizes the FSM. Non-deterministic FSMs are first made deterministic by constructing the Power-FSM.

Returns:
The minimized FSM

parallel

public FiniteStateMachine parallel(FiniteStateMachine fsm)
Constructs a FiniteStateMachine that is the asynchronous composition of the two FSMs.
If a transition has a symbol that exists in both FSM's alphabets it is treated as a synchronous transition, else it is treated as an asynchronous transition. Synchronous transitions can only "fire" if both original FSMs fire with it's symbol in the original states. If for example the letter 's' is a synchronous transition symbol, then the state A|B of the resulting FSM (A parallel to B) can only transition with 's' if both 'A' and 'B' have an equivalent transition with the same symbol. In this case A and B would both change into their successor states.
If on the other hand 's' was an asynchronous transition of the first FSM the state A|B could fire a transition with 's', if the original state 'A' had a corresponding transition. Only 'A' would change into it's successor state, while 'B' would remain unchanged.
If two states A (FSM1) and B (FSM2) are final in the original FSMs the resulting parallel state will be final.

Parameters:
fsm -
Returns:
A fsm that represents the asynchronous composition of the two FSMs

power

public FiniteStateMachine power()
Returns the power-fsm of the finite state machine.

Returns:
The deterministic and complete power-fsm of the finite state machine.

product

public FiniteStateMachine product(FiniteStateMachine fsm)
Creates a product machine which accepts as a language the intersection of the two languages of the given finite state machines.
The resulting product machine is not a complete product, it contains only reachable states.

Parameters:
fsm -
Returns:
A FSM representing the product between the two input FSMs.

removeState

public boolean removeState(State toRemove)
Removes a state (also initial state and final state) from the FSM. All connections to the state are also removed.

Parameters:
toRemove - The state to be removed. May not be null.
Returns:
True if s could be removed, false if no such state existed

setType

public void setType(State s,
                    StateType type)
Sets the state to the specified type. If no such state exists an exception is thrown.

Parameters:
s -
type -

toString

public java.lang.String toString()
Overrides:
toString in class java.lang.Object

visualize

public void visualize()