演習

用語の注意: 本書のソースコード中では run / check という言語の用語をそのまま使います。一方、画面の手順では Alloy Analyzer の UI 用語 の Execute 等に合わせてください。

解答の方針は 一つではありません。まず 解が出るか / 反例が出るか を確認し、そのあとで制約を絞り込む、という順が学習には向きます。

1. 著者は少なくとも一人

examples/hello.als（またはリポジトリの examples/hello.als）を出発点に、すべての本に少なくとも一人の著者がいることを fact で表現し、run で解が得られることを確認してください。

ヒント: Book 全体に対する all 量化と、wrote の逆方向の関係を考えます。

2. 著者は高々一人

同じモデルで、各本の著者は高々一人（重複著者なし）を追加したとき、意図した挙動になるかを確認してください。check で性質を書いても、run で反例を探しても構いません。

3. CLI（余力）

インストールした配布物の CLI で、上記のいずれかのファイルを非対話的に実行し、CI に載せるイメージを掴んでください。オプション名は版固有情報のため、手元の --help を正としてください。

次の章

次の一歩 へ。