[SyncStitch]divergence

SyncStitchユーザガイドから。
divergenceを解決する例。

Definitions

(define-event in)
(define-event out)

(define-event send)
(define-event data)
(define-event err)

(define-event ack)
(define-event nak)

SENDER

(define-process SENDER (! in S1))
(define-process S1 (! send S2))
(define-process S2 (alt (! ack SENDER) (! nak S1)))

RECEIVER

(define-process RECEIVER (alt (! data R1) (! err R2)))
(define-process R1 (! ack R3))
(define-process R2 (! nak RECEIVER))
(define-process R3 (! out RECEIVER))

Retry回数を保持する変数の使い方。

MEDIUM

(define-process MEDIUM (M 3))

(define-process (M k)
  (! send
	 (if (= k 0)
		 (! data MEDIUM)
		 (ndc
		   (! data MEDIUM)
		   (! err (M (- k 1)))))))

SYSTEM

(define-process SYSTEM
  (hide (list send data err ack nak)
	(par (list send data err)
	  MEDIUM
	  (par (list ack nak)
		SENDER
		RECEIVER))))