4.3 无死锁与可解性

// file: core/src/ashdeck/solvability.ts
// tier: P
// verify: node --test 'core/test/gd_mech_04_solvability.test.ts'
//
// 4.3 死锁与可解性：小规模穷举搜索。搜索树就是动作序列的**前缀树**。
// 两条前提都由 4.1 的测试背书：
//   - 前缀重放可用：runSpec 是纯函数，故回放前 k 条命令给出的快照与
//     「逐命令推进 k 次」逐字相同；
//   - digest 去重可用：digest 相同即状态相同（状态充分性），不会错杀。
//
// 本模块最要紧的一条是**结论的两级可靠性**：
//   solvable === true  —— 有一条取胜序列作为**证据**，与任何上限无关，恒可靠；
//   solvable === false —— 只有当 exhausted === true（前沿在 maxSteps 内被穷尽）
//                         时才是**证明**；truncated === true 时只能说「没搜到」。
//
// 本模块不读时钟、不读随机源（耗时由调用方测量），故 core/src/ashdeck/ 全目录
// 都满足「状态机确定性不依赖时间」——4.1 的源码扫描会断言这一点。

import type { Snapshot, Spec } from "./types.ts";
import { runSpec } from "./combat.ts";
import { digestSnap } from "./digest.ts";

export type Limits = {
  maxSteps: number; // 动作序列长度上限
  maxNodes: number; // 去重后状态数上限
  maxBranch: number; // 单步候选动作上限（本规则下 = handSize + 1）
};

export const DEFAULT_LIMITS: Limits = { maxSteps: 12, maxNodes: 200000, maxBranch: 6 };

export type SearchReport = {
  solvable: boolean;
  solution: string[];
  nodes: number; // 去重后的可达状态数（含根）
  expanded: number; // 实际展开过的状态数
  deadlocks: number; // 未结束且无合法动作
  stalls: number; // 未结束、有合法动作，但每个都不改变状态
  maxBranchSeen: number;
  exhausted: boolean; // 前沿被穷尽 → solvable=false 是证明
  truncated: boolean; // 撞上某个上限 → 结论不完整
};

const UNPLAYABLE = 999999;

/** 卡片费用；未知 id 视为不可负担。整数，无浮点。 */
export function cardCost(spec: Spec, id: string): number {
  for (const c of spec.cards) if (c.id === id) return c.cost;
  return UNPLAYABLE;
}

/**
 * 合法动作集：可负担的出牌 p<i>，以及（默认）结束回合 e。
 * allowEndTurn=false 是给检测器自证的**动作集变体**：本规则下 e 恒合法，
 * 死锁不可达，只有把 e 摘掉才能构造出一个真会响的负例。
 */
export function legalActions(spec: Spec, s: Snapshot, allowEndTurn = true): string[] {
  if (s.over) return [];
  const out: string[] = [];
  for (let i = 0; i < s.hand.length; i += 1) {
    if (cardCost(spec, s.hand[i]) <= s.energy) out.push("p" + i);
  }
  if (allowEndTurn) out.push("e");
  return out;
}

/** 死锁：未结束且没有任何合法动作。 */
export function isDeadlock(spec: Spec, s: Snapshot, allowEndTurn = true): boolean {
  return !s.over && legalActions(spec, s, allowEndTurn).length === 0;
}

/** 停滞：未结束、有合法动作，但每一个都不改变状态。 */
export function isStall(spec: Spec, seq: string[], s?: Snapshot): boolean {
  const snap = s ?? runSpec(spec, seq);
  if (snap.over) return false;
  const acts = legalActions(spec, snap);
  if (acts.length === 0) return false;
  const base = digestSnap(snap);
  return acts.every((a) => digestSnap(runSpec(spec, seq.concat([a]))) === base);
}

/**
 * 广度优先穷举：逐层展开，故找到的第一条取胜序列**最短**。
 * 去重键是 digest——合法动作非法化（p99 / 欠费）不改变状态，因而天然收敛。
 */
export function searchSolvable(spec: Spec, limits: Limits = DEFAULT_LIMITS): SearchReport {
  const root: string[] = [];
  const seen = new Set<string>([digestSnap(runSpec(spec, root))]);
  let frontier: string[][] = [root];
  let nodes = 1;
  let expanded = 0;
  let deadlocks = 0;
  let stalls = 0;
  let maxBranchSeen = 0;
  let solution: string[] | null = null;
  let exhausted = false;
  let truncated = false;

  for (let d = 1; d <= limits.maxSteps; d += 1) {
    const next: string[][] = [];
    for (const seq of frontier) {
      const s = runSpec(spec, seq);
      expanded += 1;
      let acts = legalActions(spec, s);
      if (acts.length > maxBranchSeen) maxBranchSeen = acts.length;
      if (!s.over && acts.length === 0) deadlocks += 1;
      if (isStall(spec, seq, s)) stalls += 1;
      if (acts.length > limits.maxBranch) {
        truncated = true; // 分支被截 → 完备性受损，如实标注
        acts = acts.slice(0, limits.maxBranch);
      }
      for (const a of acts) {
        const child = seq.concat([a]);
        const snap = runSpec(spec, child);
        if (snap.won) {
          solution = child;
          break;
        }
        const g = digestSnap(snap);
        if (seen.has(g)) continue;
        if (nodes >= limits.maxNodes) {
          truncated = true;
          break;
        }
        seen.add(g);
        nodes += 1;
        next.push(child);
      }
      if (solution !== null || truncated) break;
    }
    if (solution !== null || truncated) break;
    if (next.length === 0) {
      exhausted = true; // 前沿空 = 可达状态空间被穷尽
      break;
    }
    frontier = next;
  }
  if (solution === null && !exhausted) truncated = true;
  return {
    solvable: solution !== null,
    solution: solution ?? [],
    nodes,
    expanded,
    deadlocks,
    stalls,
    maxBranchSeen,
    exhausted,
    truncated,
  };
}

// snippet: core/test/gd_mech_04_solvability.test.ts 的三条关键断言
assert.equal(r.solvable, true);
assert.equal(r.solution.length, 8);   // 可解：解长 8，重放后 won === true
assert.deepEqual(r.solution, ["p1", "p1", "e", "p3", "p3", "e", "p3", "p3"]);

assert.equal(r.solvable, false);
assert.equal(r.exhausted, true);      // 不可解：前沿穷尽，这是证明
assert.equal(r.truncated, false);

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

[4.3] 基线可解 解长=8 状态=1517 展开=912 耗时=11ms
[4.3] 不可解证明 状态=420 展开=420 耗时=5ms
✔ 动作集：p<i> 按费用过滤，e 恒合法；分支上界 = handSize + 1 (0.6615ms)
✔ 可解：基线 spec 存在取胜序列，重放后确实取胜 (12.072333ms)
✔ 最短性：广度优先逐层展开，7 步以内无解 (8.038042ms)
✔ 无死锁：基线搜索中死锁与停滞均为 0 (10.142333ms)
✔ 死锁检测器会响：摘掉 e 之后，空手牌状态就是一个真死锁 (0.187083ms)
✔ 不可解：999 血 + 2 回合上限，搜索穷尽前沿后判不可解 (5.290625ms)
✔ 上限诚实：同一不可解 spec 在 8 步上限下结论不完整 (3.804584ms)
✔ 去重有效：实到状态数远小于无去重的理论上界 (9.424ms)
ℹ tests 8
ℹ suites 0
ℹ pass 8
ℹ fail 0
ℹ cancelled 0
ℹ skipped 0
ℹ todo 0
ℹ duration_ms 206.837833