More work on unit test style simulation checking
This commit is contained in:
parent
8dda1ba6bf
commit
5a90933e9f
|
@ -115,7 +115,8 @@ JobManager and the TaskManager, and one between the TaskManager and its
|
|||
TaskRunners.
|
||||
|#
|
||||
|
||||
(define-type-alias TaskAssigner
|
||||
;; I think this is wrong by explicitly requiring that the facet stop in response
|
||||
(define-type-alias TaskAssigner-v1
|
||||
(Role (assign)
|
||||
(Shares (Observe (TaskPerformance ID ConcreteTask ★/t)))
|
||||
;; would be nice to say how the TaskIDs relate to each other
|
||||
|
@ -123,6 +124,14 @@ TaskRunners.
|
|||
(Branch (Stop assign)
|
||||
(Effs)))))
|
||||
|
||||
(define-type-alias TaskAssigner
|
||||
(Role (assign)
|
||||
;; would be nice to say how the TaskIDs relate to each other
|
||||
(Reacts (Asserted (TaskPerformance ID ConcreteTask TaskStateDesc))
|
||||
)))
|
||||
|
||||
(export-type "task-assigner.rktd" TaskAssigner)
|
||||
|
||||
(define-type-alias TaskPerformer
|
||||
(Role (listen)
|
||||
(During (Observe (TaskPerformance ID ConcreteTask ★/t))
|
||||
|
@ -195,8 +204,8 @@ The JobManager then performs the job and, when finished, asserts
|
|||
|
||||
(define (spawn-task-runner [id : ID] [tm-id : ID])
|
||||
(spawn τc
|
||||
(begin
|
||||
(start-facet runner
|
||||
(lift+define-role task-runner-impl
|
||||
(start-facet runner ;; #:includes-behavior TaskPerformer
|
||||
(assert (task-runner id))
|
||||
(on (retracted (task-manager tm-id _))
|
||||
(stop runner))
|
||||
|
@ -222,8 +231,8 @@ The JobManager then performs the job and, when finished, asserts
|
|||
(define (spawn-task-manager [num-task-runners : Int])
|
||||
(define id (gensym 'task-manager))
|
||||
(spawn τc
|
||||
(begin
|
||||
(start-facet tm
|
||||
(#;begin lift+define-role task-manager-impl ;;export-roles "task-manager-impl.rktd"
|
||||
(start-facet tm ;; #:includes-behavior TaskAssigner
|
||||
(log "Task Manager (TM) ~a is running" id)
|
||||
(during (job-manager-alive)
|
||||
(log "TM ~a learns about JM" id)
|
||||
|
@ -339,26 +348,6 @@ The JobManager then performs the job and, when finished, asserts
|
|||
(left t)]))))
|
||||
|
||||
|
||||
#;(define (partition-ready-tasks [tasks : (List Int)]
|
||||
-> (Tuple (List Int)
|
||||
(List Int)))
|
||||
(define part (inst partition/either Int Int Int))
|
||||
(part tasks
|
||||
(lambda ([t : Int])
|
||||
(right 0)
|
||||
#;(match (some 5)
|
||||
[(some $ct)
|
||||
(right ct)]
|
||||
[none
|
||||
(left 0)]))))
|
||||
|
||||
#;(define (debug [tasks : (List Int)] -> (Tuple (List String) (List Int)))
|
||||
(define part (inst partition/either Int String Int))
|
||||
(tuple (list) (list))
|
||||
(part tasks
|
||||
(lambda ([t : Int])
|
||||
(left "hi"))))
|
||||
|
||||
(define (input->pending-task [t : InputTask] -> PendingTask)
|
||||
(match t
|
||||
[(task $id (map-work $s))
|
||||
|
@ -380,8 +369,8 @@ The JobManager then performs the job and, when finished, asserts
|
|||
|
||||
(define (spawn-job-manager)
|
||||
(spawn τc
|
||||
(begin
|
||||
(start-facet jm
|
||||
(lift+define-role job-manager-impl ;; export-roles "job-manager-impl.rktd"
|
||||
(start-facet jm ;; #:includes-behavior TaskAssigner
|
||||
(assert (job-manager-alive))
|
||||
(log "Job Manager Up")
|
||||
|
||||
|
@ -522,7 +511,7 @@ The JobManager then performs the job and, when finished, asserts
|
|||
(on (realize (tasks-finished job-id $data:TaskResult))
|
||||
(stop delegate-tasks
|
||||
(start-facet done (assert (job-completion job-id tasks data)))))
|
||||
(on (realize (task-is-ready job-id $t))
|
||||
(on (realize (task-is-ready job-id $t:ConcreteTask))
|
||||
(perform-task t push-results)))
|
||||
(for ([t (in-list ready)])
|
||||
(add-ready-task! t))))))))
|
||||
|
@ -555,3 +544,11 @@ The JobManager then performs the job and, when finished, asserts
|
|||
(spawn-task-manager 3)
|
||||
(spawn-client (file->job "lorem.txt"))
|
||||
(spawn-client (string->job INPUT)))
|
||||
|
||||
(module+ test
|
||||
(check-simulates task-runner-impl task-runner-impl)
|
||||
(check-has-simulating-subgraph task-runner-impl TaskPerformer)
|
||||
(check-simulates task-manager-impl task-manager-impl)
|
||||
(check-has-simulating-subgraph task-manager-impl TaskPerformer)
|
||||
(check-has-simulating-subgraph task-manager-impl TaskAssigner)
|
||||
(check-has-simulating-subgraph job-manager-impl TaskAssigner))
|
||||
|
|
|
@ -74,7 +74,7 @@
|
|||
;; seller
|
||||
(spawn ds-type
|
||||
(lift+define-role seller-impl
|
||||
(start-facet _
|
||||
(start-facet _ ;; #:implements seller-role
|
||||
(field [book (Tuple String Int) (tuple "Catch 22" 22)]
|
||||
[next-order-id Int 10001483])
|
||||
(on (asserted (observe (quote (bind title String) discard)))
|
||||
|
|
|
@ -64,7 +64,7 @@
|
|||
;; DEBUG and utilities
|
||||
print-type print-role role-strings
|
||||
;; Behavioral Roles
|
||||
export-roles export-type check-simulates lift+define-role
|
||||
export-roles export-type check-simulates check-has-simulating-subgraph lift+define-role
|
||||
;; Extensions
|
||||
match cond
|
||||
submod for-syntax for-meta only-in except-in
|
||||
|
@ -93,7 +93,8 @@
|
|||
(require (postfix-in - racket/set))
|
||||
|
||||
(require (for-syntax (prefix-in proto: "proto.rkt")
|
||||
syntax/id-table))
|
||||
syntax/id-table)
|
||||
(prefix-in proto: "proto.rkt"))
|
||||
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
|
@ -748,7 +749,8 @@
|
|||
;; because turnstile introduces a lot of intdef scopes; ideally, we'd be able to synthesize somethign
|
||||
;; with the right module scopes
|
||||
#:with x+ (syntax-local-introduce (datum->syntax #f (syntax-e #'x)))
|
||||
#:do [(syntax-local-lift-module-end-declaration #`(define-type-alias x+ r))]
|
||||
#:do [(define r- (synd->proto #'r))
|
||||
(syntax-local-lift-module-end-declaration #`(define- x+ '#,r-))]
|
||||
----------------------------------------
|
||||
[⊢ e- (⇒ : τ) (⇒ ν-ep ()) (⇒ ν-f (r)) (⇒ ν-s ())])
|
||||
|
||||
|
@ -771,17 +773,32 @@
|
|||
(pretty-print ty-spec-))
|
||||
ans)
|
||||
|
||||
(define-syntax-parser check-simulates
|
||||
[(_ τ-impl:type τ-spec:type)
|
||||
(displayln 'CS)
|
||||
(define τ-impl- (synd->proto #'τ-impl.norm))
|
||||
(define τ-spec- (synd->proto #'τ-spec.norm))
|
||||
(unless (proto:simulates? τ-impl- τ-spec-)
|
||||
(pretty-print τ-impl-)
|
||||
(pretty-print τ-spec-)
|
||||
(raise-syntax-error #f "type doesn't simulate spec" this-syntax))
|
||||
#'(#%app- void-)])
|
||||
(define- (ensure-Role! r)
|
||||
(unless- (#%app- proto:Role? r)
|
||||
(#%app- error- 'check-simulates "expected a Role type, got " r))
|
||||
r)
|
||||
|
||||
(begin-for-syntax
|
||||
(define-syntax-class type-or-proto
|
||||
#:attributes (role)
|
||||
(pattern t:type #:attr role #`(quote- #,(synd->proto #'t.norm)))
|
||||
(pattern x:id #:attr role #'(#%app- ensure-Role! x))
|
||||
#;(pattern ((~literal quote-) r)
|
||||
#:do [(define r- (syntax-e ))]
|
||||
#:when (proto:Role? r-)
|
||||
#:attr role r-)))
|
||||
|
||||
(require rackunit)
|
||||
|
||||
(define-syntax-parser check-simulates
|
||||
[(_ τ-impl:type-or-proto τ-spec:type-or-proto)
|
||||
(syntax/loc this-syntax
|
||||
(check-true (#%app- proto:simulates? τ-impl.role τ-spec.role)))])
|
||||
|
||||
(define-syntax-parser check-has-simulating-subgraph
|
||||
[(_ τ-impl:type-or-proto τ-spec:type-or-proto)
|
||||
(syntax/loc this-syntax
|
||||
(check-not-false (#%app- proto:find-simulating-subgraph/report-error τ-impl.role τ-spec.role)))])
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Tests
|
||||
|
|
Loading…
Reference in New Issue