fix tests

Wasn't checking redundancy in adding states to the worklist, so could
end up analyzing the same state many, many times. RoleNTimes exposed
this behavior: going from 3 to 5 repetitions caused compilation to hang

racket/info.rkt

@@ -36,3 +36,8 @@
                      "scribble-lib"
                      "sha"
                      ))
+
+(define test-omit-paths
+  ;; There's some shared library related build issue with the syndicate-gl things
+  '("syndicate-gl/"
+    "syndicate-ide/"))

racket/syndicate/actor.rkt

@@ -803,7 +803,7 @@
   #:macro-definer-name define-event-expander
   #:introducer-parameter-name current-event-expander-introducer
   #:local-introduce-name syntax-local-event-expander-introduce
-  #:expander-id-predicate-name event-expander-id?
+  #:expander-form-predicate-name event-expander-form?
   #:expander-transform-name event-expander-transform)
 
 (provide (for-syntax
@@ -811,7 +811,7 @@
           event-expander?
           event-expander-proc
           syntax-local-event-expander-introduce
-          event-expander-id?
+          event-expander-form?
           event-expander-transform)
          define-event-expander)
 
@@ -949,8 +949,8 @@
   (define event-stx (syntax-disarm armed-event-stx orig-insp))
   (syntax-parse event-stx
     #:literals [core:message asserted retracted rising-edge know forget realize]
-    [(expander args ...)
-     #:when (event-expander-id? #'expander)
+    [expander
+     #:when (event-expander-form? #'expander)
      (event-expander-transform
       event-stx
       (lambda (result)

racket/syndicate/info.rkt

@@ -7,4 +7,7 @@
   '(;; Sam: example-plain is interactive, I think
     "examples/example-plain.rkt"
     ;; Sam: for whatever reason I get a failure to load libcrypto for f-to-c
-    "examples/actor/f-to-c.rkt"))
+    "examples/actor/f-to-c.rkt"
+    ;; Sam: this test displays to stderr which the package server does not like
+    "tests/nested-spawn-exceptions.rkt"
+    ))

racket/syndicate/pattern.rkt

@@ -28,7 +28,7 @@
   #:macro-definer-name define-assertion-expander
   #:introducer-parameter-name current-assertion-expander-introducer
   #:local-introduce-name syntax-local-assertion-expander-introduce
-  #:expander-id-predicate-name assertion-expander-id?
+  #:expander-form-predicate-name assertion-expander-form?
   #:expander-transform-name assertion-expander-transform)
 
 (provide (for-syntax
@@ -36,7 +36,7 @@
           assertion-expander?
           assertion-expander-proc
           syntax-local-assertion-expander-introduce
-          assertion-expander-id?
+          assertion-expander-form?
           assertion-expander-transform)
          define-assertion-expander)
 
@@ -153,8 +153,8 @@
                    bs
                    ins))]
 
-        [(expander args ...)
-         (assertion-expander-id? #'expander)
+        [expander
+         (assertion-expander-form? #'expander)
          (assertion-expander-transform pat-stx (lambda (r) (walk (syntax-rearm r pat-stx))))]
 
         [(ctor p ...)

racket/typed/.gitignore

@@ -0,0 +1,4 @@
+*.pml
+*.trail
+*.rktd
+*.tmp

racket/typed/examples/book-club.rkt

@@ -34,14 +34,14 @@
 (define-type-alias τc
   (U BookQuote
      (Observe (BookQuoteT String ★/t))
-     (Observe (Observe (BookQuoteT ★/t ★/t)))
+     (Observe (Observe★ BookQuoteT))
      ClubMember
-     (Observe (ClubMemberT ★/t))
+     (Observe★ ClubMemberT)
      BookInterest
      (Observe (BookInterestT String ★/t ★/t))
-     (Observe (Observe (BookInterestT ★/t ★/t ★/t)))
+     (Observe (Observe★ BookInterestT))
      BookOfTheMonth
-     (Observe (BookOfTheMonthT ★/t))))
+     (Observe★ BookOfTheMonthT)))
 
 (define-type-alias Inventory (List (Tuple String Int)))
 
@@ -71,7 +71,7 @@
       ;; Give quotes to interested parties.
       (during (observe (book-quote $title _))
         ;; TODO - lookup
-        (assert (book-quote title (lookup title (ref books))))))))))
+        (assert (book-quote title (lookup title (! books))))))))))
 
 (define-type-alias leader-role
   (Role (leader)
@@ -111,52 +111,52 @@
             [title String (first titles)])
      (define (next-book)
        (cond
-         [(empty? (ref book-list))
+         [(empty? (! book-list))
           (printf "leader fails to find a suitable book\n")
           (stop get-quotes)]
          [#t
-          (set! title (first (ref book-list)))
-          (set! book-list (rest (ref book-list)))]))
+          (:= title (first (! book-list)))
+          (:= book-list (rest (! book-list)))]))
 
      ;; keep track of book club members
      (define/query-set members (club-member $name) name
          #;#:on-add #;(printf "leader acknowledges member ~a\n" name))
 
-     (on (asserted (book-quote (ref title) $quantity))
-         (printf "leader learns that there are ~a copies of ~a\n" quantity (ref title))
+     (on (asserted (book-quote (! title) $quantity))
+         (printf "leader learns that there are ~a copies of ~a\n" quantity (! title))
          (cond
-           [(< quantity (+ 1 (set-count (ref members))))
+           [(< quantity (+ 1 (set-count (! members))))
             ;; not enough in stock for each member
             (next-book)]
            [#t
             ;; find out if at least half of the members want to read the book
             (start-facet poll-members
-             (define/query-set yays (book-interest (ref title) $name #t) name)
-             (define/query-set nays (book-interest (ref title) $name #f) name)
-             (on (asserted (book-interest (ref title) $name _))
+             (define/query-set yays (book-interest (! title) $name #t) name)
+             (define/query-set nays (book-interest (! title) $name #f) name)
+             (on (asserted (book-interest (! title) $name _))
                  ;; count the leader as a 'yay'
-                 (when (>= (set-count (ref yays))
-                           (/ (set-count (ref members)) 2))
-                   (printf "leader finds enough affirmation for ~a\n" (ref title))
+                 (when (>= (set-count (! yays))
+                           (/ (set-count (! members)) 2))
+                   (printf "leader finds enough affirmation for ~a\n" (! title))
                    (stop get-quotes
                          (start-facet announce
-                                      (assert (book-of-the-month (ref title))))))
-                 (when (> (set-count (ref nays))
-                          (/ (set-count (ref members)) 2))
-                   (printf "leader finds enough negative nancys for ~a\n" (ref title))
+                                      (assert (book-of-the-month (! title))))))
+                 (when (> (set-count (! nays))
+                          (/ (set-count (! members)) 2))
+                   (printf "leader finds enough negative nancys for ~a\n" (! title))
                    (stop poll-members (next-book))))
              ;; begin/dataflow is a problem for simulation checking
              #;(begin/dataflow
                ;; count the leader as a 'yay'
-               (when (>= (set-count (ref yays))
-                         (/ (set-count (ref members)) 2))
-                 (printf "leader finds enough affirmation for ~a\n" (ref title))
+               (when (>= (set-count (! yays))
+                         (/ (set-count (! members)) 2))
+                 (printf "leader finds enough affirmation for ~a\n" (! title))
                  (stop get-quotes
                        (start-facet announce
-                         (assert (book-of-the-month (ref title))))))
-               (when (> (set-count (ref nays))
-                        (/ (set-count (ref members)) 2))
-                 (printf "leader finds enough negative nancys for ~a\n" (ref title))
+                         (assert (book-of-the-month (! title))))))
+               (when (> (set-count (! nays))
+                        (/ (set-count (! members)) 2))
+                 (printf "leader finds enough negative nancys for ~a\n" (! title))
                  (stop poll-members (next-book)))))])))))))
 
 (define-type-alias member-role

racket/typed/examples/cell.rkt

@@ -22,7 +22,7 @@
   (Role (cell-factory)
         (Reacts (Message (CreateCellT ID Value))
                 ;; want to say that what it spawns is a Cell
-                (Spawns ★/t))))
+                (ActorWithRole ★/t Cell))))
 
 (define-type-alias Reader
   (Role (reader)

racket/typed/examples/flink.rkt

@@ -161,12 +161,12 @@ The JobManager then performs the job and, when finished, asserts
      (Observe (Observe (TaskPerformance ID ★/t ★/t)))
      (JobManagerAlive)
      (Observe (JobManagerAlive))
-     (Observe (TaskRunner ★/t))
+     (Observe★ TaskRunner)
      (TaskManager ID Int)
-     (Observe (TaskManager ★/t ★/t))
+     (Observe★ TaskManager)
      (JobCompletion ID (List InputTask) TaskResult)
      (Observe (JobCompletion ID (List InputTask) ★/t))
-     (Observe (Observe (JobCompletion ★/t ★/t ★/t)))))
+     (Observe (Observe★ JobCompletion))))
 
 ;; ---------------------------------------------------------------------------------------------------
 ;; Util Macros
