Think Stitch
PRINCIPIA  最近の更新


制約プロセス: 並行合成で制約条件を表す

下図のようなプロセスが欲しいとしましょう。(もう描いてありますけど。)

並行合成によるインターリーブ

欲しい状態遷移図は、以下の状態遷移図から右上、左下の状態を取り除いたものになっています。 そこでまず、この格子状のプロセス PL を作ることにします。(もう猫いてありますけど。)

プロセス PLは、イベント a が3回、イベント b が2回、任意の順序で発生するものになっています。 そこで、イベント a だけ、イベント b だけを発生させるプロセス PA, PB をそれぞれ作ります。

イベント a を3回だけ発生させるプロセス PA

イベント b を2回だけ発生させるプロセス PB

この2つを合わせれば PL になります。 どのようにあわせるかというと、インターリーブです。 2つのプロセスは相互作用をせず、それぞれの発生させるイベントが任意の順序で発生できるからです。 これは並行合成 par で、同期リストを空にすれば実現できます。

(define-process PAB
  (par '() PA0 PB0))

結果は次のようになります。確かに PL と同じになりました。

制約プロセス

次に2つの角を落とすことを考えましょう。 どうやって落とすかというと、格子状のプロセス PAB を外から監視するプロセスを作って、初期状態からイベント a が2回連続で発生したら、3回目の a の発生を禁止するのです。 同様に初期状態からイベント b が発生したら、次の b を禁止します。 このように制約条件を表すプロセスを制約プロセスと呼ぶことにします。

いまの場合、制約プロセスは次のように作ることができます。

  • 初期状態からイベント a が2回連続発生した後は、イベント b しか発生しない。
  • 初期状態からイベント b が1回発生した後は、イベント a しか発生しない。
  • それ以外の場合は、イベント a, b のどちらが発生してもよい。

制約プロセス Q は次のようになります。

初期状態 Q から監視を始めて、イベント a が2回連続発生すると状態 Q2 に来ます。 そこでイベント b の遷移だけを用意することで、イベント a の発生を禁止します。 同様に状態 Q3 はイベント b の発生後なので、イベント a の遷移だけを持たせます。 状態 Q4 はどちらが発生してもよい状態、制約のない状態です。 状態 Q1 ではイベント b が発生可能なので、イベント b の遷移が必要です。

格子状のプロセス PAB と制約プロセス Q を並行合成します。 制約プロセスは相互作用によって監視と制約を行うのですから、同期リストにはすべてのイベントのリストを指定します。 いまの場合は (list a b) です。

(define-process PABQ
  (par (list a b) PAB Q))

結果は次のようになります。欲しいものが手に入りました。

モデル化の道具としての並行合成

並行合成については SyncStitch ユーザガイドと、プロセスの動的生成で、次の2つの役割があることを見てきました。

  • コンポーネントの動作を表すプロセスを合成して、システムの動作を表すプロセスを構築するための演算子
  • プロセスの実行時に、子プロセスを動的に生成するためのプリミティブ

さらに加えて、上で見てきたように並行合成はモデルを作成するための道具として使用することができます。 大まかいうと2つの使い方ができます。1つはインターリーブ、もう1つは制約です。 この2つはいつでも明確に区別できるわけではなく、同期リストによっては両方の意味を持つ場合もあります。

複雑で規模の大きなシステムをコンポーネントに分割すると実現やメンテナンスが容易になり、さらに再利用が可能になるとの同じように、複雑で規模の大きな動作仕様を作成する際にも、部分に分けて記述するという方法は有効です。 このとき、2つの機能を「合わせる」とか、「同時に動かす」とか、あるいは「これが動いているときには禁止される」といった、コンポーネントの設計とは異なる合成の仕方が必要になります。 並行合成はこのような用途にも使うことができるということです。

補足

  • より一般的には「イベント b しか発生しない」の部分は、「イベント a 以外のイベントのみ発生できる」とします。 同様に「イベント a, b のどちらが発生してもよい。」の部分も「何が発生してもよい」ということです。 これらはアルファベット定数・関数を使うとより一般的に定義することができます。 アルファベット定数・関数については SyncStitch リファレンスマニュアルを見てください。
  • 並行合成を制約として使うことができるのは、相互作用が同期型だからです。同期型の相互作用自体が、監視(観測)と制約(同期)を表しているからです。 そういう意味では、実装で制約プロセスを使うこともできます。 しかし制約プロセスなしにできるのであれば、その方が効率はよいでしょう。
  • 仕様を論理式(事前・事後条件や時相論理など)で書くと what に集中でき、容易に書けますが動きません。関数や命令手順で書くと how を書かなければなりませんが動きます。 制約プロセスは AND 条件のようなものなので、やや論理側に近い。表現に便利でしかも動くんですけど、効率は悪いということです。 設計って、動かない表現を動くように、動くけど効率が恐ろしく悪いものを実用的なレベルに変換していく、というイメージです。
  • 制約プロセスや特徴プロセス(ユーザガイド参照)は制約条件や特徴を表すオートマトンです。 正規言語に対するオートマトンに関係が似ています。 時相論理の論理式と、それを追跡するオートマトンとも似ていますね(LTL の場合。すみません、子供みたいに背伸びしました。ほんとは LTL のことはあまり知りません)。
  • [この項目はもっと検討が必要です:] システムを構成する要素をコンポーネントと呼ぶのに対して、仕様の部分を表す一般的な言葉はないようなので、ここでは部分仕様と呼ぶことにします。 システムをコンポーネントに分割する際の切り方と、仕様を部分仕様に分ける場合の切り方は少し違うような気がします。 まず仕様の場合は分けるというより、もともと分かれているものを合わせるという方が近いような気がします(もちろんシステムでもそういうことはありますが)。 最初は機能、ユースケースやシナリオなどの断片から考え始めるからです。 システムの作りと比較すると、(これもあくまでイメージですが)コンポーネントはどちらかというと水平に切られているのに対し、仕様は垂直に切られているような気がします。 システムはよくレイヤーに(つまり水平に)切られるのに対して、シナリオの1つ1つはレイヤーを縦に串刺しにして走るでしょう。 すると、仕様から設計への変換というのは、切り方の軸を変換しているということができるかもしれません(単なる言葉遊びかもしれませんが)。 これをもっと明確な設計手法に昇華させることはできないでしょうか。
  • たわごとついでにもう1つ。結論のある話ではありません。 機能的にはほとんど独立していて、垂直分割で作られた複数のアプリケーションからなるシステムで、突然アプリケーション間連携なんて話が出ることがあります(ありませんか?)。 経験上、こういうのは大騒ぎになることが多かったように思います。あっちに穴を空け、こっちを修正し、渡すものにあれを加えて・・・なんてカオスになるうえに、結局整合性を保つことができず(それも動かしてから気がつくんですが)、諦めたり最小限の仕様になっちゃって、当初のアイデアの魅力なんてぜんぜんなかったりして。こういうのはどうしてこうなるのか、なんとかする一般的な考え方はないか、なんて考えてしまうのですが、ことが済むとすぐ忘れてしまうので、ものになんかならないのですけどね。
2013/08/18
© 2013,2014,2015 PRINCIPIA Limited