add more fsm tests

turnstile/examples/rosette/fsm.rkt

@@ -56,7 +56,7 @@
    --------
   ;; the #'choose identifier itself must have the location of its use
   ;; see define-synthax implementation, specifically syntax/source in utils
-  [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose) e ...) ⇒ : (⊔ ty ...)]]])
+  [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose) e- ...) ⇒ : (⊔ ty ...)]]])
 
 ;; (define (apply-FSM f v) (f v))
 ;; (define-primop apply-FSM : (→ FSM (List Symbol) Bool))

turnstile/examples/tests/rosette/fsm-test.rkt

@@ -11,6 +11,13 @@
 
 (define rx #px"^c[ad]+r$")
 
+(typecheck-fail (automaton init)
+ #:with-msg "initial state init is not declared state")
+(typecheck-fail (automaton init [init : (c → more)])
+ #:with-msg "unbound identifier")
+(typecheck-fail (automaton init [init : (c → "more")])
+ #:with-msg "expected State, given String")
+
 (define M 
   (automaton init
    [init : (c → (? s1 s2))]
@@ -22,7 +29,9 @@
            (r → (? s1 s2 end reject))]
    [end  : ]))
 
+
 (check-type (M '(c a r)) : Bool) ; symbolic result
+(check-type (if (M '(c a r)) 1 2) : Int)
 
 ;; example commands 
 (check-type (m '(c a r)) : Bool -> #t)