% $Id$

FSM(T): trait
  includes
    List(String, Symbol)
    Set(Language, String)

  introduces
    __ [ __ ] : TransitionFunction, State -> State
    transitions: T, Symbol -> TransitionFunction

	% for:
	%   transition(fsm, sym)[s1] = s2
        % read:
	%   When presented with sym, fsm transitions from s1 to s2.

    start: T -> State

    consume: T, State, String -> State

    accept: T, State -> Bool
    accept: T, String -> Bool

    language: T -> Language

  asserts forall fsm: T, st: State, sym: Symbol, str: String
    accept(fsm, str) == accept(fsm, consume(fsm, start(fsm), str))

    consume(fsm, st, empty) == st
    consume(fsm, st, sym \precat str) == 
      consume(fsm, transition(fsm,sym)[st], str)

    str \in language(fsm) == accept(fsm, str)