Skip to content

Instantly share code, notes, and snippets.

@mjyc
Last active March 31, 2020 17:16
Show Gist options
  • Save mjyc/eefec664b346ec6b95301750e96489f6 to your computer and use it in GitHub Desktop.
Save mjyc/eefec664b346ec6b95301750e96489f6 to your computer and use it in GitHub Desktop.
My first FSM synthesizer using rosette
#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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment