5分で価値を体験

前提: Alloy Analyzer を起動 できること。

この章のゴール

• ソースに書かれた run / check を、ツール上では Execute で実行し、結果を Show で見る
• SAT/UNSAT（または同様の結果表記）を、「設計上、ありうる/矛盾している」に読み替えられる

手順

1. New で新規。エディタに下を貼り、Save（保存）する。

sig Item {}
one sig Inventory {
  contains: set Item
}
pred someItems {
  #Inventory.contains > 0
}
run someItems for 3

assert allItemsListed { all i: Item | i in Inventory.contains }
check allItemsListed for 3

check 側の例は、「宇宙にいる Item はみな在庫 contains に入っている」と主張する、という解釈にしています。Item の一部だけが在庫に載っている世界を許す run の解では、この主張は成り立たないことが多く、反例（反証となるインスタンス）が出やすいです。
量化了な i を本文（i in ...）で必ず使う形にしてあり、未使用変数のコンパイラ警告が出ないようにしてあります。

2. ツールバーから Execute（実行）— 上から順に、デフォルトで定義した run / check が走る動きを想定。実際の既定順は版で違うことがある。まず run 相当が選ばれていることを確認（メニューでコマンドを切り替えられる版もある）。
3. 結果（解あり/なし 等）を確認し、Show（あるいは Visualizer/Theme へ進む導線）でインスタンスを眺める。
4. 同じく Execute で check 側（assert）を走らせ、反例が出るか/出ないかを見る（版によって「次の解」「どの断片を走らせるか」の操作が違います。迷ったら Alloy Analyzer の操作）。

何が得られたか

• 例がある（run が満たす解を示す）= 想定世界が一つは成り立つ、という具体例
• 性質に反例がある（check）= 制約の書き方と意図が食い違う、という手がかり
• どちらも、議論の「たぶん」に対する手触りになる

用語の対照は Alloy Analyzer の UI 用語 を参照。次は 最初のモデル で、小さなドメインを一緒に式にします。