13.2 语义校验：可满足性与死条件
《游戏设计》卷一《玩法机制与可执行规格》 校验的是数值与规则：一条规则会不会让某个资源永远为负、会不会让某个动作永远无法触发。本节校验的是结构与条件：一个条件引用的状态量，在到达它所在的节点之前，有没有可能取到它要求的值。13.1 只看了图的形状，本节往图上叠加状态——但用的是区间，仍然不做路径枚举。两套共享「整数不变量 + 确定性」的工程纪律，判据则各自不同。
什么是死条件
死条件指一个条件在任何一条路径上都不可能成立。举一个具体的：若某个节点上挂着一句台词 line_when: ["aff","shen",">=",55]，而沿所有到达该节点的路径走下来，shen 最多只能涨到 50——那么这句台词永远不显示，这个条件就是死的。
死条件与「难触发」是两回事。难触发的条件只是概率低，只要有一条路径能成立就活着；死条件是可证否的：给不出任何一条路径让它成立。可证否这一点很重要，它让检测器可以给出确定的结论，而不是一个「大概没戏」的猜测。
判定算法：可达区间前向不动点
算法分两步，都不需要枚举完整状态空间：
- 求可达区间。 给对话图每个节点上每个好感度变量算一个整数区间
[lo, hi]。起点是点区间（初值即上下界）；每条选项把自己的效果（add一个整数）加到父节点的区间上，再把结果并进目标节点的区间。反复迭代到不动点——区间单调不减且上下界被[0,100]夹住，所以必然在有限轮收敛。 - 与条件比对。 每个条件位点（选项 / 台词 / 结局 / 场景边 / 地点解锁）拿自己所在节点的区间，和条件的阈值比：
>=看上界够不够，<看下界越没越过，==看阈值落不落在区间里。阈值落在区间外，就是死条件。
关键在于第 1 步是过近似：传播区间时不按条件剪枝，把每条边都当成可走。过近似只会把区间放宽，不会收窄。于是「过近似算出来的区间都够不着」蕴含「真实可达状态也够不着」——检测器因此不会误报。代价是可能漏报：真实的死条件在过近似下或许被放宽到看着可达。这条取舍是刻意的：一个会误报的校验器没人敢用。
S 层：区间不动点与死条件扫描
脚本复用 sim/na_00_spec_check.py 的 load_spec。flag 与 item 叶子另有一条判据：如果某个旗标从未被任何 set 写过、某个物品从未被任何 grant 给过，那么引用它的条件恒假——这也是一种死条件，但不需要区间。
#!/usr/bin/env python3
# file: sim/na_13_2_dead_condition.py
# tier: S
# verify: /opt/homebrew/bin/python3 sim/na_13_2_dead_condition.py
"""卷一 13.2 语义校验（S 层）：可满足性与死条件。
死条件 = 条件引用的状态量在到达该节点前不可能取到所需值。先沿对话图做「可达区间」
前向不动点（每节点每个好感度变量取整数区间 [lo, hi]；区间是过近似、不按条件剪枝，
故「过近似都说够不着」才是真死条件），再把每个条件位点与所在节点区间比对。flag /
item 叶子另按「是否被任何效果写过」判：从未被写的名字，条件恒假。
复用 sim/na_00_spec_check.py 的 load_spec。产出 out/narr13_dead_condition.json。
"""
from __future__ import annotations
import json
import os
import sys
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
import na_00_spec_check as base # noqa: E402 复用 load_spec
OUT = os.path.join(os.path.dirname(HERE), "out/narr13_dead_condition.json")
LO, HI = 0, 100
def clamp(v: int) -> int:
return LO if v < LO else HI if v > HI else v
def intervals(spec: dict):
"""对话图上的好感度区间前向不动点（过近似，忽略条件剪枝）。"""
vars_ = sorted(spec["state"]["vars"])
init = {v: next(c["affinity"]["init"] for c in spec["characters"] if c["id"] == v)
for v in vars_}
reach: dict = {n["id"]: None for n in spec["dialogue"]}
reach[spec["meta"]["start"]] = {v: [init[v], init[v]] for v in vars_}
changed, rounds = True, 0
while changed and rounds < 1000:
changed, rounds = False, rounds + 1
for n in spec["dialogue"]:
r = reach[n["id"]]
if r is None:
continue
for c in (n.get("choices") or []):
add = (c.get("effects") or {}).get("add") or {}
out = {v: [clamp(r[v][0] + add.get(v, 0)), clamp(r[v][1] + add.get(v, 0))]
for v in vars_}
cur = reach.get(c["goto"])
if cur is None:
reach[c["goto"]] = out
changed = True
else:
for v in vars_:
nl, nh = min(cur[v][0], out[v][0]), max(cur[v][1], out[v][1])
if [nl, nh] != cur[v]:
cur[v] = [nl, nh]
changed = True
return reach, rounds
def aff_dead(c, iv: list) -> bool:
lo, hi = iv
return {"<": lo >= c[3], ">=": hi < c[3], "==": not (lo <= c[3] <= hi),
"!=": lo == hi == c[3]}[c[2]]
def dead(c, iv_of, wflag: set, witem: set) -> bool:
"""c 是否可证明永不可满足（过近似口径，宁可漏报不误报）。"""
if not c:
return False
k = c[0]
if k == "flag":
return c[2] == 1 and c[1] not in wflag
if k == "item":
return c[2] == 1 and c[1] not in witem
if k == "aff":
return aff_dead(c, iv_of(c[1]))
if k == "and":
return dead(c[1], iv_of, wflag, witem) or dead(c[2], iv_of, wflag, witem)
if k == "or":
return dead(c[1], iv_of, wflag, witem) and dead(c[2], iv_of, wflag, witem)
return False # not 保守不判
def sites_of(spec: dict, reach: dict, bounds: dict) -> list:
"""摊平全部条件位点：(出处, 条件, 区间作用域)。"""
out = []
for n in spec["dialogue"]:
scope = reach[n["id"]] or bounds
if n.get("line_when"):
out.append((f"{n['id']}.line_when", n["line_when"], scope))
for c in (n.get("choices") or []):
if c.get("when"):
out.append((f"{n['id']}/{c['id']}", c["when"], scope))
for e in spec["endings"]:
if e.get("when"):
out.append((f"ending {e['id']}", e["when"], bounds))
for e in spec["scene_graph"]["edges"]:
if e.get("when"):
out.append((f"edge {e['from']}->{e['to']}", e["when"], bounds))
for loc in spec["world"]["locations"]:
if loc.get("unlock_when"):
out.append((f"location {loc['id']}", loc["unlock_when"], bounds))
return out
def main() -> int:
spec = base.load_spec()
vars_ = sorted(spec["state"]["vars"])
reach, rounds = intervals(spec)
bounds = {v: [min(r[v][0] for r in reach.values() if r),
max(r[v][1] for r in reach.values() if r)] for v in vars_}
wflag, witem = set(), set()
for n in spec["dialogue"]:
for c in (n.get("choices") or []):
eff = c.get("effects") or {}
wflag |= set(eff.get("set") or {})
witem |= set(eff.get("grant") or {})
sites = sites_of(spec, reach, bounds)
deads = [w for w, c, scope in sites if dead(c, lambda v, s=scope: s[v], wflag, witem)]
report = {"ok": not deads, "dead_conditions": deads, "condition_sites": len(sites),
"fixpoint_rounds": rounds, "reachable_bounds": bounds,
"written_flags": len(wflag), "written_items": len(witem)}
os.makedirs(os.path.dirname(OUT), exist_ok=True)
with open(OUT, "w", encoding="utf-8") as fh:
json.dump(report, fh, ensure_ascii=False, indent=2)
fh.write("\n")
print(f"对话图前向区间不动点：{rounds} 轮收敛")
print("可达区间（过近似，全图并集）：")
for v in vars_:
print(f" {v}: [{bounds[v][0]}, {bounds[v][1]}]")
print(f"条件位点 {len(sites)} 个（选项 / 台词 / 结局 / 场景边 / 地点解锁）")
print(f"被写过的 flag {len(wflag)} 个 / item {len(witem)} 个")
print(f"死条件 {len(deads)} 个：{deads}")
if deads:
for d in deads:
print(f"FAIL {d}")
return 1
print("OK na_13_2_dead_condition：全部条件位点均可满足")
return 0
if __name__ == "__main__":
sys.exit(main())
本机实跑 /opt/homebrew/bin/python3 sim/na_13_2_dead_condition.py：
对话图前向区间不动点：2 轮收敛
可达区间（过近似，全图并集）：
hui: [10, 97]
mu: [25, 100]
shen: [40, 100]
yan: [0, 100]
条件位点 52 个（选项 / 台词 / 结局 / 场景边 / 地点解锁）
被写过的 flag 18 个 / item 9 个
死条件 0 个：[]
OK na_13_2_dead_condition：全部条件位点均可满足
曾经有过的四个死条件
当前规格 0 个死条件，但这个检测器抓到过 4 个真实死条件，它们在规格定稿前被逐个修掉。如实记下来，比只报一个「0」有用得多：
| 位点 | 当时的症状 | 修法 |
|---|---|---|
d_chapel_2/c_chapel_2c | 要求 shen >= 55，但到该节点 shen 最多只到 50 | 在 c_chapel_1a 补 shen +5，把可达上界抬到 55 |
d_lb_2/c_lb_2c | 要求 yan >= 40，但到该节点 yan 最多只到 35 | 阈值 40 下调到 30 |
d_tc_1/c_tc_1c | 要求 fog_glass，而该物品只在洞窟之后的鱼市街才给 | 引用改为 tide_table（第一夜即可获得） |
d_mr_1/c_mr_1c | 要求 cave_explored，而该旗标只在洞窟里才置位 | 引用改为 knows_bell_legend（进鱼市街前可得） |
四条归成两类成因：前两条是阈值不可达——条件本身没问题，是数值抬得比可达上界还高；后两条是顺序倒置——引用的状态量在到达该位点之前根本还没产生。两类都会被同一个区间检测器抓到：阈值不可达表现为阈值落在区间外，顺序倒置表现为该变量在该节点处区间仍是「未产生」（对 flag / item 即从未被写过）。
P 层：边界与负例
P 层用 TypeScript 重写同一个检测器（intervals 与 Python 同算法），先对真实规格断言 0 死条件，再用边界与注入负例证明检测器会开火。下面给出可直接保存的完整文件 core/test/na_13_2_dead_condition.test.ts，包含区间传播和写入集合构造，避免只复制断言时缺少辅助函数。
// file: core/test/na_13_2_dead_condition.test.ts
// tier: P
// verify: node --test 'core/test/na_13_2_dead_condition.test.ts'
// 卷一 13.2：死条件检测器 —— 求每个状态量的可达区间，再与条件比对。区间是过近似
// （不按条件剪枝），所以「过近似都说够不着」才是真死条件，检测器不会误报。
import test from "node:test";
import assert from "node:assert/strict";
import { readFileSync } from "node:fs";
import { join, dirname } from "node:path";
import { fileURLToPath } from "node:url";
type Cond = unknown[] | null;
type Choice = { id: string; goto: string; when?: Cond; effects?: { add?: Record<string, number>; set?: Record<string, number>; grant?: Record<string, number> } };
type DNode = { id: string; choices?: Choice[]; line_when?: Cond };
type Spec = {
meta: { start: string };
state: { vars: string[] };
characters: { id: string; affinity: { init: number } }[];
dialogue: DNode[];
};
type Iv = [number, number];
const clamp = (x: number): number => (x < 0 ? 0 : x > 100 ? 100 : x);
/** 对话图上的好感度区间前向不动点（过近似，忽略条件剪枝）。 */
function intervals(spec: Spec): Map<string, Record<string, Iv>> {
const vars = [...spec.state.vars].sort();
const init: Record<string, number> = {};
for (const v of vars) init[v] = spec.characters.find((c) => c.id === v)?.affinity.init ?? 0;
const at = (): Record<string, Iv> => {
const o: Record<string, Iv> = {};
for (const v of vars) o[v] = [init[v], init[v]];
return o;
};
const reach = new Map<string, Record<string, Iv>>();
reach.set(spec.meta.start, at());
let changed = true;
while (changed) {
changed = false;
for (const n of spec.dialogue) {
const r = reach.get(n.id);
if (!r) continue;
for (const c of n.choices ?? []) {
const add = c.effects?.add ?? {};
const out: Record<string, Iv> = {};
for (const v of vars) out[v] = [clamp(r[v][0] + (add[v] ?? 0)), clamp(r[v][1] + (add[v] ?? 0))];
const cur = reach.get(c.goto);
if (!cur) {
reach.set(c.goto, out);
changed = true;
} else {
for (const v of vars) {
const nl = Math.min(cur[v][0], out[v][0]);
const nh = Math.max(cur[v][1], out[v][1]);
if (nl !== cur[v][0] || nh !== cur[v][1]) {
cur[v] = [nl, nh];
changed = true;
}
}
}
}
}
}
return reach;
}
function affDead(c: unknown[], [lo, hi]: Iv): boolean {
const op = c[2] as string;
const t = c[3] as number;
if (op === ">=") return hi < t;
if (op === "<") return lo >= t;
if (op === "==") return !(lo <= t && t <= hi);
return lo === hi && lo === t; // !=
}
function dead(c: Cond, ivOf: (v: string) => Iv, written: Set<string>): boolean {
if (!c) return false;
const k = c[0] as string;
if (k === "flag" || k === "item") return (c[2] as number) === 1 && !written.has(c[1] as string);
if (k === "aff") return affDead(c, ivOf(c[1] as string));
if (k === "and") return dead(c[1] as Cond, ivOf, written) || dead(c[2] as Cond, ivOf, written);
if (k === "or") return dead(c[1] as Cond, ivOf, written) && dead(c[2] as Cond, ivOf, written);
return false;
}
const HERE = dirname(fileURLToPath(import.meta.url));
const spec = JSON.parse(readFileSync(join(HERE, "../../config/story_spec.json"), "utf8")) as Spec;
const reach = intervals(spec);
const written = new Set<string>();
for (const n of spec.dialogue) {
for (const c of n.choices ?? []) {
for (const k of Object.keys(c.effects?.add ?? {})) written.add(k);
for (const k of Object.keys(c.effects?.set ?? {})) written.add(k);
for (const k of Object.keys(c.effects?.grant ?? {})) written.add(k);
}
}
const ivAt = (node: string, v: string): Iv => reach.get(node)?.[v] ?? [0, 100];
test("真实规格：对话层 36 个条件位点无一为死条件", () => {
let sites = 0;
let deadCount = 0;
for (const n of spec.dialogue) {
if (n.line_when) { sites += 1; if (dead(n.line_when, (v) => ivAt(n.id, v), written)) deadCount += 1; }
for (const c of n.choices ?? []) {
if (c.when) { sites += 1; if (dead(c.when, (v) => ivAt(n.id, v), written)) deadCount += 1; }
}
}
assert.equal(deadCount, 0);
assert.equal(sites, 36);
console.log(`对话层条件位点 ${sites} 个，死条件 ${deadCount} 个`);
});
test("边界：chapel_2c 的 shen 上界 55 —— 55 活 / 56 死", () => {
const iv = ivAt("d_chapel_2", "shen");
assert.deepEqual(iv, [45, 55]);
assert.equal(affDead(["aff", "shen", ">=", 55], iv), false);
assert.equal(affDead(["aff", "shen", ">=", 56], iv), true);
});
test("负例一 · 阈值越界：yan ≥ 999 被证否", () => {
assert.equal(affDead(["aff", "yan", ">=", 999], ivAt("d_lt_3", "yan")), true);
});
test("负例二 · 名字从未被写：不存在的 flag 被证否", () => {
assert.equal(dead(["flag", "never_written_flag", 1], (v) => ivAt("d_pier_1", v), written), true);
assert.equal(dead(["flag", "knows_yan_missing", 1], (v) => ivAt("d_pier_1", v), written), false);
});
test("负例三 · and 一个合取项死则整体死", () => {
const c: Cond = ["and", ["flag", "knows_yan_missing", 1], ["aff", "yan", ">=", 999]];
assert.equal(dead(c, (v) => ivAt("d_dq_2", v), written), true);
});
本机实跑 node --test 'core/test/na_13_2_dead_condition.test.ts'：
对话层条件位点 36 个，死条件 0 个
✔ 真实规格：对话层 36 个条件位点无一为死条件 (1.308333ms)
✔ 边界：chapel_2c 的 shen 上界 55 —— 55 活 / 56 死 (0.479333ms)
✔ 负例一 · 阈值越界：yan ≥ 999 被证否 (0.064875ms)
✔ 负例二 · 名字从未被写：不存在的 flag 被证否 (0.064667ms)
✔ 负例三 · and 一个合取项死则整体死 (0.298875ms)
ℹ tests 5
ℹ suites 0
ℹ pass 5
ℹ fail 0
ℹ cancelled 0
ℹ skipped 0
ℹ todo 0
ℹ duration_ms 1193.784917
判读：三条读数
第一，当前 0 个死条件。 52 个条件位点（对话层 36 个 + 结局 4 个 + 场景边 5 个 + 地点 7 个）全部可满足。不动点 2 轮就收敛——因为对话图几乎是单向的，区间传播一遍就基本到位，第二轮只做确认。
第二，过近似的取舍是可辩护的。 全图并集给出的可达区间是 yan [0,100]、hui [10,97]、shen [40,100]、mu [25,100]。这些比真实可达状态里的上下界宽（真实值要枚举状态空间才知道，那是卷二 ch5 的事），宽出来的部分正是「漏报的风险」。宁可漏报不误报：校验器一旦误报，使用者就会开始忽略它。
第三，chapel_2c 的边界说明检测器有分辨率。 shen 在 d_chapel_2 的区间上界恰好是 55，阈值 55 活、56 死。这个边界不是凑出来的——它正是当年那条死条件被修好之后留下的痕迹：修法把上界抬到了 55，于是阈值 55 从「死」翻成「活」。检测器能分辨出这一格的差别，说明它不是把所有东西都判成活的。
自检表
| 检查项 | 合格标准 |
|---|---|
| 死条件可证否 | 只在「过近似都说够不着」时判死，不依赖路径枚举 |
| 区间必然收敛 | 上下界被 [0,100] 夹住，单调不减，有限轮不动点 |
| flag / item 有独立判据 | 从未被写的名字，条件恒假，不走区间 |
| 组合条件保守 | and 有一项死即死，or 需两项皆死，not 不判 |
| 边界可分辨 | 检测器能区分「刚好够」与「差一格」，不是全判活 |
结构（13.1）问「接不接得上」，语义（13.2）问「成不成立」，两者都建立在「声明的东西和实际用的东西对得上」这个前提上。下一节把这个前提本身拿出来检查：一致性校验，看声明域与使用域的差集。
阅读导航：上一节：13.1 结构校验：孤儿节点与断链 · 下一节：13.3 一致性校验 。
继续阅读
探索更多技术文章
浏览归档，发现更多关于系统设计、工具链和工程实践的内容。