typed: start a SPIN test suite

racket/typed/syndicate/roles.rkt

@@ -66,7 +66,7 @@
          print-type print-role role-strings
          ;; Behavioral Roles
          export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
-         verify-actors
+         verify-actors verify-actors/fail
          ;; LTL Syntax
          True False Always Eventually Until WeakUntil Release Implies And Or Not A M
          ;; Extensions
@@ -961,6 +961,12 @@
    (syntax/loc this-syntax
      (check-true (#%app- proto:compile+verify spec- (#%app- list- actor-ty.role ...))))])
 
+(define-syntax-parser verify-actors/fail
+  [(_ spec actor-ty:type-or-proto ...)
+   #:with spec- #`(quote- #,(synd->proto (type-eval #'spec)))
+   (syntax/loc this-syntax
+     (check-false (#%app- proto:compile+verify spec- (#%app- list- actor-ty.role ...))))])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Tests
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

racket/typed/tests/spin/basic-assertion-communication.rkt

@@ -0,0 +1,26 @@
+#lang typed/syndicate
+
+(define-constructor* (ping [v : Int]))
+(define-constructor* (pong))
+
+(define (spawn-asserter)
+  (spawn
+   (lift+define-role ar
+   (start-facet a
+     (assert (ping 0))))))
+
+(define (spawn-responder)
+  (spawn
+   (lift+define-role rr
+   (start-facet r
+     (on (asserted (ping $x))
+         (start-facet go
+           (assert (pong))))))))
+
+(module+ test
+  (verify-actors (Eventually (A Pong))
+                 ar
+                 rr)
+
+  (verify-actors/fail (Eventually (A Pong))
+                      rr))

racket/typed/tests/spin/basic-assertion.rkt

@@ -0,0 +1,20 @@
+#lang typed/syndicate
+
+(define (spawn-asserter)
+  (spawn
+   (lift+define-role ar
+   (start-facet a
+     (assert (tuple 0))))))
+
+(module+ test
+  (verify-actors (Eventually (A (Tuple Int)))
+                 ar)
+
+  (verify-actors/fail (Not (Eventually (A (Tuple Int))))
+                      ar)
+
+  (verify-actors/fail (Always (A (Tuple Int)))
+                      ar)
+
+  (verify-actors (Eventually (Always (A (Tuple Int))))
+                 ar))