最初のモデル

この章で得ること

何を式として切り出すか（sig や関係＝設計の境界）の感覚
run が「ありうる世界の具体例を探す」操作であること
ツール上では Alloy Analyzer の UI 用語の Execute / Show を使い、結果を読むところまで踏む

目標

シグニチャ（集合のような表現）とフィールド（関係）を最小限書く
run で 解を探索 する
結果を Analyzer 上で確認する

例: 本と著者

次の例は、本と人、そして「誰が著者か」という関係を表す最小モデルです。同じ内容は、サイト上では examples/hello.als（リポジトリ直下では examples/hello.als）からも開けます。

sig Book {}
sig Person { wrote: set Book }
pred show {}
run show for 3

ざっくり説明

sig は集合の枠。ここでは Book と Person があります。
wrote は Person から Book への関係（誰がどの本を著者とみなすか）です。set Book なので、著者 0 冊以上を持てます。
pred は述語。ここは空の show です（あとで拡張してもよい）。
run show for 3 は、大きさ 3 までの範囲でインスタンスを探す、という趣旨（厳密な解釈は Analyzer の表記に従います）。

手元で試す

Analyzer を起動する。
上のコードを新規ファイルに貼り、.als として**Save** する（未保存のまま Execute しても期待どおりに動かないことがあります）。
ツールバーから Execute して、モデルに書かれた run 相当をソルバに渡す（版によってはメニューで run / check のどれを先に走らせるか選びます。迷ったら Alloy Analyzer の操作）。
見つかったインスタンスを Show や Theme / Visualizer で眺める（用語の対照は Alloy Analyzer の UI 用語）。

run が UNSAT（解なし）になった場合、制約を強めすぎていないか、for のスコープが狭すぎないか、を疑うとよいです。

`check` の入口

run は「ある制約付きモデルの存在」を探し、assert に対する check は「常に成り立つか」をソルブで検査します。最初は run だけ使えれば十分です。

次の章

言語の基礎で、リレーションと制約の表現力を少し押さえます。