[SyncStitch]an example of deadlock

本日はTopSEセミナーにて、PATツールを使ってCSPを勉強しています。
ということで、PATのCSPモデルをSyncStitchのモデルにコンバート。

deadlock.ss

; Definitions
(define-event setorange)
(define-event setlemon)
(define-event orange)
(define-event lemon)
(define-event tomato)

;DrinkDispenser
(define-process DD
  (alt
    (! setorange O)
    (! setlemon L)))

(define-process O
  (alt
    (! orange O)
    (! setlemon L)
    (! setorange O)
    (! tomato STOP)))

(define-process L
  (alt 
    (! lemon L)
    (! setorange O)
    (! setlemon L)))