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

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

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

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

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