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