LoginSignup
2

More than 5 years have passed since last update.

SyncStitch:Train Gate Controll

Posted at

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

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
2