My first FSM synthesizer using rosette

rosette-fsm-synthesis.rkt

#lang rosette

(require
  rosette/lib/lift
  (prefix-in racket/ (only-in racket assv))
  rosette/lib/angelic
  rosette/lib/synthax
  )

;; Define FSM

; lift assv functions
(define-lift assv
  [(symbol? list?) racket/assv])

; from Shriram Krishnamurthi, "Automata via Macros."
(define (automaton init-state machine stream)
  (define (walker state stream)
    (cond
      [(empty? stream)
        ; only accept the final state with no outgoing edges
        (eq? (length (assv state machine)) 1)]
      [else
        (let ([in (first stream)]
              [transitions (rest (assv state machine))])
          (let ([new-state (assv in transitions)])
            (if new-state
              (walker (first (rest new-state)) (rest stream))
              false)))]))
  (walker init-state stream))


;; FSM synthesis example

; spec
(define (m stream)
  (automaton
    'init
    '((init (c more))
      (more (a more)
            (d more)
            (r end))
      (end))
    stream))

; sketch
(define (??m stream)
  (automaton
    'init
    `((init (c ,(choose 'init 'more 'end)))
      (more (a ,(choose 'init 'more 'end))
            (d ,(choose 'init 'more 'end))
            (r end))
      (end))
    stream))

; create a symbolic input
(define (get-sym-input size [alphabet '(c a d r)])
  (for/list ([i size])
    (apply choose* alphabet)))
(define sin (get-sym-input 4))

; synthesize!
(define M (synthesize
  #:forall sin
  #:guarantee (assert (equal? (m sin) (??m sin)))))
(print-forms M)