Alloy Analyzer の操作
この章で得られること
- 何が分かるか: ソースの
run/checkをソルブに渡した結果（SAT/UNSAT や同様表記。版依存）を、制約付き世界の有無/性質の反例の有無に読み替える - どう触るか: 画面操作は、まず Alloy Analyzer の UI 用語 の
New/Save/Execute/Showなど、ラベルで辿る（runという述語と、Run という英単語のボタン名を取り違えない） - 次に行く道: 非対話的な実行・CI には 実務への接続 を次の一歩として用意している
エディタと Execute（run / check の実行）
- コンパイル（エラーチェック）: エディタ上で構文・型のエラーを直す。直さない限り
Executeは意図どおりに進みません。 - ソルバの実行: モデルに
runやcheckなどのコマンドが定義されているとき、Executeによってソルブを走らせ、SAT（解あり）/ UNSAT（制約不整合）/ 有界完了 などの結果を読みます。表記の細部は版で異なります。
ソース上の キーワード run / check のまま会話に含めてよい一方、手順では「Execute を押し、定義した run 相当（または check 相当）を走らせる」と書くと、スクリーンショット上の用語と揃います。
インスタンスと Show / Theme
インスタンス（見つかった解）を、Show や Theme、表形式のビューで追うと、関係の形が掴みやすいです。大きいモデルでは、投影して見る、スコープを下げる、制約を分解する、といった切り方が有効です。
Visualizer
グラフや表の見え方の切替、ハイライト、レイアウトの調整など、直観の補助に使います。版によってメニュー名は変わるため、手元のヘルプと照合しながら慣れましょう。ここに進む導線は、版によって Show から繋がるか、Visualizer として別名になっているかが異なります。
CLI と LSP
Alloy 6.2.0 のリリースノートでは、配布 JAR に コマンドライン（例: java -jar <配布 jar> help でヘルプ）と LSP サーバ（起動オプション lsp）が記載されています。実際のサブコマンド名・オプションは、手元の help 出力と リリースノート を正としてください。
CI でモデルを走らせる、スクリプト化する、エディタ連携を試す、といった運用上の詳細手順の置き場所は、本書では重複を避け 実務への接続 に委ねます。入門本編の GUI 用語表は、引き続き Alloy Analyzer の UI 用語 を正とします。
PATHに CLI を通す、またはjava -jarで JAR を直接呼ぶ- オプションで入力ファイル、出力形式、解の個数、時間制限等を与える（
helpに従う） - 失敗（退出コード）を CI に載せる
OS ごとのパスやファイル名は、JAR 配布か OS パッケージかで変わります。配布物の README を正とし、どのバイナリ（または JAR）が alloy 相当かをインストール先で確認してください。
困ったとき（最小のトラブルシュート）
Saveしたか — 手順が期待どおりに動かない多くは、未保存や別ファイルを見ているのが原因です。SaveしてからExecute。- スコープが狭すぎないか —
for 3等が厳しすぎると、意図した反例や解を見落とすことがあります。まず上げ下げを試す。 - 制約が強すぎないか — 一度に詰め込まず、
factを外す／assertを弱める、と分割してどこで UNSAT になるかを切り分ける。
次の章
可変性とトレース（Alloy 6） では、状態と時間の扱いの入口に触れます。