Think Stitch
PRINCIPIA  最近の更新


プロセスの逐次合成

逐次合成は指定された複数のプロセスを順番に実行するプロセスを表します。逐次合成は seq 式で表すことができます。seq の書式は次のとおりです。

(seq process-expr ...)

引数としてプロセスを実行する順番に並べます。

(seq P Q R) は次のような動作を表します。まずプロセス P のように動作します。P が終了したらプロセス Q に移行し Q のように動作します。プロセス Q が終了したら プロセス R に移行し R のように動作します。プロセス R が終了したら (seq P Q R) が終了したことになります。

  • (seq P Q R) は P が終了したら (seq Q R) に移行するということができます。
  • もしプロセス P が終了しないで停止する場合は (seq P Q R) も停止します。プロセス Q, R は実行されません。
  • (seq P) は単に P と書いたのと同じです。
  • (seq) は SKIP と同じです。

逐次合成の例

プロセス定義

プロセス P と Q を逐次合成したプロセス S を定義します。

(define-process S
  (seq P Q))

(define-process P
  (alt (! a SKIP) (! b STOP)))

(define-process Q
  (! c SKIP))

計算木

  • まずプロセス P を実行します。イベント a が発生した場合は SKIP で終了します。このときプロセス P の終了を表す終了イベント tick は内部イベント tau に変わります。プロセス P から Q への移行は逐次合成されたプロセス S の内部で行われるということです。もし tick が見えてしまうと S が終了することになってしまうからです。
  • イベント b が発生した場合、プロセス P は停止します。この場合、プロセス Q は実行されません。
  • プロセス Q はイベント c を発生させた後、終了します。プロセス Q は seq 式の最後のプロセスなので、プロセス S も終了します。
2013/07/29
© 2013,2014,2015 PRINCIPIA Limited