fsm-test.rkt (1324B)
1 #lang s-exp "../../rosette/fsm.rkt" 2 (require "../rackunit-typechecking.rkt") 3 4 (define m 5 (automaton init 6 [init : (c → more)] 7 [more : (a → more) 8 (d → more) 9 (r → end)] 10 [end : ])) 11 12 (define rx #px"^c[ad]+r$") 13 14 (typecheck-fail (automaton init) 15 #:with-msg "initial state init is not declared state") 16 (typecheck-fail (automaton init [init : (c → more)]) 17 #:with-msg "unbound identifier") 18 (typecheck-fail (automaton init [init : (c → "more")]) 19 #:with-msg "expected State, given String") 20 21 (define M 22 (automaton init 23 [init : (c → (? s1 s2))] 24 [s1 : (a → (? s1 s2 end reject)) 25 (d → (? s1 s2 end reject)) 26 (r → (? s1 s2 end reject))] 27 [s2 : (a → (? s1 s2 end reject)) 28 (d → (? s1 s2 end reject)) 29 (r → (? s1 s2 end reject))] 30 [end : ])) 31 32 33 (check-type (M '(c a r)) : Bool) ; symbolic result 34 (check-type (if (M '(c a r)) 1 2) : Int) 35 36 ;; example commands 37 (check-type (m '(c a r)) : Bool -> #t) 38 (check-type (m '(c d r)) : Bool -> #t) 39 (check-type (m '(c a d a r)) : Bool -> #t) 40 (check-type (m '(c a d a)) : Bool -> #f) 41 (check-type (verify-automaton m #px"^c[ad]+r$") : (List Symbol) -> '(c r)) 42 (check-type (debug-automaton m #px"^c[ad]+r$" '(c r)) : Pict) 43 (check-type (synthesize-automaton M #px"^c[ad]+r$") : Unit)