[SyncStitch]仕様と実装の比較

masaterukの日記
より。

こんな感じですかね。

Definitions

(define-event send.0)
(define-event send.1)
(define-event recv.0)
(define-event recv.1)

(define-channel rch (x) '((0) (1)))
(define-channel sch (x) '((0) (1)))

SPEC

(define-process SPEC
  (! send.0 (! recv.0 (! send.1 (! recv.1 SPEC)))))

Sender

(define-process S0
  (! send.0
     (! rch (0)
        (? sch (x) (= x 0)
           (! send.1
              (! rch (1)
                 (? sch (x) (= x 1) S0)))))))

Receiver

(define-process R0
  (? rch (x) (= x 0)
     (! recv.0
        (! sch (0)
           (? rch (x) (= x 1)
              (! recv.1
                 (! sch (1) R0)))))))

SYS

(define-process SYS
  (hpar (list sch rch) S0 R0))

Assertions

(deadlock SYS)
(trace SPEC SYS)
(failure SPEC SYS)