A buggy demonstration for automaton example.

automaton-demo.rkt

#lang rosette

(require rosette/query/debug rosette/lib/render rosette/lib/synthax)

; A macro to create an automaton.
(define-syntax automaton
  (syntax-rules (: →)  
    [(_ init-state
        (state : (label → target) ...) ...)
     (letrec ([state
               (lambda (stream)
                 (cond
                   [(empty? stream) (empty? '(label ...))]  
                   [else
                    (case (first stream)
                      [(label) (target (rest stream))] ...
                      [else false])]))]
              ...) 
       init-state)]))

; A special state that rejects all labels.
(define reject (lambda (stream) false))

; An automaton for the language a(b|c)*d.
(define/debug m
  (automaton init
             [init : (a → more)]
             [more : (b → more)
                     (c → more)
                     (d → end)]
             [end : ]))

(m '(a d))
(m '(a b d))
(m '(a c d))
(m '(a c b c d))
(m '(a c b c d d))

; symbolic variables
(define-symbolic bool-var boolean?)

; Static v.s. dynamic
(define (sbool)
  (define-symbolic b boolean?)
  b)

(define (dbool)
  (define-symbolic* b boolean?)
  b)

(eq? (sbool) (sbool))
(eq? (dbool) (dbool))

; Let's create symbolic words that can be used as inputs to
; our automaton.
; First, a word with exactly `k` letters chosen from `alphabet`.
(define (word k alphabet)
  (for/list ([i k])
    (define-symbolic* idx integer?)
    (list-ref alphabet idx)))

; Then, a word with at most `k` letters chosen from `alphabet`.
(define (word<= k alphabet)
  (define-symbolic* n integer?)
  (take (word k alphabet) n))

; 1. Angelic Execution
; We can now run `m` “in reverse”, e.g.
; searching for a word of length up to 4 that is accepted by `m`:
(define alp '(a b c d))
(define word1 (word<= 4 alp))
(define model1 (solve (assert (m word1))))
; (evaluate word1 model1)

; 2. Debugging
; We have just found a bug!
; We can ask the solver for a minimal set of expressions that are
; responsible for its failure to reject `'(a b)`,
; which should not be accepted by `m`, say the _unsat core_.
; (define ucore (debug [boolean?] (assert (not (m '(a b))))))
; (render ucore)

; Let's fix the bug and test again.

; 3. Verification
; Testing cannot guarantee the correctness of our implementation,
; thus let's now verify it! We'll check any word of a bounded length
; is accepted by `m` iff it matches against the corresponding
; regular expression `a(b+c)*d`, as defined by Racket.
(define (word->string w)
  (apply string-append (map symbol->string w)))
(define (spec regex w)
  (regexp-match-exact? regex (word->string w)))

; We simply just try the bound 4.
(define w (word<= 4 alp))
(define verify-model (verify (assert (eq? (m w) (spec #rx"a(b|c)*d" w)))))
; (evaluate w verify-model)
; (eq? (m '(a)) (spec #rx"a(b|c)*d" '(a)))

; 4. Synthesis
; The automaton macro provides a high level interface for specifying
; automata programs, but it still requires the details of transitions
; to be filled in manually. To ease the process, the user may specify
; a sketch and asks the solver to synthesize an actual implementation.

; Let's consider another alphabet:
(define alp2 '(c a d r))

; Sketch:
(define M 
  (automaton init
   [init : (c → (choose s1 s2))]
   [s1   : (a → (choose s1 s2 end reject)) 
           (d → (choose s1 s2 end reject))
           (r → (choose s1 s2 end reject))]
   [s2   : (a → (choose s1 s2 end reject)) 
           (d → (choose s1 s2 end reject))
           (r → (choose s1 s2 end reject))]
   [end  : ]))

; Let's synthesize an automaton which accepts `c(a|d)+r`.
(define word2 (word<= 4 alp2))
(define model2
  (synthesize #:forall word2
              #:guarantee (assert (eq? (spec #rx"c(a|d)+r" word2) (M word2)))))
; (generate-forms model2)

I am surprised that the verification invoked at line 97 fails and the solver returns a "counter-example" '(a) which in fact doesn't
violate the property. Could anyone tell me which part of code goes wrong, or this code reveals a bug in Rosette?