そういう時に着ていくスーツのズボンのチャックが閉まらないという大変残念な状態で、orz、俺。 確かに、腹周りがだいぶオヤジ体型になったとはいえ、ちょっ、それなんて言うメタボｗ状態でスーツが着れなくなってるとは。 最悪だ。 本当に最悪だ。 明日着て…

すげー勢いで、毎日１日、最長記録を更新中。 酒はまだやめられそうにないけど、タバコはこれで禁煙成功と言って大丈夫か！？

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

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

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

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

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

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

JavaをＰＣにインストールする。 ダウンロード先のファイルをダウンロードして、展開する。 ２個ほどvbsがあるので、両方とも起動する。 デスクトップにltsaのアイコンがあるので、起動！！

http://www.doc.ic.ac.uk/ltsa/

LTSAは、Labelled Transition System Analyserの略です。フリーで利用できる形式的検証のためのツールです。 詳しい話は、適当にググってください。

唐突ですが、これから数回にかけて、LTSAについて紹介します。 半分勉強も兼ねてますので、ここで書かれていることがベストとか、教科書通りとかそんなことはありません。かなり亜流でしかも試行錯誤しながら書いています。とりあえず、思いつくままに色々な…