複数プロセスの合成

LTSAでは、複数のプロセスを簡単に合成できます。
今回の例は、まだまだライトで続けます。今回は、ライトとスイッチの連携を表現してみます。

まず、ライトの定義をします。ライトの状態遷移図を下記のように定義します。今回のライトは、ボタンを押すと消灯と点灯が繰り返されるようなライトにしました。

LTSAで表現すると次のようになります。ここでは、イベントとライトの状態を明示的に区別するため、状態をラベルで表現しています。

LIGHT = OFF,
OFF = (off -> push -> ON),
ON  = (on  -> push -> OFF).

次に、スイッチを表現します。スイッチは、左に倒れているときと、右に倒れているときの二つの状態を持つようなスイッチとします。スイッチが反対側に倒されると、ライトに対してpushイベントが発生するようにします。
ここでは、LIGHT##pushと記述すると、LIGHTに対してpushイベントを発出するという意味とします。

LTSAで表現すると次のようになります。ここでは、スイッチがどちらに倒れているかは重要ではないため、状態を明示的には示していません。

SWITCH = LEFT,
LEFT  = (turn_right -> push -> RIGHT),
RIGHT = (turn_left  -> push -> LEFT).

この二つのプロセスを合成してみましょう。
合成は、二つのプロセスを同じファイルに書いてコンパイルするだけです。
（他にも書き方はたくさんありますが、いったん簡単なやり方を示します。）

LIGHT = OFF,
OFF = (off -> push -> ON),
ON  = (on  -> push -> OFF).

SWITCH = LEFT,
LEFT  = (turn_right -> push -> RIGHT),
RIGHT = (turn_left  -> push -> LEFT).

ここで、二つを合わせるとどのような動きになるか見てみましょう。
上記のLTSA記述を書いてコンパイルしてみましょう。
そして、生成された状態遷移図のうち、「||DEFAULT」を見てみます。

この状態遷移図は、ライトとスイッチを合わせた状態遷移図となります。
状態0からは、ラベル「turn_right」とラベル「off」を経由して状態2へ、同様にラベル「turn_right」からラベル「off」を経由して状態2へと線が延びています。このように、LTSAでの合成では、ラベルの全ての発生順序を状態遷移として表現しています。そして、ラベル「push」でライトとスイッチは同期をとっています。

さっそく、アニメーションにより動作を確認してみましょう。

初期状態です。ラベル「off」とラベル「turn_right」が実行可能な状態となります。
まず、ラベル「off」を実行してみます。

ラベル「off」を実行すると、ライトの状態が遷移します。そして、次に実行できるのは、ラベル「turn_right」のみとなります。ラベル「push」は、

SWITCH側ではまだ実行できませんので、LIGHT側でも実行できない扱いになります。

ラベル「turn_right」を実行すると、SWITCHの状態が遷移し、ラベル「push」が実行できるようになります。

ラベル「push」を実行すると、SWITCHとLIGHTの双方が共に状態が遷移します。
このように、LTSAではラベル遷移間の同期によって、並列処理における同期点を定義することができます。