状態の表現

LTSAではラベルのシーケンスを明示的に記述します。状態は暗黙的に定義されます。
ですが、実際には状態を明示的に定義するほうが都合が良い場面が多々あります。
その時には、次のような工夫を行うことで、状態っぽいものを記述した気になれます。

LIGTH = OFF,
OFF = (off -> turn_on -> ON),
ON  = (on -> turn_off -> OFF).

ここでは、消灯状態をラベル「off」で表現し、点灯状態をラベル「on」で表現してみました。
そして、turn_onとturn_offをイベントとして表現してみました。
LTSAでは、次の状態遷移図に変換されます。

直観的な電灯の状態遷移図とは異なるでしょう。これは、LTSAがラベル遷移の記述を主目的としているための、ある種の限界といったところです。どちらの表現を利用するかは、LTSAを用いて何を行いたいかで使い分けます。たとえば、イベントの発生系列に主眼を置きたい場合は前回の方法を、状態遷移系列に主眼を置きたい場合には今回の方法を用いるなどが考えられます。