Alloy Analyzer の UI 用語
方針: 手順の本文では、画面のラベル（下表「このブックの呼び方」）を使う。コード断片内の run / check など言語キーワードはそのまま。
主なツールバー（例: Alloy 6.2.0 付近の GUI）
| このブックの呼び方 | ざっくり役割 | 補足 |
|---|---|---|
| New | 新しいモデル | |
| Open | ファイルを開く | |
| Reload | 再読み込み | |
| Save | 保存 | 手順不整合の多くは未保存が原因 |
| Execute | モデルに書かれた run / check 等をソルバに渡す | 版で「何を最初に走らせるか」は異なる。メニューで対象を選べる版も |
| Show | インスタンスやグラフ表示系へ | 版で Visualizer/Theme との違いを確認 |
画面語と Alloy 言語
| 画面で行う操作の内容 | ソース上の用語（例） |
|---|---|
| 具体例（世界）を探す | run（述語） |
| 性質が常に成り立つか | assert + check |
| インスタンスの探索範囲 | for スコープ（例: for 3） |
版差: メニュー名が「Run」「Build」等に違う場合は、手元の表示を正とし、本ブックの表は「意味の地図」として読んでください。乖離を見つけたら リポジトリ へ指摘歓迎です。