目視の検査のテクニック - Alloy Analyzer で形式仕様記述

工事中

今回は、目視の検査についてのテクニックをご紹介します。

第１回では、簡単で小さな仕様を Alloy で記述して目視で検査してみました。
目視の検査をすると、なかなか見たいものが出てこなかったり、ゴミが出てきたり、何か出てきてもパッと見どうなっているのかすぐに分からなかったりすることがあります。
こういうイライラを解消するために、今回は具体的に以下の３つのテクニックをご紹介します。

• インスタンスの数を制限する
• 見たいインスタンスだけを探す
• インスタンスの見た目をカスタマイズする

今後はより複雑で規模の大きい仕様を扱っていくので、目視の検査が大変になっていきます。
ぜひ今回ご紹介するテクニックを使いこなせるようになってください。

1. インスタンスの数を制限する

第１回でボタンの状態空間のインスタンスを run show 見つけて表示すると、
ボタンの状態が１個表示されたり、２個表示されたりと、見つかる数がバラバラでした。