[SyncStitch]an example of divergence.

traceは等価((trace SPEC SYS))だが、
発散する((divergence SYS)が失敗する)例。

Definitions

(define-event ok)
(define-event ng)

(define-event ping)

(define-channel rch (x) '((ping)))
(define-channel sch (x) '((ok) (ng)))
(define-channel cch (x) '((ok)))

SPEC

(define-process SPEC (! ping (! ok SPEC)))

Sender

(define-process Sender
	(! ping (! rch ('ping) Try)))

(define-process Try
  (? sch (x)
	 (if (eqv? x 'ok)
		 (! ok Sender)
		 Try)))

Receiver

(define-process Receiver
  (? rch (x) (! cch ('ok) Receiver)))

RandomChannel

(define-process RandomChannel
  (? cch (x) (ndc ReplyOK ReplyNG)))

(define-process ReplyOK (! sch ('ok) RandomChannel))
(define-process ReplyNG (! sch ('ng) RandomChannel))

SYS

(define-process SYS
  (hide
	  (list rch sch cch)
	  (par '() Sender Receiver RandomChannel)))