From 4e48285d7fe5e85fe6e9866ac07be374d1a780ab Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 22 Jul 2016 15:33:46 -0400 Subject: [PATCH] add more fsm tests --- turnstile/examples/rosette/fsm.rkt | 2 +- turnstile/examples/tests/rosette/fsm-test.rkt | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/turnstile/examples/rosette/fsm.rkt b/turnstile/examples/rosette/fsm.rkt index 5567280..52af182 100644 --- a/turnstile/examples/rosette/fsm.rkt +++ b/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)) diff --git a/turnstile/examples/tests/rosette/fsm-test.rkt b/turnstile/examples/tests/rosette/fsm-test.rkt index 9289d02..e7dd395 100644 --- a/turnstile/examples/tests/rosette/fsm-test.rkt +++ b/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)