diff --git a/racket/typed/compile-spin.rkt b/racket/typed/compile-spin.rkt index 4b8ad6d..fd4d139 100644 --- a/racket/typed/compile-spin.rkt +++ b/racket/typed/compile-spin.rkt @@ -427,16 +427,17 @@ (indent) (displayln "}")] [(sstate name branches) (indent) (printf ":: ~a == ~a ->\n" (svar-name CURRENT-STATE) name) - (with-indent - (indent) (displayln "if") - (with-indent - (cond - [(empty? branches) - (indent) (displayln ":: true -> skip;")] - [else + (cond + [(empty? branches) + ;; no transitions out of this state + (indent) (displayln "end: false;")] + [else + (with-indent + (indent) (displayln "if") + (with-indent (for ([branch branches]) - (gen-spin-form branch name-env))])) - (indent) (displayln "fi;"))] + (gen-spin-form branch name-env))) + (indent) (displayln "fi;"))])] [(sbranch event dest actions) (indent) (printf ":: ~a -> ~a\n" (predicate-for event) (embed-event-as-comment event name-env)) (with-indent @@ -640,10 +641,11 @@ (zero? num-errors)) #| -Example: +Examples: 4: proc 2 (proc824:1) model.pml:140 (state 2) [ClubMemberT_String_assertions = (ClubMemberT_String_assertions+1)] + <<<<>>>> |# -(define TRAIL-LINE-RX #px"(?m:^\\s*\\d+:\\s*proc\\s*(\\d+)\\s*\\(.*\\) \\S+\\.pml:(\\d+))") +(define TRAIL-LINE-RX #px"(?m:^ <<<<>>>>|^\\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 @@ -658,8 +660,11 @@ Example: ;; a PID is a Nat -;; a TraceStep is a (trace-step PID TraceEvent) +;; a TraceStep is one of +;; - (trace-step PID TraceEvent) +;; - 'start-of-cycle (struct trace-step (pid evt) #:prefab) +(define START-OF-CYCLE 'start-of-cycle) ;; a TraceEvent is one of ;; - (assert τ) @@ -671,26 +676,33 @@ Example: (define (interpret-spin-trace pid/line-trace model-lines) (define maybe-steps (for/list ([item (in-list pid/line-trace)]) - (match-define (list pid-str line-no-str) item) - (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)))) + (match item + ['(#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))] + ))) (filter values maybe-steps)) ;; (Listof TraceStep) -> Void (define (print-trace trace) (for ([ts (in-list trace)]) - (match-define (trace-step pid evt) ts) - (match evt - [(assert ty) - (printf "Process ~a ASSERTS ~a\n" pid (τ->string ty))] - [(retract ty) - (printf "Process ~a RETRACTS ~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))]))) + (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 + [(assert ty) + (printf "Process ~a ASSERTS ~a\n" pid (τ->string ty))] + [(retract ty) + (printf "Process ~a RETRACTS ~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))])]))) (define COMMENT-RX #px"/\\*(.*)\\*/") diff --git a/racket/typed/examples/roles/flink.rkt b/racket/typed/examples/roles/flink.rkt index 2af2b02..ff0456e 100644 --- a/racket/typed/examples/roles/flink.rkt +++ b/racket/typed/examples/roles/flink.rkt @@ -204,6 +204,7 @@ The JobManager then performs the job and, when finished, asserts (define (spawn-task-runner [id : ID] [tm-id : ID]) (spawn τc + (export-roles "task-runner-impl.rktd" (lift+define-role task-runner-impl (start-facet runner ;; #:includes-behavior TaskPerformer (assert (task-runner id)) @@ -222,7 +223,7 @@ The JobManager then performs the job and, when finished, asserts (set! state (finished wc))] [(reduce-work $left $right) (define wc (hash-union/combine left right +)) - (set! state (finished wc))])))))) + (set! state (finished wc))]))))))) ;; --------------------------------------------------------------------------------------------------- ;; TaskManager @@ -231,7 +232,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 lift+define-role task-manager-impl ;;export-roles "task-manager-impl.rktd" + (export-roles "task-manager-impl.rktd" + (#;begin lift+define-role task-manager-impl (start-facet tm ;; #:includes-behavior TaskAssigner (log "Task Manager (TM) ~a is running" id) (during (job-manager-alive) @@ -293,7 +295,7 @@ The JobManager then performs the job and, when finished, asserts [OVERLOAD/ts (set! status OVERLOAD/ts)] [(finished discard) - (set! status st)]))))))))) + (set! status st)])))))))))) ;; --------------------------------------------------------------------------------------------------- ;; JobManager @@ -522,10 +524,12 @@ The JobManager then performs the job and, when finished, asserts ;; Job -> Void (define (spawn-client [j : JobDesc]) (spawn τc + (export-roles "client-impl.rktd" + (lift+define-role client-impl (start-facet _ (match-define (job $id $tasks) j) (on (asserted (job-completion id tasks $data)) - (printf "job done!\n~a\n" data))))) + (printf "job done!\n~a\n" data))))))) ;; --------------------------------------------------------------------------------------------------- ;; Main @@ -545,6 +549,20 @@ The JobManager then performs the job and, when finished, asserts (spawn-client (file->job "lorem.txt")) (spawn-client (string->job INPUT))) +(module+ test + (verify-actors (Eventually (A (JobCompletion ID (List InputTask) TaskResult))) + #;(Always (Implies (A (Observe (JobCompletion ID (List InputTask) ★/t))) + (Eventually (A (JobCompletion ID (List InputTask) TaskResult))))) + job-manager-impl + task-manager-impl + client-impl) + + (verify-actors (And (Always (Implies (A (Observe (TaskPerformance ID ConcreteTask ★/t))) + (Eventually (A (TaskPerformance ID ConcreteTask TaskStateDesc))))) + (Eventually (A (TaskPerformance ID ConcreteTask TaskStateDesc)))) + TaskAssigner + TaskPerformer)) + (module+ test (check-simulates task-runner-impl task-runner-impl) (check-has-simulating-subgraph task-runner-impl TaskPerformer)