唐突に、狼と香辛料というラノベがほしくなった。それで、セブンアンドワイの携帯サイトで注文してみることに。前々から思ってたんだけど、セブンアンドワイの携帯サイトって本を売る気がないんよね。ずっと品質が低いなとは思ってたけど、少なくともここ数…

LTSAでは、複数のプロセスを簡単に合成できます。 今回の例は、まだまだライトで続けます。今回は、ライトとスイッチの連携を表現してみます。まず、ライトの定義をします。ライトの状態遷移図を下記のように定義します。今回のライトは、ボタンを押すと消灯…

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

SWITCH = (on -> off -> SWITCH). この定義は何を示すかというと、次のようなラベルのシーケンスを定義していることになります。 on -> off -> on -> off -> on -> off ... この場合、onとoffがラベルになります。さて、シーケンスが定義されれば、その正し…

２回目です。 前回、LTSAで何ができるか書き忘れた。一言で言うと、シーケンスを定義して、そのシーケンスが定義された性質を満たすかどうかを形式的に検証できるツールです。 それではさっそく、続きに行きます。