Think Stitch
PRINCIPIA  最近の更新


改名による抽象化

設計をするとき、最初は大まかに考えますよね。 振る舞いの側面を考えるときには、例えばイベントを使って大まかな動きを状態遷移図としてスケッチします。 いくつか案があったり、書いているうちに他の可能性に気づいたりしますから、何枚かは描くことになりますし、捨てたりやり直したりすることもありますから、最初からあまり細かいことを気にするのは効率がよくありません。

いくつかスケッチを描いて方針が決まったら、次にもう少し詳細なモデルを作るでしょう。 ここでちょっと困るのは、最初に描いた(そして選んだ)スケッチと、その後に作ったより詳細なモデルでは記述の詳細度(抽象度)が異なるので、直接比較することができないことです。 この2つの間には大まかには正当性関係があるはずですから、比較検査をしたいところです。

一口に詳細にするといってもいろいろあります。 ここでは抽象的なイベントで描かれたスケッチから、チャネルやガード、状態変数などを使ったモデルに進んだ場合を考えます。 このような場合に、抽象的なスケッチと詳細なモデルを比較できるようにする方法をご紹介します。 改名を使う方法です。

例として次のようなプロセスを考えます。 基本的には受け取ったデータを元に何か計算をして、結果を返すプロセスです。 このプロセスは2つのモードを持っていて、1つはただ結果を返すのですが、もう1つのモードでは、処理のレポートを別のチャネルを通じて出力するものとします。 問題を簡単にするために、モードの設定は起動時に1度だけ行えるものとします。

遷移はすべてイベント同期にしてあります。 処理の大まかな流れだけに注目していて、受信したデータや送信する結果、およびレポートの内容はとりあえず無視しているということです。

大まかな動作を決めたら、次に詳細なモデルを作ります。 まず送受信およびレポート出力をチャネルに代えます。 さらに、モード設定もチャネル受信にしました。 モードは状態変数に格納して覚えておくことにして、抽象スケッチと異なり、ガードを使って場合分けを行うことにします。 送信する結果とレポートの内容については、この例では受信した値をそのまま送ることにします。例なので勘弁してください。

計算木は次のようになります。 スケッチのように、モードによってレポートの有無が切り替えられていることが確認できます。

改名を使ってプロセスを抽象化する

残念ながらこのままでは詳細なモデル IMP がスケッチ SPEC を満たしているかどうか検査することができません。 アルファベットが異なるからです。 設計者である我々はイベントとチャネルの対応関係を知っていますから、図を見たときに頭の中で変換して確認することができます。 であれば、この対応関係をデータとして表現して、プログラムで変換すれば比較ができるはずです。 実際、これは改名を使って実行できます。

次のように、詳細モデルで使われているチャネルを、スケッチで使われている対応するイベントに改名します。 モード設定では、チャネルイベントを使って、引数ごとに異なるイベントに改名します。 チャネルからイベントへの改名は多対一の変換です。 チャネル引数の違いを無視する、あるいは捨てていることになるので、抽象化をしているということです。 別のいい方をすると、改名を使って詳細モデルの抽象度をスケッチに合わせているということです。

(define-process IMP-ABS
  (rename `((,($ ch-mode 0) . ,mode0)
            (,($ ch-mode 1) . ,mode1)
            (,ch-in . ,in)
            (,ch-out . ,out)
            (,ch-report . ,report))
    P0))

このように改名を使って抽象化を行えば、スケッチとの比較が可能になります。 実際に正当性を検査してみると、以下のようにスケッチで決めた振る舞いを満たしていることが検査できます。

(ささやかな成果ですが、このモデルを作っているとき、モードの 0, 1 を間違えていて、実際に検査で発見しました。 この段階ならば30秒で直せますけど、こんなものでも開発の終盤であればテストのやり直しやらマスターの作り直しやらで大騒ぎでしょう。 リリースコストの異なる分野では違う感覚かもしれませんが。)

抽象化したプロセスを探査する

改名によって抽象化したモデルを探査してみましょう。 計算木は次のようになります。 改名は計算木のラベルを単に置き換えるのと同じことなので、チャネル引数の分だけ同じ遷移が出ています。 環境ウィンドウで状態変数の値を覗いてみると、抽象化をする前の値を見ることができます。

状態変数の値が異なるので、これらは異なる状態だと考えられるかもしれません。 しかし思い出していただきたいのは、プロセスの振る舞いというのは相互作用を通じて観測できるものだけで決まるということです。 重複して現れている3つの流れはどれも同じイベントの列を持っています。 したがって外部からはこれらを区別することはできません。

実際、このプロセスをプロセスエクスプローラのトレースモードで見てみると、3つの流れは区別されないことがわかります。 トレースモードで探査するには、プロセス STOP との正当性比較を行います。(比較を故意に失敗させます。)

3つの状態が1つにまとめられていることがわかります。

ガードがある場合

もう1つ別の例を見てみましょう。 今度の例では、チャネル c から受信した値を見て、ガードによって場合分けを行っています。 受信した値が 0 だった場合はイベント e を発生させます。 そうでなければ、受信した値から何か計算を行って、結果をチャネル d から出力します。 (ここでは簡単に -1 しました。)

計算木は次のとおりです。

先ほどと同じように、各チャネル c, d をイベント ca, da に改名することでプロセスを抽象化します。

(define-process P-ABS
  (rename `((,c . ,ca) (,d . ,da)) P0))

