3.12 Solution: Finite State Machines

  #lang racket
   
  ;; modeling the transitions in non-deterministic finite-state machines 
   
  (require redex)
   
  ;; -----------------------------------------------------------------------------
  ;; syntax 
   
  (define-language L
    [FSM (rule ...)]
    [rule [state -> input -> state]]
    [state variable-not-otherwise-mentioned]
    [input variable-not-otherwise-mentioned])
   
  ;; -----------------------------------------------------------------------------
  ;; the reduction system
   
  (module+ test
    (define fsm1 (term ([a -> x -> b]
                        [a -> y -> c]
                        [b -> x -> a])))
    
    (test-->> -->fsm
              (term [,fsm1
                     a
                     (x x y)])
              (term [,fsm1
                     c
                     ()]))
    (test-->> -->fsm
              (term [,fsm1
                     a
                     (x x y x)])
              (term [,fsm1
                     c
                     (x)]))
    
    (define fsm2 (term ([a -> x -> b]
                        [a -> y -> c]
                        [a -> y -> d]
                        [b -> x -> a]
                        [d -> x -> b])))
    (test-->>∃ -->fsm
               (term [,fsm2
                      a
                      (x x y x)])
               (term [,fsm2
                      b
                      ()])))
   
  (define -->fsm
    (reduction-relation
     L
     #:domain [FSM state (input ...)]
     (--> [FSM state_1 (input_0 input_1 ...)]
          [FSM state_2 (input_1 ...)]
          (where (_ ... [state_1 -> input_0 -> state_2] _ ...)
                 FSM))))
   
  (module+ test
    (test-results))