@@ -471,7 +471,7 @@ The JobManager then performs the job and, when finished, asserts
       ;; Requires (task-ready? t)
       (define (∀ (ρ) (perform-task [t : ConcreteTask]
                                    [k : (proc TaskID TaskResult -> ★/t
-                                              #:roles (ρ))]))
+                                              #:effects (ρ))]))
         (start-facet perform
          (on start (set! tasks-in-progress (add1 (ref tasks-in-progress))))
          (on stop (set! tasks-in-progress (sub1 (ref tasks-in-progress))))
@@ -479,8 +479,8 @@ The JobManager then performs the job and, when finished, asserts
          (log "JM begins on task ~a" this-id)
 
          ;; ID -> ...
-         (define (assign-task [mngr : ID]
-                              [request-again! : (→fn ★/t)])
+         (define (∀ (ρ) (assign-task [mngr : ID]
+                                     [request-again! : (proc -> ★/t #:effects (ρ))]))
            (start-facet assign
             (on (retracted (task-manager mngr _))
                 ;; our task manager has crashed

racket/typed/examples/observe-star.rkt

@@ -0,0 +1,21 @@
+#lang typed/syndicate
+;; Expected Output:
+;; got: new
+
+(define-constructor* (something : SomethingT new blue)
+  #:with Something (SomethingT String Int))
+
+(define-type-alias τc
+  (U Something
+     (Observe★ SomethingT)))
+
+(run-ground-dataspace
+ τc
+ (spawn
+  (start-facet _
+    (assert (something "new" 42))))
+ (spawn
+  (start-facet _
+    (on (asserted (something $x 42))
+        (printf "got: ~a\n" x))))
+ )

racket/typed/examples/require-struct/client2.rkt

@@ -0,0 +1,17 @@
+#lang typed/syndicate
+
+;; using different syntax than "client.rkt"
+
+(require/typed "driver.rkt" [#:struct msg])
+
+(define m : (MsgT Int String) (msg 1 "hi"))
+
+(msg-in m)
+(msg-out m)
+
+(match m
+  [(msg (bind x Int) discard)
+   (displayln x)])
+
+;; error: msg/checked: arity mismatch
+#;(msg 1 2 3)

racket/typed/examples/with-facets.rkt

@@ -0,0 +1,22 @@
+#lang typed/syndicate
+
+(define (wf1)
+(spawn
+ (with-facets
+   ([onn (facet (assert (tuple 'on))
+                (on start (printf "on\n")))]
+    [off (facet (on (asserted (tuple 'go))
+                    (stop off
+                          (start onn)))
+                (on start (printf "off\n")))])
+   off)))
+
+(run-ground-dataspace
+ (wf1)
+ (spawn (start-facet _ (assert (tuple 'go)))))
+
+;; BAD
+#;(spawn
+ (with-facets
+   [on (facet (on start (start on)))]
+   on))

racket/typed/info.rkt

@@ -9,4 +9,5 @@
 (define test-omit-paths
   ;; a number of the examples use SPIN for model checking which I need
   ;; to figure out how to get working on the package server
-  '("examples/"))
+  '("examples/"
+    "tests/spin/"))

racket/typed/scribblings/typed-syndicate.scrbl

@@ -364,7 +364,9 @@ Like @racket[during], but spawns an actor for the behavior @racket[expr ...].
                         (code:line #:on-add on-add-expr))
           (maybe-on-remove (code:line)
                            (code:line #:on-remove on-remove-expr))]]{
-Equivalent to the untyped @racket[untyped:define/query-value].
+Equivalent to the untyped @racket[untyped:define/query-value]. The
+@racket[on-add-expr] and @racket[on-remove-expr], when given, execute after
+@racket[name] has been updated.
 }
 
 @defform[(define/query-set name pattern expr

racket/typed/syndicate/compile-spin.rkt

@@ -6,10 +6,11 @@
 (require "ltl.rkt")
 (require racket/runtime-path)
 (require syndicate/trace syndicate/trace/msd)
-(require (prefix-in synd: (only-in syndicate/core assert retract))
+(require (prefix-in synd: (only-in syndicate/core assert retract message))
          (prefix-in synd: (only-in syndicate/patch patch-empty patch-seq)))
 
 (require (only-in racket/hash hash-union))
+(require syntax/parse/define)
 
 (module+ test
   (require rackunit)
@@ -18,12 +19,22 @@
 
 
 ;; a SpinProgram is a
-;;   (sprog Assignment [Listof SpinProcess] MessageTable SpinLTL NameEnvironment)
-(struct sprog [assignment procs spec msg-tabe name-env] #:transparent)
+;;   (sprog Assignment
+;;          [Listof SpinProcess]
+;;          MessageTable
+;;          SpinLTL
+;;          [Setof SName]
+;;          NameEnvironment)
+(struct sprog [assignment procs spec msg-tabe assertion-tys name-env] #:transparent)
 
 ;; a SpinProcess is a
-;;   (sproc SName [Setof SName] Assignment [Listof SAction] [Setof SpinState])
-(struct sproc [name state-names locals init-actions states] #:transparent)
+;;   (sproc SName
+;;          [Setof SName]
+;;          SName
+;;          Assignment
+;;          [Listof SAction]
+;;          [Setof SpinState])
+(struct sproc [name state-names st0 locals init-actions states] #:transparent)
 
 ;; an Assignment is a [Hashof SVar SValue]
 
@@ -58,6 +69,7 @@
 ;; a SAction is one of
 ;;   - (assert ?)
 ;;   - (retract ?)
+;;   - (unlearn ?)
 ;;   - (send ?)
 ;;   - (incorporate D+)
 ;;   - (add-message-interest ?)
@@ -65,6 +77,7 @@
 ;;   - (transition-to SName)
 (struct assert [ty] #:prefab)
 (struct retract [ty] #:prefab)
+(struct unlearn [ty] #:prefab)
 (struct add-message-interest [ty] #:prefab)
 (struct remove-message-interest [ty] #:prefab)
 ;; send defined in proto.rkt
@@ -90,22 +103,23 @@
   (define assertion-tys (all-assertions rgs))
   (define message-tys (all-messages rgs))
   (define event-tys (all-events rgs))
+  (define-values (spec-asserts spec-msgs) (spec-types spec))
   (define-values (message-evts assertion-evts) (set-partition Message? event-tys))
   (define msg-event-tys (list->set (set-map message-evts Message-ty)))
-  (define msg-bodies (set-union message-tys msg-event-tys))
-  (define event-subty# (make-event-map assertion-tys assertion-evts))
-  (define all-assertion-tys (set-union assertion-tys assertion-evts))
+  (define msg-bodies (set-union message-tys msg-event-tys spec-msgs))
+  (define event-subty# (make-event-map assertion-tys (set-union assertion-evts spec-asserts)))
+  (define all-assertion-tys (set-union assertion-tys assertion-evts spec-asserts))
   (define all-mentioned-tys (set-union all-assertion-tys msg-bodies))
   (define name-env (make-name-env all-mentioned-tys))
   (define procs (for/list ([rg rgs]) (rg->spin rg event-subty# name-env)))
   (define assertion-vars (initial-assertion-vars-for all-assertion-tys name-env))
+  (define assertion-nms (for/set ([τ (in-set all-assertion-tys)]) (hash-ref name-env τ)))
   (define messages-vars (initial-message-vars-for msg-bodies name-env))
   (define mailbox-vars (initial-mailbox-vars msg-bodies (map sproc-name procs) name-env))
   (define msg-table (make-message-table message-tys msg-event-tys name-env))
-  ;; TODO : should make sure all types mentioned in spec have variables, too
   (define globals (hash-union assertion-vars messages-vars mailbox-vars))
   (define spec-spin (rename-ltl spec name-env))
-  (sprog globals procs spec-spin msg-table name-env))
+  (sprog globals procs spec-spin msg-table assertion-nms name-env))
 
 ;; [Setof τ] [Setof τ] NameEnvironment -> MessageTable
 (define (make-message-table message-tys msg-event-tys name-env)
@@ -131,19 +145,22 @@
   (define all-events (all-event-types (in-hash-values states)))
   (define state-renaming (make-state-rename (hash-keys states)))
   (define states- (for/list ([st (in-hash-values states)])
-                    (state->spin st states event-subty# name-env state-renaming)))
+                    (state->spin st states all-events event-subty# name-env state-renaming)))
   (define st0- (hash-ref state-renaming st0))
   ;; ergh the invariant for when I tack on _assertions to a name is getting tricksy
   (define st0-asserts (state-assertions (hash-ref states st0)))
   (define st0-msg-interests (message-transitions (state-transitions (hash-ref states st0))))
-  (define initial-asserts (transition-assertions (set) st0-asserts event-subty# name-env))
+  (define initial-asserts (transition-assertions (set) st0-asserts all-events event-subty# name-env))
   (define initial-msg-interests (transition-msg-interests (set) st0-msg-interests event-subty# name-env))
   (define init-acts (append initial-asserts initial-msg-interests))
   (define assignment (local-variables-for st0- all-events name-env))
-  (sproc name (hash-values-set state-renaming) assignment init-acts (list->set states-)))
+  (define relevant-assertions (for/set ([evt (in-set all-events)]
+                                         #:unless (Message? evt))
+                                (hash-ref name-env evt)))
+  (sproc name (hash-values-set state-renaming) st0- relevant-assertions init-acts (list->set states-)))
 
-;; State [Sequenceof State] [Hashof τ [Setof τ]] NameEnvironment [Hashof StateName SName] -> SpinState
-(define (state->spin st states event-subty# name-env state-env)
+;; State [Sequenceof State] [Setof [U τ (Message τ)]] [Hashof τ [Setof τ]] NameEnvironment [Hashof StateName SName] -> SpinState
+(define (state->spin st states all-events event-subty# name-env state-env)
   (match-define (state name transitions assertions) st)
   (define name- (hash-ref state-env name))
   (define msg-txns (message-transitions transitions))
@@ -153,7 +170,7 @@
                      (match-define (state _ dest-txns dest-assertions) (hash-ref states dest))
                      (define dest- (hash-ref state-env dest))
                      (define dest-msg-txns (message-transitions dest-txns))
-                     (branch-on D+ assertions msg-txns dest- dest-assertions dest-msg-txns effs event-subty# name-env)))
+                     (branch-on D+ assertions msg-txns dest- dest-assertions dest-msg-txns effs all-events event-subty# name-env)))
   (sstate name- branches))
 
 ;; (Hashof D+ _) -> (Setof τ)
@@ -182,6 +199,10 @@
 (define (assertions-var-name s)
   (string->symbol (format "~a_assertions" s)))
 
+;; SName -> SName
+(define (assertions-update-var-name s)
+  (string->symbol (format "~a_update" s)))
+
 ;; SName -> SName
 (define (active-var-name s)
   (string->symbol (format "know_~a" s)))
@@ -220,8 +241,10 @@
 
 ;; [Setof τ] NameEnvironment -> Assignment
 (define (initial-assertion-vars-for assertion-tys name-env)
-  (for/hash ([τ (in-set assertion-tys)])
-    (values (svar (assertions-var-name (hash-ref name-env τ)) SInt)
+  (for*/hash ([τ (in-set assertion-tys)]
+              [bucket? (in-list '(#t #f))])
+    (define namer (if bucket? assertions-var-name assertions-update-var-name))
+    (values (svar (namer (hash-ref name-env τ)) SInt)
             0)))
 
 ;; [Setof τ] NameEnvironment -> Assignment
@@ -281,7 +304,7 @@
     (set-union as (all-events-of rg)))
   )
 
-;; [Sequenceof State] -> ?
+;; [Sequenceof State] -> [Setof [U τ (Message τ)]]
 (define (all-event-types states)
   (for*/set ([st states]
              [D+ (in-hash-keys (state-transitions st))])
@@ -293,6 +316,34 @@
       [_
        (raise-argument-error 'all-event-types "internal events not allowed" D+)])))
 
+;; SpinLTL -> (Values (Setof τ) (Setof τ))
+;; extract the types of assertions and messages mentioned in a spec
+(define (spec-types ltl)
+  (let loop ([ltls (list ltl)]
+             [asserts (set)]
+             [msgs (set)])
+    (match ltls
+      ['()
+       (values asserts msgs)]
+      [(cons ltl more-ltls)
+       (match ltl
+         [(or (always more-ltl)
+              (eventually more-ltl)
+              (ltl-not more-ltl))
+          (loop (cons more-ltl more-ltls) asserts msgs)]
+         [(or (weak-until ltl1 ltl2)
+              (strong-until ltl1 ltl2)
+              (ltl-implies ltl1 ltl2)
+              (ltl-and ltl1 ltl2)
+              (ltl-or ltl1 ltl2))
+          (loop (list* ltl1 ltl2 more-ltls) asserts msgs)]
+         [(atomic (Message τ))
+          (loop more-ltls asserts (set-add msgs τ))]
+         [(atomic τ)
+          (loop more-ltls (set-add asserts τ) msgs)]
+         [_
+          (loop more-ltls asserts msgs)])])))
+
 ;; SName [Setof [U τ D+] NameEnvironment -> Assignment
 (define (local-variables-for st0 all-events name-env)
   (define assign
@@ -301,11 +352,18 @@
       (values (svar (active-var-name (hash-ref name-env evt))
                     SBool)
               #f)))
-  (hash-set assign CURRENT-STATE st0))
+  assign
+  #;(hash-set assign CURRENT-STATE st0))
 
-;; D+ [Setof τ] [Setof τ] SName [Setof τ] [Setof τ] [Listof TransitionEffect] [Hashof τ [Setof τ]] NameEnvironment -> SBranch
-(define (branch-on D+ curr-assertions curr-msg-txns dest dest-assertions dest-msg-txns effs event-subty# name-env)
-  (define assertion-updates (transition-assertions curr-assertions dest-assertions event-subty# name-env))
+;; [Setof SName] -> Void
+(define (update-knowledge relevant-assertions)
+  (for ([assert-nm (in-set relevant-assertions)])
+    (define know-nm (active-var-name assert-nm))
+    (indent) (printf "~a = (~a -> ASSERTED(~a) : ~a);\n" know-nm know-nm assert-nm know-nm)))
+
+;; D+ [Setof τ] [Setof τ] SName [Setof τ] [Setof τ] [Listof TransitionEffect] [Setof [U τ (Message τ)]] [Hashof τ [Setof τ]] NameEnvironment -> SBranch
+(define (branch-on D+ curr-assertions curr-msg-txns dest dest-assertions dest-msg-txns effs all-events event-subty# name-env)
+  (define assertion-updates (transition-assertions curr-assertions dest-assertions all-events event-subty# name-env))
   (define msg-interest-updates (transition-msg-interests curr-msg-txns dest-msg-txns event-subty# name-env))
   (define effs- (rename-effects effs name-env))
   (define renamed-evt (rename-event D+ name-env))
@@ -315,14 +373,18 @@
                                            msg-interest-updates
                                            effs-))))
 
-;; [Setof τ] [Setof τ] [Hashof τ [Setof τ]] NameEnvironment -> [Listof SAction]
-(define (transition-assertions curr-assertions dest-assertions event-subty# name-env)
+;; [Setof τ] [Setof τ] [Setof [U τ (Message τ)]] [Hashof τ [Setof τ]] NameEnvironment -> [Listof SAction]
+(define (transition-assertions curr-assertions dest-assertions all-events event-subty# name-env)
   (define new-assertions (super-type-closure (set-subtract dest-assertions curr-assertions) event-subty#))
   (define retractions (super-type-closure (set-subtract curr-assertions dest-assertions) event-subty#))
   (define (lookup ty) (hash-ref name-env ty))
   (define asserts (set-map new-assertions (compose assert lookup)))
   (define retracts (set-map retractions (compose retract lookup)))
-  (append asserts retracts))
+  (define unlearns (for/list ([τ (in-set retractions)]
+                              #:when (and (Observe? τ)
+                                          (set-member? all-events (Observe-ty τ))))
+                     (unlearn (lookup (Observe-ty τ)))))
+  (append asserts retracts unlearns))
 
 ;; [Setof τ] [Setof τ] [Hashof τ [Setof τ]] NameEnvironment -> [Listof SAction]
 (define (transition-msg-interests curr-msg-txns dest-msg-txns event-subty# name-env)
@@ -528,33 +590,101 @@
 ;; SpinProgram -> Void
 (define (gen-spin prog)
   (match prog
-    [(sprog assignment procs spec msg-table name-env)
+    [(sprog assignment procs spec msg-table assertion-tys name-env)
      (display SPIN-PRELUDE)
      (gen-assignment assignment)
      (newline)
+     (gen-assign GLOBAL-CLOCK-VAR GLOBAL-CLOCK-INIT-VAL #:declare #t)
      (for ([p procs])
        (gen-spin-proc p name-env)
        (newline))
-     (gen-msg-dispatcher msg-table (map sproc-name procs))
+     (gen-clock-ticker (map sproc-name procs) msg-table assertion-tys)
+     (newline)
      (gen-spec "spec" (lambda () (gen-ltl spec)))
      (newline)
      (gen-sanity-ltl assignment)]))
 
+;; (-> Void) -> Void
+;; generate the prelude for spin atomic sequences, call `gen-bdy`,
+;; then end the atomic block
+(define (with-spin-atomic* gen-bdy)
+  (indent) (displayln "atomic {")
+  (with-indent (gen-bdy))
+  (indent) (displayln "}"))
+
+(define-syntax-parse-rule (with-spin-atomic bdy ...+)
+  (with-spin-atomic* (lambda () bdy ...)))
+
+;; (-> Void) -> Void
+;; generate the prelude for spin dstep sequences, call `gen-bdy`,
+;; then end the dstep block
+(define (gen-spin-dstep gen-bdy)
+  (indent) (printf "d_step { ~a\n" (format-as-comment DSTEP-EVENT))
+  (with-indent (gen-bdy))
+  (indent) (displayln "}"))
+
+(define-syntax-parse-rule (with-spin-dstep bdy ...+)
+  (gen-spin-dstep (lambda () bdy ...)))
+
+;; (-> Void) -> Void
+(define (gen-spin-if gen-bdy)
+  (indent) (displayln "if")
+  (with-indent (gen-bdy))
+  (indent) (displayln "fi;"))
+
+(define-syntax-parse-rule (with-spin-if bdy ...+)
+  (gen-spin-if (lambda () bdy ...)))
+
+;; (-> Void) -> Void
+(define (gen-spin-do gen-bdy)
+  (indent) (displayln "do")
+  (with-indent (gen-bdy))
+  (indent) (displayln "od;"))
+
+(define-syntax-parse-rule (with-spin-do bdy ...+)
+  (gen-spin-do (lambda () bdy ...)))
+
+(define (gen-spin-branch pred gen-body [comment ""])
+  (indent) (printf ":: ~a -> ~a\n" pred comment)
+  (with-indent (gen-body)))
+
+(define-syntax-parse-rule (with-spin-branch pred (~optional (~seq #:comment comment))
+                            body ...+)
+  (gen-spin-branch pred (lambda () body ...) (~? comment)))
+
+(define (gen-spin-break)
+  (indent) (displayln "break;"))
+
+(define (gen-spin-skip)
+  (indent) (displayln "skip;"))
+
 ;; SpinProcess NameEnvironment -> Void
 (define (gen-spin-proc proc name-env)
-  (match-define (sproc name state-names locals init-actions states) proc)
+  (match-define (sproc name state-names st0 relevant-assertions init-actions states) proc)
+  (define my-clock (proc-clock-var name))
+  (define locals (for/hash ([evt (in-set relevant-assertions)])
+                   (values (svar (active-var-name evt)
+                                 SBool)
+                           #f)))
   (indent) (declare-mtype state-names)
+  (indent) (gen-assign my-clock GLOBAL-CLOCK-INIT-VAL #:declare #t)
   (indent) (printf "active proctype ~a() {\n" name)
   (with-indent
+    (gen-assign CURRENT-STATE st0 #:declare #t)
     (gen-assignment locals)
-    (indent) (displayln "atomic {")
-    (for ([a init-actions])
-      (gen-spin-form a name-env name))
-    (indent) (displayln "}")
-    (indent) (displayln "end: do")
+    (with-spin-atomic
+      (for ([a init-actions])
+        (gen-spin-form a name-env name)))
+    (indent) (printf "~a: do\n" (format-end-label name))
     (with-indent
-      (for ([st states])
-        (gen-spin-form st name-env name)))
+      (with-spin-branch "true"
+        (indent) (printf "~a;\n" (clock-predicate my-clock))
+        (with-spin-atomic
+          (indent) (update-clock my-clock)
+          (with-spin-do
+            (for ([st states])
+              (gen-spin-form st name-env name)))
+          (update-knowledge relevant-assertions))))
     (indent) (displayln "od;"))
   (indent) (displayln "}"))
 
@@ -566,26 +696,26 @@
      (cond
        [(empty? branches)
         ;; no transitions out of this state
-        (indent) (displayln "end: false;")]
+        #;(gen-spin-skip) (gen-spin-break)
+        ]
        [else
         (with-indent
-          (indent) (displayln "if")
-          (with-indent
+          (with-spin-if
             (for ([branch branches])
-              (gen-spin-form branch name-env proc-name)))
-          (indent) (displayln "fi;"))])]
+              (gen-spin-form branch name-env proc-name))
+            (gen-spin-branch "else" #;gen-spin-skip gen-spin-break)))])]
     [(sbranch event dest actions)
      (indent) (printf ":: ~a -> ~a\n" (predicate-for event proc-name) (embed-event-as-comment event name-env))
      (with-indent
-       (indent) (displayln "atomic {")
        (with-indent
          (for ([act actions])
-           (gen-spin-form act name-env proc-name)))
-       (indent) (displayln "}"))]
+           (gen-spin-form act name-env proc-name))))]
     [(assert x)
      (indent) (printf "ASSERT(~a); ~a\n" x (embed-value-as-comment assert x name-env))]
     [(retract x)
      (indent) (printf "RETRACT(~a); ~a\n" x (embed-value-as-comment retract x name-env))]
+    [(unlearn x)
+     (indent) (printf "~a = false;\n" (active-var-name x))]
     [(send x)
      (indent) (printf "SEND(~a); ~a\n" x (embed-value-as-comment send x name-env))]
     [(add-message-interest x)
@@ -599,29 +729,42 @@
     [(transition-to dest)
      (indent) (printf "~a = ~a;\n" (svar-name CURRENT-STATE) dest)]))
 
-;; MessageTable [Listof SName] -> Void
-(define (gen-msg-dispatcher msg-table proc-names)
-  (unless (hash-empty? msg-table)
-    (indent) (displayln "active proctype __msg_dispatcher__() {")
-    (with-indent
-      (indent) (displayln "end: do")
-      (with-indent
-        (for ([(sent-msg matching-evts) (in-hash msg-table)])
-          (gen-msg-dispatch sent-msg matching-evts proc-names)))
-      (indent) (displayln "od;"))
-    (indent) (displayln "}")))
+;; [Listof SName] MessageTable -> Void
+(define (gen-clock-ticker proc-names msg-table assertion-tys)
+  (define clock-names (for/list ([pn (in-list proc-names)])
+                        (svar-name (proc-clock-var pn))))
+  (indent) (displayln "active proctype __clock_ticker__() {")
+  (with-indent
+    (indent) (displayln "end_clock_ticker:")
+    (with-spin-do
+      (with-spin-branch (all-procs-ready-predicate clock-names)
+        (with-spin-dstep
+          (indent) (update-clock GLOBAL-CLOCK-VAR (format-as-comment TURN-BEGIN-EVENT))
+          (update-all-assertion-vars assertion-tys)
+          (unless (hash-empty? msg-table)
+            (with-spin-do
+              (gen-spin-branch "else" gen-spin-break)
+              (for ([(sent-msg matching-evts) (in-hash msg-table)])
+                (gen-msg-dispatch sent-msg matching-evts proc-names))))))))
+  (indent) (displayln "}"))
+
+;; (Setof SName) -> Void
+;; update the assertion bucket variables based on the update variables
+(define (update-all-assertion-vars assertion-nms)
+  (for ([assertion (in-set assertion-nms)])
+    (define bucket (assertions-var-name assertion))
+    (define update (assertions-update-var-name assertion))
+    (indent) (printf "~a = ~a + ~a;\n" bucket bucket update)
+    (indent) (printf "~a = 0;\n" update)))
 
 ;; SName (Setof SName) [Listof SName] -> Void
 (define (gen-msg-dispatch sent-msg matching-evts proc-names)
   (define mailbox-nm (messages-var-name sent-msg))
   (indent) (printf ":: ~a > 0 ->\n" mailbox-nm)
   (with-indent
-    (indent) (displayln "atomic {")
-    (with-indent
-      (indent) (printf "~a--;\n" mailbox-nm)
-      (for ([proc (in-list proc-names)])
-        (dispatch-to matching-evts proc)))
-    (indent) (displayln "}")))
+    (indent) (printf "~a--;\n" mailbox-nm)
+    (for ([proc (in-list proc-names)])
+      (dispatch-to matching-evts proc))))
 
 ;; [Setof SName] SName -> Void
 (define (dispatch-to matching-evts proc)
@@ -643,12 +786,16 @@
 ;; Assignment -> Void
 (define (gen-assignment assign)
   (for ([(var val) (in-hash assign)])
-    (indent) (printf "~a = ~a;\n"
-                     (declare-var var)
-                     (spin-val->string val))))
+    (gen-assign var val #:declare #t)))
 
-;; SVar -> Void
-(define (declare-var var)
+;; SVar SValue [Bool] -> Void
+(define (gen-assign var val #:declare [declare? #f])
+  (indent) (printf "~a = ~a;\n"
+                   (if declare? (var-decl var) (svar-name var))
+                   (spin-val->string val)))
+
+;; SVar -> String
+(define (var-decl var)
   (match-define (svar name ty) var)
   (format "~a ~a" (spin-type->string ty) name))
 
@@ -665,7 +812,7 @@
 ;; SType -> String
 (define (spin-type->string ty)
   (match ty
-    [(== SInt) "int"]
+    [(== SInt) "short"]
     [(== SBool) "bool"]
     [(== mtype) "mtype"]))
 
@@ -709,7 +856,11 @@
 ;; (τ -> Any) SName NameEnvironment -> String
 (define (embed-value-as-comment tag sname name-env)
   (define ty (reverse-lookup name-env sname))
-  (format "/*~a*/" (tag ty)))
+  (format-as-comment (tag ty)))
+
+;; Any -> String
+(define (format-as-comment v)
+  (format "/*~a*/" v))
 
 ;; NameEnvironment SName -> τ
 (define (reverse-lookup name-env sname)
@@ -717,6 +868,35 @@
               #:when (equal? v sname))
     k))
 
+;; String -> String
+;; format a suitable end label based on the process/state name
+(define (format-end-label s)
+  (format "end_~a" s))
+
+;; SName -> SVar
+;; SVar for a process's clock
+(define (proc-clock-var proc-name)
+  (svar (string->symbol (format "~a_clock" proc-name))
+        SBool))
+
+(define GLOBAL-CLOCK-VAR (svar 'GLOBAL_CLOCK SBool))
+(define GLOBAL-CLOCK-INIT-VAL #t)
+
+;; SVar -> String
+(define (clock-predicate clock-var)
+  (format "~a == ~a" (svar-name clock-var) (svar-name GLOBAL-CLOCK-VAR)))
+
+;; SVar -> Void
+(define (update-clock clock [comment ""])
+  (printf "~a = !~a;~a\n" (svar-name clock) (svar-name clock) comment))
+
+;; (Listof SName) -> String
+(define (all-procs-ready-predicate clock-names)
+  (define global-name (svar-name GLOBAL-CLOCK-VAR))
+  (define preds (for/list ([cn (in-list clock-names)])
+                  (format "(~a != ~a)" global-name cn)))
+  (string-join preds " && "))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; LTL
 
@@ -746,6 +926,8 @@
      (gen-ltl-bin-op "W" p q)]
     [(strong-until p q)
      (gen-ltl-bin-op "U" p q)]
+    [(release p q)
+     (gen-ltl-bin-op "V" p q)]
     [(ltl-implies p q)
      (gen-ltl-bin-op "->" p q)]
     [(ltl-and p q)
@@ -775,12 +957,17 @@
   (indent) (display "(") (gen-ltl q) (displayln ")"))
 
 ;; Assignment -> Void
+;; SPIN sometimes errors (seemingly in the front end) if this is "too big." What
+;; constitutes too big seems to change. At first setting the limit to 33 worked,
+;; but then I lowered it again, so IDK. It gives an error message like:
+;;   tl_spin: expected ')', saw 'predicate'
 (define (gen-sanity-ltl assignment)
   (gen-spec "sanity"
             (lambda ()
               (indent) (displayln "[](")
               (with-indent
-                (for ([assertion-var (in-hash-keys assignment)])
+                (for ([assertion-var (in-hash-keys assignment)]
+                      [i (in-range 14)])
                   (indent) (printf "~a >= 0 &&\n" (svar-name assertion-var)))
                 (indent) (displayln "true"))
               (indent) (displayln ")"))))
@@ -793,25 +980,38 @@
 
 ;; [LTL τ] [Listof Role] -> Bool
 (define (compile+verify spec roles)
-  (define role-graphs (for/list ([r (in-list roles)]) (compile/internal-events (compile r))))
-  (run-spin (program->spin role-graphs spec)))
+  (let/ec stop
+    (define role-graphs
+      (for/list ([r (in-list roles)])
+        (define ans (compile/internal-events (compile r)))
+        (when (detected-cycle? ans)
+          (printf "detected cycle!\n")
+          (describe-detected-cycle ans)
+          (stop #f))
+        ans))
+    (run-spin (program->spin role-graphs spec))))
 
 ;; SpinThang String -> Bool
 (define (run-spin spin [spec-name "spec"])
   (define tmp (make-temporary-file "typed-syndicate-spin~a.pml"))
   (gen-spin/to-file spin tmp)
-  (define out (with-output-to-string
-                (thunk (system* RUN-SPIN.EXE tmp spec-name))))
+  (define-values (script-completed? script-output script-err)
+    (run-script RUN-SPIN.EXE (list tmp spec-name)))
   (define trail-file (format "~a.trail" (path->string tmp)))
   (define trail-exists? (file-exists? trail-file))
-  (when (file-exists? trail-file)
-    (displayln "Detected Trail File!")
-    (analyze-spin-trail tmp)
-    (copy-file tmp (build-path (current-directory) "model.pml") #t)
-    (copy-file trail-file (build-path (current-directory) "model.pml.trail") #t)
-    (delete-file trail-file))
+  (cond
+    [(not script-completed?)
+     (displayln "Error running SPIN; Output:")
+     (display script-err)
+     (display script-output)]
+    [trail-exists?
+       (displayln "Detected Trail File!")
+       (copy-file tmp (build-path (current-directory) "model.pml") #t)
+       (copy-file trail-file (build-path (current-directory) "model.pml.trail") #t)
+       (analyze-spin-trail tmp)
+       (delete-file trail-file)])
   (delete-file tmp)
-  (not trail-exists?))
+  (and script-completed? (not trail-exists?)))
 
 (define SPIN-REPORT-RX #px"(?m:^State-vector \\d+ byte, depth reached \\d+, errors: (\\d+)$)")
 
@@ -829,19 +1029,32 @@ Examples:
   4:	proc  2 (proc824:1) model.pml:140 (state 2)	[ClubMemberT_String_assertions = (ClubMemberT_String_assertions+1)]
   <<<<<START OF CYCLE>>>>>
 |#
-(define TRAIL-LINE-RX #px"(?m:^  <<<<<START OF CYCLE>>>>>|^\\s*\\d+:\\s*proc\\s*(\\d+)\\s*\\(.*\\) \\S+\\.pml:(\\d+))")
+(define TRAIL-LINE-RX #px"(?m:^\\s*<<<<<START OF CYCLE>>>>>|^\\s*\\d+:\\s*proc\\s*(\\d+)\\s*\\(.*\\) \\S+\\.pml:(\\d+))")
 
 ;; Path -> Void
 ;; assume the trail file exists in the same directory as the spin (model) file
 (define (analyze-spin-trail spin-file)
-  (define out (with-output-to-string
-                (thunk (system* REPLAY-TRAIL.EXE spin-file))))
-  (pretty-display out)
-  (define pid/line-trace (regexp-match* TRAIL-LINE-RX out #:match-select cdr))
-  (define model-lines (file->vector spin-file))
-  (define trace (interpret-spin-trace pid/line-trace model-lines))
+  (define-values (_ out __) (run-script REPLAY-TRAIL.EXE (list spin-file)))
+  #;(pretty-display out)
+  (define trace (spin-trace->syndicate-trace out spin-file))
   (print-trace trace)
-  (log-trace-msd trace))
+  #;(log-trace-msd trace))
+
+;; String Path -> (Listof TraceStep)
+(define (spin-trace->syndicate-trace spin-out spin-file)
+  (define pid/line-trace (regexp-match* TRAIL-LINE-RX spin-out #:match-select cdr))
+  (define model-lines (file->vector spin-file))
+  (interpret-spin-trace pid/line-trace model-lines))
+
+;; String (Listof String) -> (Values Bool String String)
+(define (run-script cmd args)
+  (match-define (list stdo stdin pid stderr ctrl)
+    (apply process* cmd args))
+  (define script-output (port->string stdo))
+  (define script-err (port->string stderr))
+  (define script-completed? (equal? (ctrl 'status) 'done-ok))
+  (close-output-port stdin)
+  (values script-completed? script-output script-err))
 
 ;; a PID is a Nat
 
@@ -856,6 +1069,13 @@ Examples:
 ;;   - (retract τ)
 ;;   - (Asserted τ)
 ;;   - (Retracted τ)
+;;   - 'dstep
+;;   - 'turn-begin
+
+;; the first statement in a d_step sequence (possibly atomic too) has the line
+;; number of the d_step block itself in the trace
+(define DSTEP-EVENT 'dstep)
+(define TURN-BEGIN-EVENT 'turn-begin)
 
 ;; (Listof (List String String)) (Vectorof String) -> (Listof TraceStep)
 (define (interpret-spin-trace pid/line-trace model-lines)
@@ -865,71 +1085,102 @@ Examples:
         ['(#f #f)
          START-OF-CYCLE]
         [(list pid-str line-no-str)
-         (define line (vector-ref model-lines (sub1 (string->number line-no-str))))
-         (define evt (extract-comment-value line))
-         (and evt
-              (trace-step (string->number pid-str) evt))]
-        )))
+         (define line-no (string->number line-no-str))
+         (extract-trace-step pid-str line-no model-lines)])))
   (filter values maybe-steps))
 
+;; String Nat (Vectorof String) -> (Maybe TraceEvent)
+(define (extract-trace-step pid-str line-no model-lines)
+  (define line (vector-ref model-lines (sub1 line-no)))
+  (define evt (extract-comment-value line))
+  (cond
+    [(equal? evt DSTEP-EVENT)
+     (extract-trace-step pid-str (add1 line-no) model-lines)]
+    [evt
+     (trace-step (string->number pid-str) evt)]
+    [else
+     #f]))
+
 ;; (Listof TraceStep) -> Void
 (define (print-trace trace)
+  (when (empty? trace)
+    (printf "Starting state of program violates specification\n"))
   (for ([ts (in-list trace)])
     (match ts
       [(== START-OF-CYCLE)
        (printf "Start of Cycle (if this is the last step that means the final state is stuttered):\n")]
       [(trace-step pid evt)
        (match evt
+         [(== TURN-BEGIN-EVENT)
+          (printf "A new turn begins\n")]
+         [(== DSTEP-EVENT)
+          (printf "\nERROR ERROR!! SAW DSTEP EVENT!! ERROR ERROR\n\n")]
          [(assert ty)
           (printf "Process ~a ASSERTS ~a\n" pid (τ->string ty))]
          [(retract ty)
           (printf "Process ~a RETRACTS ~a\n" pid (τ->string ty))]
+         [(send ty)
+          (printf "Process ~a SENDS ~a\n" pid (τ->string ty))]
          [(Asserted ty)
           (printf "Process ~a REACTS to the ASSERTION of ~a\n" pid (τ->string ty))]
          [(Retracted ty)
-          (printf "Process ~a REACTS to the RETRACTION of ~a\n" pid (τ->string ty))])])))
+          (printf "Process ~a REACTS to the RETRACTION of ~a\n" pid (τ->string ty))]
+         [(Message ty)
+          (printf "Process ~a REACTS to the MESSAGE of ~a\n" pid (τ->string ty))])])))
 
 ;; (Listof TraceStep) -> Void
 ;; use syndicate's msd logger logging
 (define (log-trace-msd trace)
   (start-tracing! "trace.msd")
-  (define (end-turn! pid point patch)
+  (define (end-turn! pid point patch messages)
     (let* ([p (trace-turn-end point pid #f)]
-           [p (trace-actions-produced p pid (list patch))]
+           [p (trace-actions-produced p pid (cons patch messages))]
            [p (trace-action-interpreted p pid patch)])
       p))
-  (define-values (final-pid final-point final-patch)
+  (define-values (final-pid final-point final-patch final-messages)
     (for/fold ([current-actor #f]
                [point #f]
-               [current-patch synd:patch-empty])
+               [current-patch synd:patch-empty]
+               [messages (list)])
               ([ts (in-list trace)])
       (match ts
         [(== START-OF-CYCLE)
-         (values current-actor point current-patch)]
+         (values current-actor point current-patch messages)]
         [(trace-step pid evt)
          (define-values (next-point next-patch)
            (cond
              ;; either startup or the begin of a new actor's turn
              [(and current-actor (not (equal? pid current-actor)))
-              (define p (end-turn! current-actor point current-patch))
+              (define p (end-turn! current-actor point current-patch messages))
               (values (trace-turn-begin p pid #f)
                       synd:patch-empty)]
              [else
               (values point current-patch)]))
          (match evt
+           [(== DSTEP-EVENT)
+            (printf "\nERROR ERROR!! SAW DSTEP EVENT!! ERROR ERROR\n\n")]
            [(assert ty)
             (define p (synd:assert ty))
-            (values pid next-point (synd:patch-seq next-patch p))]
+            (values pid next-point (synd:patch-seq next-patch p) messages)]
            [(retract ty)
             (define p (synd:retract ty))
-            (values pid next-point (synd:patch-seq next-patch p))]
+            (values pid next-point (synd:patch-seq next-patch p) messages)]
+           [(send ty)
+            (define a (synd:message ty))
+            (values pid next-point next-patch (cons a messages))]
            [(Asserted ty)
             #;(trace-event-consumed ??? ??? pid ???)
-            (values pid next-point next-patch)]
+            (values pid next-point next-patch messages)]
            [(Retracted ty)
             #;(trace-event-consumed ??? ??? pid ???)
-            (values pid next-point next-patch)])])))
-  (end-turn! final-pid final-point final-patch))
+            (values pid next-point next-patch messages)]
+           [(Message ty)
+            #;(trace-event-consumed ??? ??? pid ???)
+            (values pid next-point next-patch messages)]
+           [(or (== TURN-BEGIN-EVENT)
+                (== DSTEP-EVENT))
+            (values pid next-point next-patch messages)])])))
+  (end-turn! final-pid final-point final-patch final-messages))
 
 (define COMMENT-RX #px"/\\*(.*)\\*/")
 
@@ -944,10 +1195,13 @@ Examples:
       "extracting values back out from spin model"
     (define evt-str "        :: ASSERTED(BookQuoteT_String_Int) && !know_BookQuoteT_String_Int -> /*#s(Asserted #s(Struct BookQuoteT (#s(Base String) #s(Base Int))))*/\n")
     (define assert-str "  ASSERT(Obs_Obs_BookInterestT); /*#s(assert #s(Observe #s(Observe #s(Struct BookInterestT (#s(Base String) #s(Mk⋆) #s(Mk⋆))))))*/\n")
+    (define send-str "            SEND(FlipSwitchCmdT_Symbol); /*#s(send #s(Struct FlipSwitchCmdT (#s(Base Symbol))))*/\n")
     (check-equal? (extract-comment-value evt-str)
                   #s(Asserted #s(Struct BookQuoteT (#s(Base String) #s(Base Int)))))
     (check-equal? (extract-comment-value assert-str)
-                  #s(assert #s(Observe #s(Observe #s(Struct BookInterestT (#s(Base String) #s(Mk⋆) #s(Mk⋆)))))))))
+                  #s(assert #s(Observe #s(Observe #s(Struct BookInterestT (#s(Base String) #s(Mk⋆) #s(Mk⋆)))))))
+    (check-equal? (extract-comment-value send-str)
+                  #s(send #s(Struct FlipSwitchCmdT (#s(Base Symbol)))))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Misc Utils

racket/typed/syndicate/core-expressions.rkt

@@ -44,39 +44,30 @@
 
 ;; copied from stlc
 (define-typed-syntax (ann e (~optional (~datum :)) τ:type) ≫
-  [⊢ e ≫ e- (⇐ : τ.norm)]
-  #:fail-unless (pure? #'e-) "expression must be pure"
+  [⊢ e ≫ e- (⇐ : τ.norm) (⇒ ν (~effs eff ...))]
   ------------------------------------------------
-  [⊢ e- (⇒ : τ.norm) ])
+  [⊢ e- (⇒ : τ.norm) (⇒ ν (eff ...))])
 
 ;; copied from ext-stlc
 (define-typed-syntax if
   [(_ e_tst e1 e2) ⇐ τ-expected ≫
    [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
    #:fail-unless (pure? #'e_tst-) "expression must be pure"
-   [⊢ e1 ≫ e1- (⇐ : τ-expected)
-      (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))]
-   [⊢ e2 ≫ e2- (⇐ : τ-expected)
-      (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))]
+   [⊢ e1 ≫ e1- (⇐ : τ-expected) (⇒ ν (~effs eff1 ...))]
+   [⊢ e2 ≫ e2- (⇐ : τ-expected) (⇒ ν (~effs eff2 ...))]
    --------
    [⊢ (if- e_tst- e1- e2-)
       (⇒ : τ-expected)
-      (⇒ ν-ep (eps1 ... eps2 ...))
-      (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...))))
-      (⇒ ν-s (ss1 ... ss2 ...))]]
+      (⇒ ν #,(make-Branch #'((eff1 ...) (eff2 ...))))]]
   [(_ e_tst e1 e2) ≫
    [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy.
    #:fail-unless (pure? #'e_tst-) "expression must be pure"
-   [⊢ e1 ≫ e1- (⇒ : τ1)
-      (⇒ ν-ep (~effs eps1 ...)) (⇒ ν-f (~effs fs1 ...)) (⇒ ν-s (~effs ss1 ...))]
-   [⊢ e2 ≫ e2- (⇒ : τ2)
-      (⇒ ν-ep (~effs eps2 ...)) (⇒ ν-f (~effs fs2 ...)) (⇒ ν-s (~effs ss2 ...))]
+   [⊢ e1 ≫ e1- (⇒ : τ1) (⇒ ν (~effs eff1 ...))]
+   [⊢ e2 ≫ e2- (⇒ : τ2) (⇒ ν (~effs eff2 ...))]
    #:with τ (mk-U- #'(τ1 τ2))
    --------
    [⊢ (if- e_tst- e1- e2-) (⇒ : τ)
-      (⇒ ν-ep (eps1 ... eps2 ...))
-      (⇒ ν-f #,(make-Branch #'((fs1 ...) (fs2 ...))))
-      (⇒ ν-s (ss1 ... ss2 ...))]])
+      (⇒ ν #,(make-Branch #'((eff1 ...) (eff2 ...))))]])
 
 (define-typed-syntax (when e s ...+) ≫
   ------------------------------------
@@ -93,26 +84,18 @@
    [⊢ e ≫ e- ⇒ : τ_x] ...
    #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
    [[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇐ : τ_expected)
-                   (⇒ ν-ep (~effs eps ...))
-                   (⇒ ν-f (~effs fs ...))
-                   (⇒ ν-s (~effs ss ...))]
+                   (⇒ ν (~effs eff ...))]
    ----------------------------------------------------------
    [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_expected)
-      (⇒ ν-ep (eps ...))
-      (⇒ ν-f (fs ...))
-      (⇒ ν-s (ss ...))]]
+      (⇒ ν (eff ...))]]
   [(_ ([x e] ...) e_body ...) ≫
    [⊢ e ≫ e- ⇒ : τ_x] ...
    #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions must be pure"
    [[x ≫ x- : τ_x] ... ⊢ (block e_body ...) ≫ e_body- (⇒ : τ_body)
-                   (⇒ ν-ep (~effs eps ...))
-                   (⇒ ν-f (~effs fs ...))
-                   (⇒ ν-s (~effs ss ...))]
+                   (⇒ ν (~effs eff ...))]
    ----------------------------------------------------------
    [⊢ (let- ([x- e-] ...) e_body-) (⇒ : τ_body)
-      (⇒ ν-ep (eps ...))
-      (⇒ ν-f (fs ...))
-      (⇒ ν-s (ss ...))]])
+      (⇒ ν (eff ...))]])
 
 ;; copied from ext-stlc
 (define-typed-syntax let*
@@ -127,14 +110,10 @@
   [⊢ pred ≫ pred- (⇐ : Bool)] ...
   #:fail-unless (stx-andmap pure? #'(pred- ...)) "predicates must be pure"
   [⊢ (block s ...) ≫ s- (⇒ : τ-s)
-                   (⇒ ν-ep (~effs eps ...))
-                   (⇒ ν-f (~effs fs ...))
-                   (⇒ ν-s (~effs ss ...))] ...
+                   (⇒ ν (~effs eff ...))] ...
   ------------------------------------------------
   [⊢ (cond- [pred- s-] ...) (⇒ : (U τ-s ...))
-     (⇒ ν-ep (eps ... ...))
-     (⇒ ν-f #,(make-Branch #'((fs ...) ...)))
-     (⇒ ν-s (ss ... ...))])
+     (⇒ ν #,(make-Branch #'((eff ...) ...)))])
 
 (define else #t)
 
@@ -145,9 +124,7 @@
                      (elaborate-pattern/with-type pat #'τ-e))
   #:with (([x τ:type] ...) ...) (stx-map pat-bindings #'(p/e ...))
   [[x ≫ x- : τ.norm] ... ⊢ (block s ...) ≫ s- (⇒ : τ-s)
-                (⇒ ν-ep (~effs eps ...))
-                (⇒ ν-f (~effs fs ...))
-                (⇒ ν-s (~effs ss ...))] ...
+                (⇒ ν (~effs eff ...))] ...
   ;; REALLY not sure how to handle p/p-/p.match-pattern,
   ;; particularly w.r.t. typed terms that appear in p.match-pattern
   [⊢ p/e ≫ p-- ⇒ τ-p] ...
@@ -161,9 +138,7 @@
   [⊢ (match- e- [p- s-] ...
                 [_ (#%app- error- "incomplete pattern match")])
      (⇒ : (U τ-s ...))
-     (⇒ ν-ep #,(make-Branch #'((eps ...) ...)))
-     (⇒ ν-f #,(make-Branch #'((fs ...) ...)))
-     (⇒ ν-s #,(make-Branch #'((ss ...) ...)))])
+     (⇒ ν #,(make-Branch #'((eff ...) ...)))])
 
 
 ;; (Listof Value) -> Value
@@ -171,21 +146,21 @@
   (#%app- cons- 'tuple es))
 
 (define-typed-syntax (tuple e:expr ...) ≫
-  [⊢ e ≫ e- (⇒ : τ)] ...
-  #:fail-unless (stx-andmap pure? #'(e- ...)) "expressions not allowed to have effects"
+  [⊢ e ≫ e- (⇒ : τ) (⇒ ν (~effs F ...))] ...
   -----------------------
-  [⊢ (#%app- mk-tuple (#%app- list- e- ...)) (⇒ : (Tuple τ ...))])
+  [⊢ (#%app- mk-tuple (#%app- list- e- ...))
+     (⇒ : (Tuple τ ...))
+     (⇒ ν (F ... ...))])
 
 (define unit : Unit (tuple))
 
 (define-typed-syntax (select n:nat e:expr) ≫
-  [⊢ e ≫ e- (⇒ : (~Tuple τ ...))]
-  #:fail-unless (pure? #'e-) "expression not allowed to have effects"
+  [⊢ e ≫ e- (⇒ : (~Tuple τ ...)) (⇒ ν (~effs F ...))]
   #:do [(define i (syntax->datum #'n))]
   #:fail-unless (< i (stx-length #'(τ ...))) "index out of range"
   #:with τr (list-ref (stx->list #'(τ ...)) i)
   --------------------------------------------------------------
-  [⊢ (#%app- tuple-select n e-) (⇒ : τr)])
+  [⊢ (#%app- tuple-select n e-) (⇒ : τr) (⇒ ν (F ...))])
 
 (define- (tuple-select n t)
   (#%app- list-ref- t (#%app- add1- n)))
@@ -264,8 +239,15 @@
        (quasisyntax/loc pat
          (tuple #,@(stx-map elaborate-pattern #'(p ...))))]
       [(~constructor-exp ctor p ...)
+       (define field-tys (ctor-field-tys #'ctor))
+       (define sub-pats
+         (for/list ([field-pat (in-syntax #'(p ...))]
+                    [field-ty? (in-list field-tys)])
+           (if field-ty?
+               (elaborate-pattern/with-type field-pat field-ty?)
+               (elaborate-pattern field-pat))))
        (quasisyntax/loc pat
-         (ctor #,@(stx-map elaborate-pattern #'(p ...))))]
+         (ctor #,@sub-pats))]
       [e:expr
        #'e]))
 
@@ -376,7 +358,6 @@
   [⊢ e ≫ e- (⇒ (~Tuple τ ...))]
   #:fail-unless (stx-length=? #'(x ...) #'(τ ...))
                 "mismatched size"
-  #:fail-unless (pure? #'e-) "expr must be pure"
   #:with (sel ...) (for/list ([y (in-syntax #'(x ...))]
                               [t (in-syntax #'(τ ...))]
                               [i (in-naturals)])

racket/typed/syndicate/drivers/tcp.rkt

@@ -62,7 +62,7 @@
   (U (Observe (Observe (TcpConnection ★/t (TcpListener ★/t))))
      (Observe (TcpConnection ★/t (TcpListener Int)))
      (Observe (TcpConnection ★/t (TcpListener Int)))
-     (Advertise (Observe (TcpChannel ★/t (TcpListener (TcpHandle (Seal ★/t)) ★/t))))
+     (Advertise (Observe (TcpChannel ★/t (TcpListener (TcpHandle (Seal ★/t))) ★/t)))
      (Observe (Advertise (TcpChannel (TcpAddress String Int) (TcpHandle (Seal ★/t)) ★/t)))
      (TcpAccepted ★/t)
      (Advertise (TcpChannel (TcpHandle (Seal ★/t)) (TcpAddress String Int) ★/t))
@@ -102,7 +102,7 @@
 
 (require/typed syndicate/drivers/tcp2)
 (require/typed (submod syndicate/drivers/tcp2 syndicate-main)
-               [activate! : (→ (Computation (Value (U))
+  [activate! : (proc → (U) #:effects ((Actor Tcp2Driver))) #;(→ (Computation (Value (U))
                                             (Endpoints)
                                             (Roles)
                                             (Spawns (Actor Tcp2Driver))))])

racket/typed/syndicate/for-loops.rkt

@@ -12,7 +12,7 @@
 (require (only-in "list.rkt" List ~List))
 (require (only-in "set.rkt" Set ~Set))
 (require (only-in "hash.rkt" Hash ~Hash))
-(require (only-in "prim.rkt" Bool + #%datum))
+(require (only-in "prim.rkt" Int Bool + #%datum))
 (require (only-in "core-expressions.rkt" let unit tuple-select mk-tuple))
 (require "maybe.rkt")
 
@@ -139,18 +139,14 @@
   [[[x ≫ x-- : τ] ...]
    [[acc ≫ acc- : τ-acc] ...] ⊢ (block e-body ...) ≫ e-body-
                                (⇐ : body-ty)
-                               (⇒ ν-ep (~effs τ-ep ...))
-                               (⇒ ν-s (~effs τ-s ...))
-                               (⇒ ν-f (~effs τ-f ...))]
+                               (⇒ ν (~effs F ...))]
   -------------------------------------------------------
   [⊢ (values->tuple #,num-accs
        (for/fold- ([acc- init-] ...)
          clauses-
          #,(bind-renames #'([x-- x-] ...) #`(tuple->values #,num-accs e-body-))))
      (⇒ : body-ty)
-     (⇒ ν-ep (τ-ep ...))
-     (⇒ ν-s (τ-s ...))
-     (⇒ ν-f (τ-f ...))]]
+     (⇒ ν (F ...))]]
   [(for/fold (accs ... [acc:id init] more-accs ...)
              clauses
      e-body ...+) ≫
@@ -208,21 +204,17 @@
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
   [[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
                            (⇒ : τ-body)
-                           (⇒ ν-ep (~effs τ-ep ...))
-                           (⇒ ν-s (~effs τ-s ...))
-                           (⇒ ν-f (~effs τ-f ...))]
+                           (⇒ ν (~effs F ...))]
   ----------------------------------------------------------------------
   [⊢ (for/set- clauses-
        #,(bind-renames #'([x-- x-] ...) #'e-body-))
               (⇒ : (Set τ-body))
-              (⇒ ν-ep (τ-ep ...))
-              (⇒ ν-s (τ-s ...))
-              (⇒ ν-f (τ-f ...))])
+              (⇒ ν (F ...))])
 
 (define-typed-syntax (for/sum (clause ...)
                        e-body ...+) ≫
   ----------------------------------------------------------------------
-  [≻ (for/fold ([acc 0])
+  [≻ (for/fold ([acc Int 0])
                (clause ...)
        (+ acc (let () e-body ...)))])
 
@@ -239,9 +231,7 @@
   #:with (clauses- ([x x- τ] ...)) (analyze-for-clauses #'(clause.parend ...))
   [[x ≫ x-- : τ] ... ⊢ (block e-body ...) ≫ e-body-
                  (⇒ : τ-body)
-                 (⇒ ν-ep (~effs τ-ep ...))
-                 (⇒ ν-s (~effs τ-s ...))
-                 (⇒ ν-f (~effs τ-f ...))]
+                 (⇒ ν (~effs F ...))]
   [[res ≫ _ : τ-body] ⊢ res  ≫ res- (⇒ : _)]
   ----------------------------------------------------------------------
   [⊢ (let- ()
@@ -252,6 +242,4 @@
             (some res-)
             none))
      (⇒ : (Maybe τ-body))
-     (⇒ ν-ep (τ-ep ...))
-     (⇒ ν-s (τ-s ...))
-     (⇒ ν-f (τ-f ...))])
+     (⇒ ν (F ...))])

racket/typed/syndicate/ltl.rkt

@@ -7,9 +7,10 @@
 ;;  - (eventually [LTL X])
 ;;  - (weak-until [LTL X] [LTL X])
 ;;  - (strong-until [LTL X] [LTL X])
+;;  - (release [LTL X] [LTL X])
 ;;  - (ltl-implies [LTL X] [LTL X])
-;;  - (ltl-and [Listof [LTL X]])
-;;  - (ltl-or  [Listof [LTL X]])
+;;  - (ltl-and [LTL X] [LTL X])
+;;  - (ltl-or  [LTL X] [LTL X])
 ;;  - (ltl-not [LTL X])
 ;;  - (atomic X)
 ;;  - Bool
@@ -20,6 +21,7 @@
 (struct atomic [p] #:prefab)
 (struct weak-until [p q] #:prefab)
 (struct strong-until [p q] #:prefab)
+(struct release [p q] #:prefab)
 (struct ltl-implies [p q] #:prefab)
 (struct ltl-and [p q] #:prefab)
 (struct ltl-or [p q] #:prefab)
@@ -37,6 +39,8 @@
        (weak-until (loop p) (loop q))]
       [(strong-until p q)
        (strong-until (loop p) (loop q))]
+      [(release p q)
+       (release (loop p) (loop q))]
       [(ltl-implies p q)
        (ltl-implies (loop p) (loop q))]
       [(ltl-and p q)

racket/typed/syndicate/maybe.rkt

@@ -5,9 +5,12 @@
          None*
          Some
          some
-         none)
+         none
+         has?)
 
 (require "core-types.rkt")
+(require "prim.rkt")
+(require "core-expressions.rkt")
 
 
 (define-constructor* (none* : None*))
@@ -35,3 +38,10 @@
      (error "some")]
     [none
      (error "none")]))
+
+(define (∀ (X) (has? [v : (Maybe X)] [p : (→fn X Bool)] -> Bool))
+  (match v
+    [none
+     #f]
+    [(some $x)
+     (p x)]))

racket/typed/syndicate/prim.rkt

@@ -1,28 +1,31 @@
 #lang turnstile
 
 (provide (all-defined-out)
+         True False Bool
          (for-syntax (all-defined-out)))
 
 (require "core-types.rkt")
 (require (rename-in racket/math [exact-truncate exact-truncate-]))
-(require (postfix-in - (only-in racket/format ~a)))
+(require (postfix-in - (only-in racket/format ~a ~v)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Primitives
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(define-base-types Int Bool String ByteString Symbol)
+(define-base-types Zero NonZero String ByteString Symbol)
+
+(define-type-alias Int (U Zero NonZero))
 
 ;; hmmm
-(define-primop + (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
-(define-primop - (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
-(define-primop * (→ Int Int (Computation (Value Int) (Endpoints) (Roles) (Spawns))))
-(define-primop not (→ Bool (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop < (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop > (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop <= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop >= (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
-(define-primop = (→ Int Int (Computation (Value Bool) (Endpoints) (Roles) (Spawns))))
+(define-primop + (→fn Int Int Int))
+(define-primop - (→fn Int Int Int))
+(define-primop * (→fn Int Int Int))
+(define-primop not (→fn Bool Bool))
+(define-primop < (→fn Int Int Bool))
+(define-primop > (→fn Int Int Bool))
+(define-primop <= (→fn Int Int Bool))
+(define-primop >= (→fn Int Int Bool))
+(define-primop = (→fn Int Int Bool))
 (define-primop even? (→fn Int Bool))
 (define-primop odd? (→fn Int Bool))
 (define-primop add1 (→fn Int Int))
@@ -35,11 +38,11 @@
 (define-primop current-inexact-milliseconds (→fn Int))
 (define-primop string=? (→fn String String Bool))
 
-(define-primop bytes->string/utf-8 (→ ByteString (Computation (Value String) (Endpoints) (Roles) (Spawns))))
-(define-primop string->bytes/utf-8 (→ String (Computation (Value ByteString) (Endpoints) (Roles) (Spawns))))
-(define-primop gensym (→ Symbol (Computation (Value Symbol) (Endpoints) (Roles) (Spawns))))
-(define-primop symbol->string (→ Symbol (Computation (Value String) (Endpoints) (Roles) (Spawns))))
-(define-primop string->symbol (→ String (Computation (Value Symbol) (Endpoints) (Roles) (Spawns))))
+(define-primop bytes->string/utf-8 (→fn ByteString String))
+(define-primop string->bytes/utf-8 (→fn String ByteString))
+(define-primop gensym (→fn Symbol Symbol))
+(define-primop symbol->string (→fn Symbol String))
+(define-primop string->symbol (→fn String Symbol))
 
 (define-typed-syntax (/ e1 e2) ≫
   [⊢ e1 ≫ e1- (⇐ : Int)]
@@ -96,17 +99,35 @@
   --------------------------------------------------
   [⊢ (#%app- ~a- e- ...) (⇒ : String)])
 
+(define-typed-syntax (~v e ...) ≫
+  [⊢ e ≫ e- (⇒ : τ)] ...
+  #:fail-unless (stx-andmap flat-type? #'(τ ...))
+  "expressions must be string-able"
+  --------------------------------------------------
+  [⊢ (#%app- ~v- e- ...) (⇒ : String)])
+
+(define-typed-syntax (format s e ...) ≫
+  [⊢ s ≫ s- (⇐ : String)]
+  [⊢ e ≫ e- (⇒ : τ)] ...
+  #:fail-unless (stx-andmap flat-type? #'(τ ...))
+  "expressions must be string-able"
+  --------------------------------------------------
+  [⊢ (#%app- format- s- e- ...) (⇒ : String)])
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Basic Values
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (define-typed-syntax #%datum
   [(_ . n:integer) ≫
+   #:with T (if (zero? (syntax-e #'n)) #'Zero #'NonZero)
   ----------------
-  [⊢ (#%datum- . n) (⇒ : Int)]]
-  [(_ . b:boolean) ≫
+  [⊢ (#%datum- . n) (⇒ : T)]]
+  [(_ . b:boolean)
+   ≫
+   #:with T (if (syntax-e #'b) #'True #'False)
   ----------------
-  [⊢ (#%datum- . b) (⇒ : Bool)]]
+  [⊢ (#%datum- . b) (⇒ : T)]]
   [(_ . s:string) ≫
   ----------------
   [⊢ (#%datum- . s) (⇒ : String)]])

racket/typed/syndicate/proto.rkt

@@ -13,6 +13,7 @@
 ;; Role Type Data Definitions
 
 ;; a FacetName is a symbol
+;; a Name is a Symbol
 
 ;; a T is one of
 ;;   - (Role FacetName (Listof EP)), also abbreviated as just Role
@@ -20,19 +21,24 @@
 ;;   - (Sends τ)
 ;;   - (Realizes τ)
 ;;   - (Stop FacetName Body)
+;;   - (WriteField Name τ)
 (struct Role (nm eps) #:prefab)
 (struct Spawn (ty) #:prefab)
 (struct Sends (ty) #:prefab)
 (struct Realizes (ty) #:prefab)
 (struct Stop (nm body) #:prefab)
+(struct WriteField (nm ty) #:prefab)
+(struct ReadField (nm) #:prefab)
 
 ;; a EP is one of
 ;;   - (Reacts D Body), describing an event handler
 ;;   - (Shares τ), describing an assertion
 ;;   - (Know τ), describing an internal assertion
+;;   - (Field Name τ), describing a field declaration
 (struct Reacts (evt body) #:prefab)
 (struct Shares (ty) #:prefab)
 (struct Know (ty) #:prefab)
+(struct Field (nm ty) #:prefab)
 
 ;; a Body describes actions carried out in response to some event, and
 ;; is one of
@@ -84,6 +90,8 @@
 ;;   - ⋆
 ;;   - (Base Symbol)
 ;;   - (internal-label Symbol τ)
+;;   - (VarTy Name (NEListof (List τ τ))), describing an assertion endpoint
+;;       whose type varies depending on the type of the named field
 (struct U (tys) #:prefab)
 (struct Struct (nm tys) #:prefab)
 (struct Observe (ty) #:prefab)
@@ -92,6 +100,7 @@
 (struct Hash (ty-k ty-v) #:prefab)
 (struct Mk⋆ () #:prefab)
 (struct internal-label (actor-id ty) #:prefab)
+(struct VarTy (nm tys) #:prefab)
 ;; TODO this might be a problem when used as a match pattern
 (define ⋆ (Mk⋆))
 (struct Base (name) #:prefab)
@@ -133,8 +142,8 @@
 ;; a TransitionEffect is one of
 ;;   - (send τ)
 ;;   - (realize τ)
-(struct send (ty) #:transparent)
-(struct realize (ty) #:transparent)
+(struct send (ty) #:prefab)
+(struct realize (ty) #:prefab)
 
 ;; a TransitionDesc is a (Hashof D+ (Setof (Listof RoleEffect)), describing the
 ;; possible ways an event (+/- of an assertion) can alter the facet tree.
@@ -204,13 +213,14 @@
            (values D txns)))
        (define assertions (assertions-in-state current assertion#))
        (define new-work
-         (for*/list ([txns (in-hash-values transitions)]
+         (for*/set ([txns (in-hash-values transitions)]
                      [txn (in-set txns)]
                      [st (in-value (transition-dest txn))]
-                     #:unless (equal? st current)
-                     #:unless (hash-has-key? states st))
+                     #:unless (or (equal? st current)
+                                  (hash-has-key? states st)
+                                  (member st more)))
            st))
-       (loop (append more new-work)
+       (loop (append more (set->list new-work))
              (hash-set states current (state current transitions assertions)))]
       ['()
        (role-graph (set (Role-nm role)) states)])))
@@ -377,6 +387,15 @@
           (set)
           (hash))))
 
+#|
+(define input (file->value "va2.rktd"))
+(define rg (compile input))
+(render-to-file rg "va2.dot")
+
+(define rgi (compile/internal-events rg))
+(render-to-file rgi "va2i.dot")
+|#
+
 ;; (Listof TraceStep) D StateName (DetectedCycle -> X) -> (U X Void)
 ;; the path is in reverse, and the final step is the pair evt/dest;
 ;; so their is a cycle if the sequence from the first occurrence of

racket/typed/syndicate/run-spin.sh

@@ -1,12 +1,21 @@
 #!/bin/sh
 
-pushd ${1%/*}/
+pushd ${1%/*}/ > /dev/null
 
 EXE="$1-verifier.o"
 
 spin -a $1
-gcc -o $EXE pan.c
-$EXE -a -f -n -N $2
-rm $EXE pan.c
+if [[ $? -ne 0 ]]; then
+    popd > /dev/null
+    exit 1
+fi
 
-popd
+gcc -o $EXE -D NFAIR=3 pan.c
+
+# -a to analyze, -f for (weak) fairness
+# -n to elide report of unreached states
+# -N spec-name to verify a particular specification
+$EXE -a -f -n -N $2
+rm $EXE pan.*
+
+popd > /dev/null

racket/typed/syndicate/spin-prelude.pml

@@ -2,8 +2,8 @@
 
 #define ASSERTED(x) (x##_assertions > 0)
 #define RETRACTED(x) (x##_assertions == 0)
-#define ASSERT(x) x##_assertions = x##_assertions + 1
-#define RETRACT(x) x##_assertions = x##_assertions - 1
+#define ASSERT(x) x##_update = x##_update + 1
+#define RETRACT(x) x##_update = x##_update - 1
 #define SEND(x) x##_messages = x##_messages + 1
 
 /* Rest of Program */

racket/typed/syndicate/sugar.rkt

@@ -0,0 +1,56 @@
+#lang turnstile
+
+(provide Observe★
+         RoleNTimes
+         (for-syntax RoleNTimes*))
+
+(require "core-types.rkt")
+(require turnstile/typedefs)
+
+(define-syntax (Observe★ stx)
+  (define star (type-eval #'★/t))
+  (syntax-parse stx
+    [(_ TyCons:id)
+     #:do [(define arity? (get-type-arity #'TyCons))]
+     #:when arity?
+     (mk-Observe- (list (reassemble-type #'TyCons (make-list (arity-min arity?) star))))]
+    [(_ t)
+     #:with (~Any/new TyCons τ ...) (type-eval #'t)
+     #:when (reassemblable? #'TyCons)
+     (mk-Observe- (list (reassemble-type #'TyCons (stx-map (lambda (_) star) #'(τ ...)))))]
+    [_
+     (raise-syntax-error #f "Not a type that can automatically be subscribed to" stx)]))
+
+(begin-for-syntax
+  ;; Arity -> Nat
+  (define (arity-min a)
+    (match a
+      [(arity-eq n) n]
+      [(arity-ge n) n])))
+
+(define-for-syntax (RoleNTimes* n Step behav)
+  (let loop ([i 1])
+  (define nm (format-id behav "step~a" i))
+  (quasisyntax/loc behav
+    (Role (#,nm)
+      #,@(if (= i 1)
+             (list #'(Shares Unit))
+             (list))
+      (Reacts #,(if (= i 1)
+                    #'(Asserted Unit)
+                    #`(Message #,Step))
+              #,@(if (= i n)
+                     (list)
+                     (list #`(Sends #,Step))))
+      (Reacts (Message #,Step)
+              (Effs #,behav
+                    (Stop #,nm
+                          #,@(if (< i n)
+                                 (if (= i 1)
+                                     (list #`(Sends #,Step) (loop (add1 i)))
+                                     (list (loop (add1 i))))
+                                 (list)))))))))
+
+(define-syntax-parser RoleNTimes
+  [(_ ~! n:nat Step:type behav:type)
+   (RoleNTimes* (syntax-e #'n) #'Step.norm #'behav.norm)])

racket/typed/tests/constructor-naming-conventions.rkt

@@ -0,0 +1,22 @@
+#lang typed/syndicate
+
+(require rackunit/turnstile)
+
+(define-constructor* (trust lvl))
+
+(check-type (trust 5) : (TrustT Int))
+
+(define-constructor* (hungry-hippos count appetite)
+  #:with HungryHippos (HungryHipposT Int String))
+
+(check-type (hungry-hippos 12 "massive") : HungryHippos)
+
+(define-constructor* (doggy [color : String] [weight : Int]))
+
+(check-type (doggy "black" 60) : (DoggyT String Int))
+(check-type (doggy "brown" 45) : Doggy)
+
+(define-constructor* (leaf))
+
+(check-type (leaf) : (LeafT))
+(check-type (leaf) : Leaf)

racket/typed/tests/effect-polymorhpism.rkt

@@ -2,16 +2,21 @@
 
 (require rackunit/turnstile)
 
-(define (∀ (ρ) (assert-something! [p : (proc → ★/t #:endpoints (ρ))]))
+(define (∀ (ρ) (assert-something! [p : (proc → ★/t #:effects (ρ))]))
   (p))
 
 (define (test-fun)
   (call/inst assert-something! (lambda () (assert 5))))
 
-
-(check-type test-fun : (proc → ★/t #:endpoints ((Shares Int))))
+(check-type test-fun : (proc → ★/t #:effects ((Shares NonZero))))
 
 (define (test-call/inst-insertion)
   (assert-something! (lambda () (assert 5))))
 
-(check-type test-call/inst-insertion : (proc → ★/t #:endpoints ((Shares Int))))
+(check-type test-call/inst-insertion : (proc → ★/t #:effects ((Shares NonZero))))
+
+(define (∀ (ρ) (start-something! [p : (proc → ★/t #:effects (ρ))]))
+  (p))
+
+(define (test-call-start-something)
+  (start-something! (lambda () (start-facet x (assert 5)))))

racket/typed/tests/endpoint-effects-branch.rkt

@@ -0,0 +1,7 @@
+#lang typed/syndicate
+
+(lambda ()
+  (start-facet x
+    (if #f
+        (assert (tuple 0))
+        (assert (tuple 1)))))

racket/typed/tests/for-loops.rkt

@@ -9,7 +9,7 @@
             : Int
             ⇒ 0)
 
-(check-type (for/fold ([x 0])
+(check-type (for/fold ([x : Int 0])
                       ([y (list 1 2 3)])
               y)
             : Int
@@ -20,13 +20,13 @@
 (define inventory0 (list (tuple "The Wind in the Willows" 5)
                            (tuple "Catch 22" 2)
                            (tuple "Candide" 33)))
-(check-type (for/fold ([stock 0])
+(check-type (for/fold ([stock : Int 0])
                       ([item inventory0])
               (select 1 item))
             : Int
             ⇒ 33)
 
-(check-type (for/fold ([stock 0])
+(check-type (for/fold ([stock : Int 0])
                       ([item inventory0])
               (if (equal? "Catch 22" (select 0 item))
                   (select 1 item)
@@ -36,7 +36,7 @@
 
 (define (lookup [title : String]
                 [inv : Inventory] -> Int)
-  (for/fold ([stock 0])
+  (for/fold ([stock : Int 0])
             ([item inv])
     (if (equal? title (select 0 item))
         (select 1 item)

racket/typed/tests/phantom-rho.rkt

@@ -18,4 +18,4 @@
     (on start (call/inst perform-task push-results))))
  : (List String)
  -> (list
-     "(Role (x) (Reacts OnStart (Role (perform) (Reacts OnStart (Stop perform (Branch (Effs (Role (done) (Shares Bool))) (Effs)))))))"))
+     "(Role (x) (Reacts OnStart (Role (perform) (Reacts OnStart (Stop perform (Branch (Effs (Role (done) (Shares True))) (Effs)))))))"))

racket/typed/tests/removing-annotations.rkt

@@ -0,0 +1,41 @@
+#lang typed/syndicate
+
+(require rackunit/turnstile)
+
+(define-constructor* (run [distance : Int] [windy? : Bool]))
+
+(check-type
+ (spawn
+  (start-facet runner
+    (assert (run 5 #t))))
+ : ★/t)
+
+(check-type
+ (spawn
+  (start-facet longer
+    (on (asserted (run $d $w?))
+        (printf "run ~a ~a\n" (add1 d) (if w? "brr" "")))))
+ : ★/t)
+
+(check-type
+ (dataspace
+  (spawn
+   (start-facet runner
+                (assert (run 5 #t))))
+  (spawn
+   (start-facet longer
+                (on (asserted (run $d $w?))
+                    (printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
+ : ★/t)
+
+(typecheck-fail
+ (dataspace
+  (spawn
+   (start-facet runner
+                ;; NB
+                (assert (run "FAR" #t))))
+  (spawn
+   (start-facet longer
+                (on (asserted (run $d $w?))
+                    (printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
+ #:verb-msg "unprepared to handle inputs: (RunT String True)")

racket/typed/tests/require-struct.rkt

@@ -0,0 +1,21 @@
+#lang typed/syndicate
+
+(require rackunit/turnstile)
+
+(require/typed "struct-provider.rkt"
+  [#:struct donkey [weight : Int] [grey? : Bool]])
+
+(check-type (donkey 5 #t)
+            : (DonkeyT Int Bool))
+
+(check-type (donkey 5 #t)
+            : Donkey)
+
+(check-type (donkey-grey? (donkey 5 #t))
+            : Bool)
+
+(require/typed "struct-provider.rkt"
+  [#:struct pot])
+
+(check-type (pot) : (PotT))
+(check-type (pot) : Pot)

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))

racket/typed/tests/spin/var-assert-basic.rkt

@@ -0,0 +1,38 @@
+#lang typed/syndicate
+
+(define (fut1)
+(lift+define-role va1
+(start-facet X
+  (field [state Bool #t])
+  (assert (tuple (! state))))))
+
+(module+ test
+  (verify-actors (Eventually (A (Tuple Bool)))
+                 va1)
+  )
+
+(define-constructor* (go-true))
+(define-constructor* (go-false))
+
+(define (fut2)
+  (lift+define-role va2
+  (export-roles "va2.rktd"
+  (print-role
+  (start-facet X
+    (field [state Bool #f])
+    (assert (tuple (! state)))
+    (on (message (go-true))
+        (:= state #t))))))
+
+  (lift+define-role gt
+  (start-facet Y
+    (on (asserted (tuple _))
+        (send! (go-true))))))
+
+(module+ test
+  (verify-actors (Eventually (A (Tuple True)))
+                 va2
+                 gt)
+  (verify-actors/fail (Always (Not (A (Tuple False))))
+    va2
+    gt))

racket/typed/tests/struct-provider.rkt

@@ -0,0 +1,9 @@
+#lang racket
+
+(struct donkey (weight stubborn?) #:transparent)
+
+(provide (struct-out donkey))
+
+(struct pot () #:transparent)
+
+(provide (struct-out pot))

racket/typed/tests/var-assert.rkt

@@ -0,0 +1,23 @@
+#lang typed/syndicate
+
+(require rackunit/turnstile)
+
+(check-type
+ (role-strings
+  (start-facet X
+    (field [state Bool #t])
+    (assert (tuple (! state)))))
+  : (List String)
+  -> (list "(Role (X) (VarAssert state (--> (U False True) (Tuple (U False True))) (--> False (Tuple False)) (--> True (Tuple True))) (MakesField state (U False True) True))"))
+
+(define (spawn-B)
+  (spawn
+   (start-facet B
+                (field [Bst Bool #t])
+                (assert (tuple (! Bst))))))
+
+(lambda ()
+  (lift+define-role rA
+  (start-facet A (on start (spawn-B))
+    (field [Ast Bool #t])
+    (assert (tuple (! Ast))))))