次の一歩

入門完了のチェックリスト

• 3 分で説明できる: Alloy / Analyzer を設計に持ち込むと、何が得られるか（曖昧さの削減、反例、具体例の探索）
• 画面語で辿れる: 少なくとも Save / Execute / Show 相当の何を指しているか、自分の手元の版で言える
• 一文で言える: run と check の違い（具体例の探索 / 不変条件の検査）と、それが設計上のどの問いに答えるか
• 一歩次へ: 公式ドキュメントか 実務への接続 のどこか一つに、次に何をするかを決めている

目的別

• 学習: 本書の 演習 と、英語で掘り下げるなら Practical Alloy を併用する
• 研究: 公式 ドキュメント と Alloy 6 概要 から、扱う時間・可変性の表現に合わせる
• チーム導入: CI・CLI・LSP の導入イメージは 実務への接続 を出発点にし、配布物の help とリリースノートを正にする

公式一次情報

• alloytools.org — ダウンロードとドキュメント（例: download.html、documentation、Alloy 6 概要）
• GitHub: org.alloytools.alloy — リリースノートと課題管理

学習用の本（英語）

• Practical Alloy — ハンズオン中心

コミュニティ

講演資料や論文、周辺ツール（LSP 等）の状況は移り変わります。最新は 公式サイトとリリース を併せて追うのが安全です。

このリポジトリへ

誤字・不整合・よりよい演習案は、Issue / PR で歓迎します。book.toml の git-repository-url や site-url を、あなたのフォーク先に合わせて更新したうえで、変更を送ってください。