task performer spec and task runner type

racket/typed/examples/roles/flink.rkt

@@ -112,6 +112,19 @@ JobManager and the TaskManager, and one between the TaskManager and its
 TaskRunners.
 |#
 
+(define-type-alias TaskAssigner
+  (Role (assign)
+    (Shares (TaskAssignment ID ID ConcreteTask))
+    ;; would be nice to say how the IDs relate to each other (first two are the same)
+    (Reacts (Know (TaskState ID ID ID ★/t))
+            (Branch (Stop assign)
+                    (Effs)))))
+
+(define-type-alias TaskPerformer
+  (Role (listen)
+    (During (TaskAssignment ID ID ConcreteTask)
+      (Shares (TaskState ID ID TaskID TaskStateDesc)))))
+
 #|
 Job Submission Protocol
 -----------------------
@@ -389,11 +402,11 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
 
          ;; ID -> ...
          (define (assign-task [mngr : ID])
-           (start-facet this-facet
+           (start-facet assign
             (assert (task-assignment mngr job-id t))
             (on (retracted (task-manager mngr discard))
                 ;; our task manager has crashed
-                (stop this-facet
+                (stop assign
                       (set! task-mngr not-a-real-task-manager)))
             (on start
                 ;; N.B. when this line was here, and not after `(when mngr ...)` above,
@@ -413,14 +426,14 @@ The JobManager then performs the job and, when finished, asserts (job-finished I
                    ;; don't think we need a release-slot! here, because if we've heard back from a task manager,
                    ;; they should have told us a different slot count since we tried to give them work
                    (log "JM overloaded manager ~a with task ~a" mngr this-id)
-                   (stop this-facet
+                   (stop assign
                          (set! task-mngr not-a-real-task-manager))]
                   [(finished $results)
                    (log "JM receives the results of task ~a" this-id)
                    (stop perform (k this-id results))]))))
 
            (define (select-a-task-manager)
-             (start-facet this-facet
+             (start-facet select
               (begin/dataflow
                 (when (equal? (ref task-mngr) not-a-real-task-manager)
                   (define mngr?

racket/typed/proto.rkt

@@ -1041,11 +1041,7 @@
            (esc #f))
          (define assertions1 (hash-ref assertion#1 sn1))
          (define assertions2 (hash-ref assertion#2 sn2))
-         (define superset?
+         (unless (assertion-superset? assertions1 assertions2)
-           (for/and ([assertion2 (in-set assertions2)])
-             (for/or ([assertion1 (in-set assertions1)])
-               (<:? assertion1 assertion2))))
-         (unless superset?
            (return #f))
          (define transitions1 (state-transitions (hash-ref st#1 sn1)))
          (define transitions2 (state-transitions (hash-ref st#2 sn2)))
@@ -1085,7 +1081,7 @@
            (for/and ([goal (in-set matching)])
              (define hypotheses (set-remove matching goal))
              (verify goal (set-union hypotheses assumptions))))])))
-    (verify (equiv st0-1 st0-2) (set)))
+  (verify (equiv st0-1 st0-2) (set)))
 
 ;; (Sequenceof StateName) Role -> (Hashof StateName (Setof τ))
 ;; map each state name to its active assertions
@@ -1105,6 +1101,13 @@
     (values (Role-nm role)
             (role-assertions role))))
 
+;; (Setof τ) (Setof τ) -> Bool
+;; is as1 a superset of as2?
+(define (assertion-superset? as1 as2)
+  (for/and ([assertion2 (in-set as2)])
+    (for/or ([assertion1 (in-set as1)])
+      (<:? assertion2 assertion1))))
+
 (module+ test
   (test-case
       "simplest simul"
@@ -1350,16 +1353,18 @@
                                        (Branch (Effs (Stop get-quotes)) (Effs)))))))
   (test-case
       "parsed types are (not) the same as my manual conversions"
-    ;; because I parse (Bind τ) as ⋆, whereas my manual conversions use τ
+    ;; because I parse (Bind τ) as ⋆, whereas my manual conversions use τ thus
-    (check-false (simulates? (parse-T real-seller-ty) seller-actual))
+    ;; the "real" types are more specialized and implement the manual
+    ;; conversions, but not vice versa
+    (check-true (simulates? (parse-T real-seller-ty) seller-actual))
     (check-false (simulates? seller-actual (parse-T real-seller-ty)))
 
-    (check-false (simulates? (parse-T real-member-ty) member-actual))
+    (check-true (simulates? (parse-T real-member-ty) member-actual))
     (check-false (simulates? member-actual (parse-T real-member-ty)))
 
-    (check-false (simulates? (parse-T real-leader-ty) leader-actual))
+    (check-true (simulates? (parse-T real-leader-ty) leader-actual))
     (check-false (simulates? leader-actual (parse-T real-leader-ty)))
-    (check-false (simulates? (parse-T real-leader-ty) leader-revised))
+    (check-true (simulates? (parse-T real-leader-ty) leader-revised))
     (check-false (simulates? leader-revised (parse-T real-leader-ty)))))
 
 (define real-seller-ty
@@ -1501,3 +1506,80 @@
     (define jm (compile jmr))
     (check-true (role-graph? jm))
     (check-true (simulates? jmr jmr))))
+
+(define task-performer-spec
+  '(Role
+    (listen)
+    (Reacts
+     (Know
+      (TaskAssignment
+       Symbol
+       Symbol
+       (Task
+        Int
+        (U
+         (MapWork String)
+         (ReduceWork (Hash String Int) (Hash String Int))))))
+     (Role
+      (during-inner)
+      (Reacts
+       (¬Know
+        (TaskAssignment
+         Symbol
+         Symbol
+         (Task
+          Int
+          (U
+           (MapWork String)
+           (ReduceWork (Hash String Int) (Hash String Int))))))
+       (Stop during-inner))
+      (Shares
+       (TaskState
+        Symbol
+        Symbol
+        Int
+        (U (Finished (Hash String Int)) Symbol)))))))
+
+(module+ test
+  (test-case "parse and compile task-performer-spec"
+    (check-true (Role? (parse-T task-performer-spec)))
+    (check-true (role-graph? (compile (parse-T task-performer-spec))))))
+
+(define task-runner-ty
+  '(Role
+    (runner)
+    (Shares (TaskRunner Symbol (U (Executing Int) Symbol)))
+    (Reacts
+     (Know
+      (TaskAssignment
+       Symbol
+       (Bind Symbol)
+       (Task
+        (Bind Int)
+        (Bind
+         (U
+          (MapWork String)
+          (ReduceWork (Hash String Int) (Hash String Int)))))))
+     (Role
+      (during-inner)
+      (Shares
+       (TaskState Symbol Symbol Int (U (Finished (Hash String Int)) Symbol)))
+      (Reacts
+       (¬Know
+        (TaskAssignment
+         Symbol
+         Symbol
+         (Task
+          Int
+          (U
+           (MapWork String)
+           (ReduceWork (Hash String Int) (Hash String Int))))))
+       (Stop during-inner))))
+    (Reacts OnDataflow)))
+
+(module+ test
+  (test-case "parse and compile task-runner-ty"
+    (check-true (Role? (parse-T task-runner-ty)))
+    (check-true (role-graph? (compile (parse-T task-runner-ty))))
+    (check-true (simulates? (parse-T task-runner-ty)
+                            (parse-T task-performer-spec)))))