10.3 死锁与可解性检测

#!/usr/bin/env python3
# file: sim/gd_mech_10_detection.py
# tier: S
# verify: /opt/homebrew/bin/python3 sim/gd_mech_10_detection.py
"""10.3 死锁与可解性检测（S 层）。

4.3 已交付 core/src/ashdeck/solvability.ts（BFS + digest 去重 + 三重上限）。本节在它
**之上**给一张判据表，把四种「卡住」分门别类检测出来，并说清可靠性边界：
  可解       找到取胜序列 → solvable=True，恒可靠（有证据）
  不可解证明 前沿被穷尽（exhausted=True）→ solvable=False 是证明
  截断       撞上某个上限（truncated=True）→ 只能说「限深内没搜到」
  死锁       未结束且无合法动作（摘掉 e 的动作集变体下才可达）

用与 solvability.ts 同口径的 Python BFS 逐 fixture 复算，输出 CSV 与判据表。
全整数，无浮点，无 random。
"""
from __future__ import annotations

import copy
import os
import sys

import ashlib

ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))


def cost(spec, cid):
    return next((c["cost"] for c in spec["cards"] if c["id"] == cid), 999999)


def acts_of(spec, s, allow_e=True):
    if s["over"]:
        return []
    a = ["p" + str(i) for i, cid in enumerate(s["hand"]) if cost(spec, cid) <= s["energy"]]
    if allow_e:
        a.append("e")
    return a


def is_stall(spec, seq, s, allow_e=True):
    if s["over"]:
        return False
    a = acts_of(spec, s, allow_e)
    if not a:
        return False
    base = ashlib.digest(s)
    return all(ashlib.digest(ashlib.run_spec(spec, seq + [x])) == base for x in a)


def search(spec, max_steps=12, max_nodes=200000, max_branch=6, allow_e=True):
    """与 core/src/ashdeck/solvability.ts 的 searchSolvable 同口径。"""
    seen = {ashlib.digest(ashlib.run_spec(spec, []))}
    frontier = [[]]
    nodes, expanded, deadlocks, stalls, max_seen = 1, 0, 0, 0, 0
    solution, exhausted, truncated = None, False, False
    for _ in range(1, max_steps + 1):
        nxt = []
        for seq in frontier:
            s = ashlib.run_spec(spec, seq)
            expanded += 1
            a = acts_of(spec, s, allow_e)
            max_seen = max(max_seen, len(a))
            if not s["over"] and not a:
                deadlocks += 1
            if is_stall(spec, seq, s, allow_e):
                stalls += 1
            if len(a) > max_branch:
                truncated, a = True, a[:max_branch]
            for x in a:
                child = seq + [x]
                snap = ashlib.run_spec(spec, child)
                if snap["won"]:
                    solution = child
                    break
                g = ashlib.digest(snap)
                if g in seen:
                    continue
                if nodes >= max_nodes:
                    truncated = True
                    break
                seen.add(g)
                nodes += 1
                nxt.append(child)
            if solution is not None or truncated:
                break
        if solution is not None or truncated:
            break
        if not nxt:
            exhausted = True
            break
        frontier = nxt
    if solution is None and not exhausted:
        truncated = True
    return {"solvable": solution is not None, "solution": solution or [], "nodes": nodes,
            "expanded": expanded, "deadlocks": deadlocks, "stalls": stalls,
            "maxBranchSeen": max_seen, "exhausted": exhausted, "truncated": truncated}


def verdict(r):
    """四类判据，按特异性从高到低判定。"""
    if r["solvable"]:
        return "可解(证据)"
    if r["deadlocks"] > 0:
        return "死锁"
    if r["exhausted"] and not r["truncated"]:
        return "不可解(证明)"
    return "截断(未搜到)"


def main():
    spec = ashlib.load_spec()
    deep = copy.deepcopy(spec)
    deep["params"]["enemyHp"] = 999
    deep["params"]["turnLimit"] = 2
    fixtures = [("baseline", spec, 12, True), ("unsolvable", deep, 12, True),
                ("truncated", deep, 8, True), ("deadlock", spec, 12, False)]
    header = ["fixture", "solvable", "solLen", "nodes", "expanded", "deadlocks",
              "stalls", "exhausted", "truncated", "verdict"]
    rows = []
    for name, fx, steps, allow_e in fixtures:
        r = search(fx, max_steps=steps, allow_e=allow_e)
        rows.append([name, str(r["solvable"]).lower(), len(r["solution"]), r["nodes"],
                     r["expanded"], r["deadlocks"], r["stalls"], str(r["exhausted"]).lower(),
                     str(r["truncated"]).lower(), verdict(r)])
    n = ashlib.write_csv(os.path.join(ROOT, "out", "mech10_detection.csv"), header, rows)

    print(" ".join(header))
    for r in rows:
        print(" ".join(str(x) for x in r))
    print("wrote out/mech10_detection.csv rows=%d" % n)
    kinds = {r[0]: r[9] for r in rows}
    ok = (kinds["baseline"] == "可解(证据)" and kinds["unsolvable"] == "不可解(证明)"
          and kinds["truncated"] == "截断(未搜到)" and kinds["deadlock"] == "死锁")
    print("verdicts=%s" % kinds)
    print("allFourDistinct=%s" % ok)
    return 0 if ok else 1


if __name__ == "__main__":
    sys.exit(main())

fixture solvable solLen nodes expanded deadlocks stalls exhausted truncated verdict
baseline true 8 1517 912 0 0 false false 可解(证据)
unsolvable false 0 420 420 0 0 true false 不可解(证明)
truncated false 0 408 382 0 0 false true 截断(未搜到)
deadlock false 0 18 18 3 0 true false 死锁
wrote out/mech10_detection.csv rows=4
verdicts={'baseline': '可解(证据)', 'unsolvable': '不可解(证明)', 'truncated': '截断(未搜到)', 'deadlock': '死锁'}
allFourDistinct=True

// snippet: core/test/gd_mech_10_detection.test.ts 的关键断言
const r = searchSolvable(unsolvable());          // 敌方 999 血 + 2 回合上限
assert.equal(r.solvable, false);
assert.equal(r.exhausted, true);                 // 前沿被穷尽 → 这是证明
assert.equal(r.truncated, false);

const base = searchSolvable(SPEC);
assert.equal(base.solvable, true);
assert.equal(runSpec(SPEC, base.solution).won, true);   // true 有证据，可重放

const short = searchSolvable(unsolvable(), { ...DEFAULT_LIMITS, maxSteps: 8 });
assert.equal(short.exhausted, false);
assert.equal(short.truncated, true);             // 撞上限 → 只能说「没搜到」

✔ 判据一：无合法动作即死锁，但本规则下 e 恒合法故默认不可达 (0.752417ms)
✔ 判据二：无进展循环即停滞——e 必然推进 turn，故基线恒 false (0.243833ms)
✔ 判据三：资源不可达目标即不可解，穷尽前沿后是证明 (5.0865ms)
✔ 证明边界：true 有证据恒可靠，false 撞上限时只能说没搜到 (16.138125ms)
✔ 基线分类：可解、死锁 0、停滞 0——判据一与判据二在本规则下不可达 (11.409458ms)
ℹ tests 5
ℹ suites 0
ℹ pass 5
ℹ fail 0
ℹ cancelled 0
ℹ skipped 0
ℹ todo 0
ℹ duration_ms 241.324542