可変性とトレース（Alloy 6）

本編では時間と状態の入り口に立つ章です。先に 言語の基礎 と Alloy Analyzer の操作（必要なら Alloy Analyzer の UI 用語）を済ませておくと、トレースの読み方がつかみやすいです。

Alloy 6 では、可変な状態や実行のトレースを扱う表現が強化され、より「振る舞い」の探索に近づけます。一次情報は Alloy 6 の紹介 と ドキュメント を参照してください。

何のための章か

• ある初期状態から遷移の列を探索し、仕様が意図した通りかを見る
• 不変条件がトレース全体で保たれるかを check で押さえる

学び方のすすめ

1. まず小さな 遷移システム（数行の sig と pred）で run し、Visualizer で列として見る
2. util/ordering など、標準ライブラリの慣用に慣れる
3. スコープを上げる前に、遷移の長さや状態の大きさを分けて調整する

このブックでは入り口のみ示し、本文の深掘りは公式資料と Practical Alloy 等へ委ねます。

次の章

演習 で手を動かしましょう。