実際に実行

まず，LTSA のエディタ画面に以下の FSP を記述しましょう．これは ON と OFF を繰り返すスイッチです．

SWITCH = OFF,
OFF    = (on -> ON),
ON     = (off-> OFF).

下の図のようになります．

次にコンパイルボタンを押してコンパイルしましょう．Draw タブを選択し，"SWITCH"を選択すると，生成された LTS を見ることができます．

LTSA アニメータ

LTSA のアニメータ機能を使用することによって，プロセスの振る舞いをシミュレーションすることができます．右上のアニメーションボタンを押すことで，アニメータを使用できます．

• 印のついた動作が選べる
• LTS では最近の動作が赤で示される