Alloy というのが面白いらしいのでやってみた。ちなみに、これを書いている時点で Alloy というのが何なのか説明を読んでも人に聞いても全くさっぱり分かってないですが、とりあえず触ってみます。
SAT ソルバと Kodkod
SAT というのはある問題を表現する手法で、日本語では 充足可能性問題 と言うそうです。ようするに AND OR NOT を使って表現出来る範囲の問題という事なのかな？
Kodkod というのは、これを使って、first order logic、transitive closure、partial models を解決する物とあります。transitive closure というのは聞き慣れない言葉ですが、wikipedia の説明だけ読むと、ある関係 R を沢山つなげた時に出来る関係らしいです。例えば、親子関係に対する先祖子孫関係とかです。first order logic を再帰的に使うのと同じだと思うけど、何で特別な言葉があるのか分かりません。また、partial model というのも良くわかりませんでした。
closure というと、関数オブジェクトの事だと思ってしまいそうですが、正規表現の * (Kleene closure) みたいに、「どんどん繰り返して作る」という意味があるみたいです。
alloy チュートリアル
チュートリアルは http://alloy.mit.edu/alloy4/tutorial4/ から始まります。ソフトの使い方の説明が分かるまではつまらないので、先に http://alloy.mit.edu/alloy4/tutorial4/frame-FS-2.html を読みます。
- 右上の窓に表示されるソースを alloy にコピー(一番上のタイトル行だけ削除)
- check 文がテストケースみたいな物で、他の分が定義文
- Execute メニューに check 文がリストアップされるので、どれか選択するとその check 文が正しいかどうかをテストする。
これだけでは全部 valid になってしまって面白くないので、ワザと間違った文を入れます。
assert Wrong {
all obj, p: (FSObject - Root) | (obj.parent = p.parent)
}
check Wrong for 3ここで メニュー - Execute - check Wrong for 3 をすると invalid になります。そこで Counterexample リンクをクリックすると反例がグラフィカルに表示されます。
グラフをカスタマイズするには Theme をクリックします。例えば、左のツリーの relations - contents を選択して Show as arcs のチェックボックスを外して Close アイコンを押すと、contents の線が消えてすっきりします。Theme 画面のまま表示を確認するには projection: none のボタンを色々触ると反映されます。
と、ここまででやる気が出てから改めてチュートリアルを読み直す予定です。