抽象化されたプロセスの計算木は次のとおりです。

今回は、先ほどと異なり、同じイベント ca が発生した後に異なる振る舞いがあります。 つまり非決定性があるということです。 これをトレースモードを使って確認します。

イベント ca が発生した後の状態グループには極小受理が2つあるので、非決定性があることがわかります。

実際、抽象化されたプロセスは、次の典型的な非決定的プロセスと同じプロセスになります。

このように、改名によってプロセスを抽象化すると非決定性が現れることがあります。 この例のように、チャネル引数の値によって場合分けを行っていると非決定性が現れます。 その理由は、抽象化によって引数の情報が失われるので、ガードが成立するかどうかがわからなくなるためです。 場合分けが非決定的選択になってしまうのですから、この抽象化されたプロセスを許容する仕様は、規定としてはかなり弱いということになります。

逆に、改名による抽象化の結果、非決定性が現れないということは、プロセスはチャネル引数の値に依存していないということです。 例えば、いままでにバッファやキュー、スタックなどの例が出てきましたが、これらは抽象化を行っても非決定性は現れません。 受信したデータをそのまま保持し、後で出力するだけで、内容については関知していないからです。 つまり、改名によって抽象化することで、データに対する独立性がわかるということです。

抽象化を細かく制御する

場合分けが非決定的選択になってしまうのは規定として弱すぎるので、スケッチの段階では異なるイベントで場合分けを表している、ということがあるでしょう。 このような場合、やや面倒ではありますが、チャネルの引数、あるいはチャネルに属するチャネルイベントを、場合分けの条件によってグループ分けして、それぞれのグループをスケッチで使用しているイベントに改名すれば、比較ができるようになります。

上の例でいうと、引数 0 の場合とそれ以外に分けて、それぞれイベント ca0 と ca に改名します。 (この2つのイベントがスケッチで使われているとします。)

(define-process P-ABS2
  (rename `((,($ c 0) . ,ca0)
            (,($ c 1) . ,ca)
            (,($ c 2) . ,ca)
            (,($ c 3) . ,ca)
            (,d . ,da))
    P0))

計算木は次のようになります。

今度は非決定性は生じません。トレースモードで確認すると次のようになります。

チャネルイベントの関数を利用する

改名による抽象化については以上ですが、話のついでにチャネルイベントの扱いについて補足します。

上の改名マップの部分はあまり格好のいいものではありません。 チャネル c の引数が直接使われているので、定義域が変わったら合わせて修正しなければなりません。 加えて、場合分けの条件が状態遷移図と改名と2カ所に現れるので、それもよくありません。 チャネルイベントに関する関数を使うと、この問題を少し緩和できます。

まず場合分けの条件を表す述語関数 g? を定義しておきます。 状態遷移図のガード条件でも、これを使うようにします。 (実際のモデルでは、もっと説明的な名前をつけるべきでしょう。)

(define (g? x) (= x 0))

チャネルに属するチャネルイベントは、関数 channel-events で手に入ります。 (channel-events ch) は ch に属するすべてのチャネルイベントのリストを返します。 順序に意味はありません。

チャネルイベントからチャネル引数を取り出すには関数 channel-event-args を使います。 引数が1個しかない場合でも、引数のリストになる点に注意してください。

改名マップ作成の戦略はこうです。 まず channel-events によってチャネルイベントを列挙します。 つぎに各チャネルイベントの引数を channel-event-args で取り出し、g? で分類します。 分類されたチャネルイベントをそれぞれイベント ca0, ca とペアにすれば改名マップができあがります。

(define-process P-ABS3
  (rename
      `((,d . ,da)
        ,@(map (lambda (x)
                 (if (g? (car (channel-event-args x)))
                     (cons x ca0)
                     (cons x ca)))
               (channel-events c)))
    P0))

こうしておけば、チャネル c の定義域が変わっても、場合分けの条件が変わっても、改名マップを修正しなくて済みます。

2013/08/16
© 2013,2014,2015 PRINCIPIA Limited