SyncStitchを勉強中。
CSP(Communicating Sequential Processes)を論理基盤に持つ、
並行プロセス検証ツール。
Schemeで書けて、軽快に動作する。
以下は、作りかけの電車の遮断機制御プロセス。
遮断機の前後に、電車進入検知器がある、という想定。
このモデルは無条件で全部のプロセスを合成しているため、
ありえない遷移が発生する。
Definitions
(define-event f.enter)
(define-event f.exit)
(define-event b.enter)
(define-event b.exit)
(define-event c.open)
(define-event c.close)
SYS
(define-channel ch-fc (x) '((0)))
(define-channel ch-bc (x) '((0)))
(define-channel ch-cg (x) '((0) (1)))
(define-process SYS
(par '() FRONT BACK CTRL-CLOSE))
(define-process FRONT
(! f.enter (! ch-fc (0) (! f.exit FRONT))))
(define-process BACK
(! b.enter (! b.exit (! ch-bc (0) BACK))))
(define-process CTRL-CLOSE
(? ch-fc (x) (! c.open
(? ch-bc (x) (! c.close CTRL-CLOSE)))))