syndicate-lang
/
syndicate-2017
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

some handling of cycles in spin traces

This commit is contained in:
Sam Caldwell 2021-01-22 10:38:10 -05:00
parent bd267cfaa9
commit 04530893f4
2 changed files with 61 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
racket/typed/compile-spin.rkt
View File

@ -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)]
<<<<<START OF CYCLE>>>>>
|#
(define TRAIL-LINE-RX #px"(?m:^\\s*\\d+:\\s*proc\\s*(\\d+)\\s*\\(.*\\) \\S+\\.pml:(\\d+))")
(define TRAIL-LINE-RX #px"(?m:^ <<<<<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
@ -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"/\\*(.*)\\*/")

26
racket/typed/examples/roles/flink.rkt
View File

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