初歩の初歩

初歩の初歩ということで、LTSAの最初の例としてよく取り上げられる、電気のスイッチを試してみます。スイッチを入れると電気が付き、スイッチを消すと電気が消えるというやつです。
さっそく、LTSAのプログラムを見てみましょう。

SWITCH = (on -> off -> SWITCH).

このプログラムは、次のことを表わしています。

  • SWITCHというのは、「on」というイベントが発生したのち、「off」というイベントが発生し、それ以降は同じイベント遷移が繰り返される。

次に、コンパイルしてみましょう。

コンパイルするためには、MINIMIZEボタンを押します。
すると、「Output」タブにこんなメッセージが出力されます。

Compiled: SWITCH
Composition:
DEFAULT = SWITCH
State Space:
 2 = 2 ** 1
Composing...

    

  • 

      

    • States: 2 Transitions: 2 Memory used: 7664K
      • 

    • 

Composed in 63ms
DEFAULT minimising..
Minimised States: 2 in 1ms

こんなメッセージが出力されれば成功です。
ここで、「Draw」タブにて状態遷移図が表示されているので、確認してみましょう。

丸は状態を表し、矢印線にて状態遷移を表現しています。
状態は自動で生成されます。この状態遷移図は、0にて電気が消灯、1にて電気が点灯していることを表しています。

ライトは、次のようにも表現できます。
最初は、ライトは消えている状態（LIGHT_OFF）です。
そして、イベント「on」が発生すると、ライトが点いている状態（LIGHT_ON）になり、イベント「off」が発生すると、再びライトは消えている状態になることを表しています。

SWITCH = LIGHT_OFF,
LIGHT_OFF = (on  -> LIGHT_ON),
LIGHT_ON  = (off -> LIGHT_OFF).

コンパイルすると、先ほどの記述と全く同じ結果が出ていることがわかります。

Compiled: SWITCH
Composition:
DEFAULT = SWITCH
State Space:
 2 = 2 ** 1
Composing...

    

  • 

      

    • States: 2 Transitions: 2 Memory used: 7560K
      • 

    • 

Composed in 56ms
DEFAULT minimising..
Minimised States: 2 in 1ms

最後に、状態遷移図を実行してみます。

実行ボタンを押します。

こんな画面が出てきます。チェックボックスが、利用可能な遷移イベントになります。
ここでは、「on」イベントが利用できます。さっそく、「on」イベントを実行してみましょう。

実行すると、画面上の状態遷移図が上記のように変わります。
「on」イベントが実行され、状態が「0」から「1」に遷移したことを表します。
状態が遷移したことで、次に実行できるイベントが下記のように変化しています。

当然、今度は「off」イベントを発生させると、元通りに戻ります。

今日はこんなところで、終了。