旗の組み合わせ 269 万通りを全部歩く。「世界が黙る状態」は無いか
Walking all 2.69 million flag combinations: is there a state where the world goes silent?
D18-4-T36-reach-state-space・技術・日本語入力でプレイする仕組み
聞き込みの順番は、プレイヤーごとに違います。
どんな順で聞いても、次にどこへ向かえばいいかの一文が必ず出て、3 回の発話で前へ進めるか。
これを遊ばずに確かめるため、フラグの組み合わせとしてありうる状態を全部歩いています。
今日の版で 2,699,496 状態でした。
夕方の T35（clearpath）は、クリアに要る手を後ろ向きに 1 本だけたどる道具でした。
こちらは前向きに、全部の状態を歩きます。
この回の位置と、前後の回#
区切り: T34〜T49 確かめ方（16 回のうち 3 回目）
先に読むとよい回: T35（解ける道を逆算する）
次に読む回: T37（台本の中に期待を書く）
名前 — explicit-state model checking#
- 正式名
- explicit-state model checking
- 略称
- なし（使う道具の名前で呼ばれることが多い。SPIN、Murφ、TLC など）
- 日本語
- 明示的状態のモデル検査
- 初出
- model checking は、Edmund M. Clarke と E. Allen Emerson の "Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic"（Workshop on Logics of Programs 1981、LNCS 131、1982）と、Jean-Pierre Queille と Joseph Sifakis の "Specification and Verification of Concurrent Systems in CESAR"（International Symposium on Programming 1982、LNCS 137）が、それぞれ独立に始めたものです。
- 関連
- safety property（Leslie Lamport、"Proving the Correctness of Multiprocess Programs"、IEEE TSE、1977 が safety と liveness の語を導入）、bounded model checking（Armin Biere・Alessandro Cimatti・Edmund M. Clarke・Yunshan Zhu、"Symbolic Model Checking without BDDs"、TACAS 1999）
model checking とは#
model checking（モデル検査）とは、系の振る舞いを状態と遷移のグラフとして持ち、そのグラフの上で、ある性質が成り立つかを機械が全部調べる方法です。
テストが「試した経路」しか見ないのに対し、全部の経路について言えるのが違いです。
性質は時相論理で書くのがふつうです。
二つの型があります。
- safety（安全性）… 悪いことは決して起きない。「どの到達状態でも p が成り立つ」。CTL なら AG p、LTL なら G p。破れるときは、悪い状態へ至る有限の経路が反例になります。
- liveness（活性）… 良いことはいつか必ず起きる。「要求すれば、いつか応答がある」。反例は無限の経路（ループ）になります。
explicit-state は、状態を 1 つずつ実際に作って列挙するやり方です。
初期状態から遷移を展開し、見た状態をハッシュ表に入れ、まだ見ていない状態だけを積む。
到達した状態ごとに、性質を確かめる。
SPIN（Holzmann）や Murφ（Dill）がこの系統です。
よく知られた弱点は state space explosion（状態爆発）です。
真偽の旗が n 本あれば、状態は最大 2 の n 乗。
並行プロセスなら、各プロセスの状態の積になります。
対策として、半順序簡約、対称性の簡約、状態の圧縮（bit-state hashing）などが使われます。
もう一つの系統が記号的な方法です。
状態の集合を BDD や論理式でまとめて扱います。
bounded model checking（BMC）はその一つで、遷移を k 段だけ展開して命題論理の式にし、SAT ソルバに「k 手以内に性質を破る経路はあるか」を解かせます。
k 手以内の反例は確実に見つかりますが、k より深い反例については何も言えません。
有界なのは「探索の深さ」です。
うちの状態#
reach の状態は、立っているフラグの集合です。
場所も、話し相手も、手帳の中身も、状態に入れていません。
進行を決めるのはフラグだけだからです。
宣言されたフラグは 102 本（flags.json）。
章を表す擬似フラグ（phase:1〜3）を 3 本足して、105 ビットです。
上限は 192 ビット、64 ビットの語 3 つです。
static constexpr size_t kReachMaxFlags = 192;
struct FlagMask
{
static constexpr size_t kWords = kReachMaxFlags / 64;
std::array<uint64_t, kWords> W{};
static FlagMask Bit(int I) { FlagMask M; M.W[(size_t)I >> 6] = (uint64_t)1 << (I & 63); return M; }
...
};
105 ビットなら、組み合わせの上限は 2 の 105 乗です。
実際に到達するのは 2,699,496 状態でした。
フラグはほとんどが「前のフラグが立っていないと立たない」ので、組み合わせの大半は来ません。
遷移#
1 手は、1 回の発話です。
ある意図が、いまの状態で選ぶ段の sets（立てるフラグ）が、遷移の中身です。
段の選び方は、実行時と同じ関数を通します。
auto StepPick = [&](const Step& Sp, const FlagMask& S) -> kaede::adv::TierPick {
if (!Met(Sp.Active, S)) { return kaede::adv::TierPick{}; }
return kaede::adv::PickByTier(
(int)Sp.Confront.size(), [&](int i) { return Met(Sp.Confront[i], S); },
(int)Sp.Plain.size(), [&](int i) { return Met(Sp.Plain[i], S); });
};
PickByTier は AdvIntents.hpp にあり、ゲームの実行時の段選びもこれを呼びます。
2026-09-01 まで、reach の中に同じ規則の写しがありました。
写しがあると、片方だけ規則を変えても検査は緑のまま通ります。
いまは同じ 1 本を呼んでいます。
移動は手数に数えません。
場所に入ると立つフラグや、条件つきのイベントは、0 手の遷移として閉包を取ります。
auto Closure = [&](FlagMask S) {
bool bChanged = true;
while (bChanged)
{
bChanged = false;
for (const AutoSet& A : Autos)
{
if (Met(A.When, S) && (S | A.Sets) != S) { S |= A.Sets; bChanged = true; }
}
}
return S;
};
意図が有効かどうか（場所・話者の在席・章・requires）は、全部 1 つの条件に畳んであります。
在席の条件は 2026-08-23 に足しました。
それまで、居ない人と話せることになっていました。
近似が三つあります。
- 言葉の条件（その話題の語を言ったか）は、いつでも満たせるとみなす。プレイヤーは言おうと思えば言えるからです。
- 態度で変わる段（丁寧に・強く）は sets を持てない決まりなので、遷移に入れない。
- 回数の条件のような派生のフラグ（sys_*）を要る段は、成り立たないとみなす。
探索#
章ごとに歩きます。
for (const int P : PhaseList)
{
FlagMask Base;
if (P == Engine.data.initial.phase) { Base = Init; }
else if (EnterSeen[P]) { Base = Closure(Enter[P]); }
else { continue; }
std::vector<FlagMask> Queue{ Base };
Visited.Insert(Base);
while (!Queue.empty())
{
const FlagMask S = Queue.back();
Queue.pop_back();
for (const Step& Sp : Steps)
{
if (Sp.Phase != 0 && Sp.Phase != P) { continue; }
const FlagMask Add = StepSets(Sp, S);
if (!Add.Any() || (S | Add) == S) { continue; }
const FlagMask N = Closure(S | Add);
const int NP = TopPhase(N);
if (NP > P)
{
if (!EnterSeen[NP]) { Enter[NP] = N; EnterSeen[NP] = true; }
else { Enter[NP] = Enter[NP] & N; }
Visited.Insert(N);
continue;
}
if (Visited.Insert(N)) { Queue.push_back(N); }
}
}
}
次の章の出発点は、その章へ入ったすべての状態の積（AND）です。
つまり、前の章でどの道を通っても必ず立っているフラグだけを持って、次の章を歩き始めます。
前の章の寄り道で立つフラグを、次の章の前提にさせないためです。
章ごとに歩くのは、2026-09-09 からです。
章をまたいで一度に歩くと、章 1 の寄り道の有無 × 章 2 の寄り道の有無 × … の積になります。
第二章を足したところで 45,017,568 状態になり、約 9GB を使って OS に止められました。
章ごとに歩けば、積が和になります。
到達集合は、開番地法（線形探査）の平坦なハッシュ表 1 つで持ちます。
std::set では 1 件ごとにノードを確保し、4,500 万件を超えたところで止まったからです。
ハッシュは FNV で混ぜたあと、仕上げにもう一度撹拌しています。
uint64_t H = 1469598103934665603ull;
for (uint64_t X : M.W) { H ^= X; H *= 1099511628211ull; }
// 仕上げの撹拌が要る。 FNV だけだと低位ビットが偏り、線形探査の塊ができて
// 件数が増えるほど遅くなる（2026-09-09 実測: 20万件で 32k件/秒 → 300万件で 15k件/秒）。
H ^= H >> 33; H *= 0xff51afd7ed558ccdULL;
H ^= H >> 33; H *= 0xc4ceb9fe1a85ec53ULL;
H ^= H >> 33;
コメントは「BFS」と書いていますが、実装は配列の末尾から取り出すので深さ優先です。
到達集合は歩く順に関係なく同じなので、結果は変わりません。
確かめる性質#
到達したすべての状態について、二つを見ます。
一つ目、focusless。
その状態で、焦点（画面の上に出る「次に何をするか」の一文）が必ず 1 つ出るか。
焦点は hints.json の上から順に、requires を満たし、missing のフラグがまだ立っていない最初の 1 件です。
第一章の例を写します。
{"missing": ["f_hal_saeki_8pm"], "text": "聞いた話の裏を、まだ取っていない", "rescue": "「昨夜、佐伯さんは来たか」と聞いてみよう", "rescueWho": "hal", "rescueWhere": "banya"}
佐伯から夜の居場所を聞き、女将の証言をまだ取っていない状態では、この一文が出ます。
どの焦点の条件にも当てはまらない状態があれば、その状態では世界が黙ります。
二つ目、unguided。
出た焦点の missing のフラグを、--max-steps 手以内の発話で立てられるか。
std::function<bool(const FlagMask&, const FlagMask&, int)> CanGain = [&](const FlagMask& S, const FlagMask& Want, int Depth) -> bool
{
if (Depth <= 0) { return false; }
for (const Step& Sp : Steps)
{
const FlagMask Add = StepSets(Sp, S);
if (!Add.Any() || (S | Add) == S) { continue; }
const FlagMask N = Closure(S | Add);
if ((N & Want).Any()) { return true; }
if (CanGain(N, Want, Depth - 1)) { return true; }
}
return false;
};
焦点が「女将に聞け」と言っているのに、女将の証言を立てるには 5 手かかる、という状態を見つけます。
焦点はあるのに、焦点の先へ行けない状態です。
ほかに、どの到達状態でも requires が成り立たない段（書いたのに誰も読めない台詞・dead-stage）、名前がまだ明かされていない人物の名前を口にしうる段（name-leak）、仮説が「立ってから崩れる」順で起こりうるか（hypotheses）も、同じ到達集合で見ています。
テスト計画の合格条件の 2 番目が、この結果です（unguided=0・focusless=0・dead-stage=0）。
今日の値（10/29） — explicit-state model checking#
既定（手数の上限 3）:
REACH states=2699496 focusless=0 unguided=0 hypotheses=2/2 name-leak(warn)=0 allowed=12 focus-name-leak(warn)=0 focus-allowed=0 stale-allow=0 dead-stage=0 maxSteps=3
REACH walked=3 章ぶん（章ごとに歩く・2026-09-09）
REACH VERDICT=PASS
2 分 26 秒でした。
手数の上限だけを変えて、同じ版でもう 2 回流しました。
- 上限 1 … unguided 61,872 状態・FAIL（2 分 25 秒）
- 上限 2 … unguided 0・PASS（2 分 31 秒）
- 上限 3 … unguided 0・PASS
到達状態の数は、3 回とも 2,699,496 で同じです。
変わったのは、各状態で「焦点の先へ何手で届くか」を何手まで許すか、だけです。
上限 1 では、焦点の先へ 1 手では届かない状態が 6 万あります。
2 手なら、全部の状態で届きます。
既定の 3 は、1 手ぶんの余裕を持った線です。
名前どおりでない所 — explicit-state model checking#
探索の部分は、explicit-state model checking として名前どおりです。
状態を 1 つずつ作り、ハッシュ表で重複を除き、到達した全部の状態で性質を見ています。
状態数が 1 億を超えたら止まるだけで、途中で打ち切ってはいません。
違うのは三つです。
一つ目、「bounded」の意味。
うちの名前の対応表（named-methods-audit）は、この行を「--max-steps 3 で切っているので、正確には bounded model checking」と書いています。
ソースを読むと、そうなっていません。
--max-steps は探索の深さではなく、unguided の性質の中の「n 手以内」にだけ効きます。
到達状態は、手数に関係なく全部歩きます。
Biere らの BMC は「k 段まで展開した経路の上で反例を探す」方法で、深さで切るのは探索の方です。
しかも SAT に帰着させる記号的な方法で、状態を 1 つずつ作りません。
うちの reach は、全探索の上で「有界の応答」を確かめている、と言うのが正確です。
対応表の書き方は、この回で報告に回しました（連載の T02 の表も、同じ書き方をしていました）。
二つ目、unguided は典型的な safety property ではありません。
focusless は「どの到達状態でも焦点がある」で、AG p の形の不変条件、つまり safety そのものです。
unguided は「どの到達状態からも、3 手以内に焦点の先へ届く道が存在する」です。
CTL で書けば AG（3 手以内に EF）で、「存在する道」が入る分岐時間の性質です。
線形の経路の上で定義される safety と liveness の分け方には、そのまま入りません。
対応表は両方を safety と書いていますが、本文ではこう分けました。
三つ目、抽象化が片側に寄っていません。
言葉の条件をいつでも満たせるとみなすのは、プレイヤーにできることを広く取る近似です。
この近似は「届く」を言いすぎる方向に働きます。
reach が「3 手で届く」と言っても、その 3 手の言い方が照合で拾われるかは見ていません。
実際、焦点の先に受け皿の段しか無く、AI のプレイヤー 3 人が全員そこで止まったことがあります（2026-09-20）。
reach は緑でした。
一方で、回数の条件を持つ段を「成り立たない」とみなすのは、狭く取る近似です。
どちらに外れるかは、条件の種類ごとに違います。
弱点と、採らなかった案 — explicit-state model checking#
- 訪問した場所や、会った人は状態に入っていません。「まだ行っていない場所の名前を、焦点が先に使う」型の漏れは、ここでは見えません。ソースのコメントに、二つの形を試して両方外した記録が残っています。
- 1 回 2 分半かかります。データを変えるたびには回さず、ループの節目で回しています。
- unguided は状態の数で数えます。1 つの焦点の欠陥が何万状態に出ると、何万と出ます。反例の表示は先頭の 5 件だけです。上限 1 の 61,872 も、欠陥の種類の数ではありません。
採らなかった案です。
- SPIN や TLA+ の TLC のような既成の model checker へデータを書き出す。書き出すと、段選びの規則をもう一つの言語で写すことになります。上に書いたとおり、写しは片側だけ変わります。状態数が手元の RAM に収まる間は、実行時と同じ C++ の関数を呼ぶ方を選んでいます。
- BDD や SAT を使う記号的な方法。到達状態が数百万なら、平坦な表に全部入ります（1 件 24 バイト）。全部の状態を手で持っている方が、反例をそのまま表示でき、名前の先出しのような別の検査を同じ集合で回せます。
- 全部の章を一度に歩く。上に書いたとおり、積になって止まりました。
検索語#
explicit-state model checking
state space explosion
bounded model checking SAT
safety liveness Lamport
聞き込みの順番は自由です。どの順で聞いても、画面の上の一文が次の行き先を言うはずです。『霧走町 流氷に眠る』の第一章をブラウザで遊んで、黙る瞬間があるか試してみてください。プロフィールのリンクから。