软件建模32：模型校验与业务约束
一个状态模型可以是合法JSON，所有引用都能找到，每个操作也只有一个目标，却仍然允许退役设备恢复在役。错误没有藏在逗号或类型里，而是模型选择的业务规则与既定合同不同。把所有检查统称为“模型合法”，会掩盖已经证明和仍未证明的部分。
受限模型转换 已经执行模型到代码的转换。本篇在转换输入之前区分语法结构、通用状态机语义和设备业务合同，并用实际可执行的错误策略检验这三层。另以租期和设备引用说明，模型约束与实例数据约束也有不同对象。解析成功只排除了一类问题
JSON首先提供一种数据表示方式。states 写成字符串仍可能通过JSON解析，但当前语言要求它是标识符数组；迁移少了目标字段也没有形成完整模型。结构检查必须落实到选定语言的字段、类型、版本和标识符规则。
本章先完整执行 validate_structure，检查对象字段集合、数组形状及每条迁移的三个字段。它也拒绝重复JSON键和非标准数值常量，这是本工具的严格输入政策。不能因为常见解析器恰好保留最后一个同名键，就把含混输入当作确定模型。
flowchart TD
I[输入模型文本] --> S[语法与完整结构检查]
S -->|PASS| F[第30篇通用FSM校验]
F -->|PASS| B[第24篇设备合同校验]
B -->|PASS| A[当前模型可进入后续生成]
S -->|FAIL| X[后续 NOT_RUN]
F -->|FAIL| Y[业务层 NOT_RUN]
B -->|FAIL| Z[结构合法但业务不匹配]这里没有单凭错误码猜测前一层通过。第30篇解析器会在不同位置检查结构和语义；若一条边引用未知状态，另一条边又把目标写成数字，只看第一个异常不能证明所有结构都正确。新增前置扫描完整检查结构，再进入原解析器，实验专门保留这个混合错误反例。
诊断结果为每层记录 PASS、FAIL 或 NOT_RUN。输入连结构都不满足时，业务合同一栏是未运行，不能记成通过或失败。错误同时携带代码和路径，让调用者知道应该修改状态引用、字段类型还是领域约定。
路径提供的是当前输入位置，并不保证业务原因只有一个。例如首条未知引用被修复后，下一次可能继续暴露第二处问题。当前工具明确采用首错停止，后续阶段没有执行就不下结论；它没有收集全量诊断，也不会自动替用户选择一个看似接近的状态名。
状态机语义仍然不认识设备
结构通过后，第30篇的 parse_model 检查名字唯一、引用存在、分派确定、初态可达和已声明终态没有出边。目标写为不存在的 GHOST 会失败；同一源状态和操作出现两条边，也会失败。
这些是当前有限状态语言的规则。它并不知道“退役”在租赁业务中意味着永久退出；一个叫 RETIRED 的字符串没有天然的不可逆性。终态由模型的 terminal 字段声明，不能仅凭英文名称赋予额外规则。
因此存在两种不同错误。保留终态声明又给退役状态加出边，会被通用语义层拒绝；先删除终态声明再加出边，则可以构成一台完全确定、引用完整的状态机。第二种修改正好适合检验业务校验是否独立存在。
实际运行一次错误的退役政策
本章自己的 models/32/wrong-policy.json 保留三个状态和原来的四条迁移，把终态列表置空，再添加“退役后验收通过回到在役”的第五条边。它与第30篇交换审批目标的错误样本不同，两份样本都继续参与检查。
程序先用通用解析器加载新样本，从待检执行退役，状态变成 RETIRED；再执行验收，实际返回 ACTIVE。日志中的这条轨迹不是人工写出的预期输出，而是连续调用状态机 step 的结果。
stateDiagram-v2
[*] --> INSPECTION_REQUIRED
INSPECTION_REQUIRED --> RETIRED: retire
RETIRED --> ACTIVE: approveInspection
note right of RETIRED
错误样本删除终态声明
通用状态机允许这条出边
设备合同要求在业务层拒绝
end note随后调用 validate_equipment_contract，得到 EQUIPMENT_CONTRACT 错误。三层报告依次是通过、通过、失败。该函数检查与第24篇设备生命周期子集严格相等，包括初态、终态、操作集合和允许边，因此不会被“语法都对”绕过。
严格相等也有代价。若业务确实批准增加报废审核状态，当前检查会把新模型拒绝，即使新流程有合理解释。正确处理方式是明确修订合同和验收样本，而不是删掉失败断言让新文件通过。校验器维护的是当前已选择的规则，不拥有决定未来业务政策的权力。
约束落在模型还是数据上
生命周期约束的对象是状态机定义；租期检查的对象则是一组具体预留记录。本章另提供 validate_reservations，逐条检查请求编号、设备引用、时间格式和活动标志，再检查同设备活跃区间是否重叠。
教学输入只接受UTC整秒时间，采用起点严格早于终点的半开区间。十点至十二点与十二点至十三点可以同时存在；把第二条改成十一点开始就会失败。这个输入范围比 Java Instant 更窄，不支持小数秒或本地时区，不能把它宣传为前文时间类型的完整替代。
引用存在与状态合法也不是同一个问题。设备字段写成有效字符串 GHOST，仍会因目录中没有这台设备而失败；设备存在，也不代表它在役或当前可出租。这里只验证给定集合中的引用，不查询设备仓储、维修系统或授权信息。
取消后的历史记录可以不再占用资源，但仍须有合法租期和有效设备引用。请求编号重复也会被拒绝，不能因为其中一条不活跃就允许两条记录使用同一身份。这些规则分别约束历史表达和当前占用，避免一个 active 标志关闭所有检查。
实验还覆盖反向区间、零长度、缺失时区、不存在的日期和错误布尔类型。数字一不会被接受为活动标志，布尔值也不能充当设备身份。检查器只返回或抛出错误，不改写输入；通过后原始数据与检查前相同。
OCL 可以表达约束，但本例没有运行它
OMG OCL 2.4将OCL定义为描述模型表达式的语言，表达式求值没有副作用。规范区分不变量、操作前置条件与后置条件，并将它们关联到具体上下文。原文，7.1、7.3.3—7.3.4节
在具有相应类型和关系的模型中，“租期起点早于终点”适合放在租期的不变量位置；“调用退役前尚未退役”适合描述操作前置条件；“调用后状态为退役”适合描述后置条件。表达式的意义依赖模型里确实存在的属性、操作和类型，不能脱离上下文抄一段语法就当作已验证规则。
本实验实际执行的是 Python条件判断、集合比较、图可达性检查和区间比较，没有加载OCL文本，也没有运行OCL解析器或求值器。因此日志只能证明这些Python机制识别了给定反例，不会写成“通过OCL验证”。
无副作用的校验同样不提供写入原子性。两份快照各自检查通过后，仍可能被两个并发调用同时写入；这与第25篇的先查后写反例相同。要保证运行时排他，约束必须在合适的一致性边界内落实，或者由存储机制承担相应保证。
三层都通过之后还缺什么
通过当前设备合同，只能说明有限模型对应那四条生命周期边。它没有检查身份相等、描述修改、金额计算、恢复授权和完整租赁用例，也没有证明业务人员认同这些约定。校验范围应随报告一起交付，不能被一个绿色总状态吞掉。
本章前置结构检查重复了第30篇格式中的一部分知识，这是为了得到完整分层诊断。若以后修改DSL版本，需要同时更新这层规则和回归样本；否则会出现语言已经接受新字段、报告入口却仍然拒绝的漂移。当前通过第30篇全部错误样本来约束这个维护边界。
运行时的数据检查还依赖输入快照是否完整。如果调用者只传来今天新建的两条记录，校验器看不到昨天已经承诺的同一租期，就无法判断与旧记录的冲突。通过的含义只能是给定集合内部满足这些约束；查询范围、隔离方式和写入时机必须由应用另行保证。
运行与错误定位
从仓库根目录执行 examples/software-modeling/labs/32/run.sh。本次 Python 3.14.4实跑38项检查并退出零；第30篇原入口也在临时副本中完成23项回归。原始输出位于 examples/software-modeling/evidence/32/，没有用生成页面代替实验日志。
执行 examples/software-modeling/labs/32/run.sh examples/software-modeling/models/32/wrong-policy.json 会打印三层报告并退出一，明确显示前两层通过、设备合同失败。校验接口与错误码定义在 examples/software-modeling/models/32/contracts.md，后续生成步骤可以据此决定是否接受输入，不能把退出一当作可忽略的提示。
