同一个预留请求被取消以后，系统仍能返回它最初的处理结果。这条约定要求保留两份用途不同的数据：当前占用设备的预留，以及记住原请求结果的回执。只画“客户提交、系统处理、返回结果”，看不出取消究竟删掉哪一份数据；直接画数据库表，又容易跳过这些数据从哪里来、由谁产生的问题。

数据流图适合检查这种信息关系。它把系统视为接收数据、转换数据和产生数据的过程，再逐层展开过程内部的组成。画图的目标是发现遗漏的输入、来源不明的输出和说不清含义的数据名。图本身不负责证明程序执行顺序，也不能证明两次并发预留不会同时成功。

本篇承接场景、用例与规则，继续使用单实例、单线程的设备租赁教学案例。客户、合同和结算属于系列背景，当前边界只覆盖指定设备预留、重复请求与取消。这里没有企业访谈，也没有从现实业务推导出一套未经确认的流程。

先固定系统边界

外部角色取“租赁经办角色”，表示提交请求的调用方。它可以由网页、命令行或另一段程序承担，图里不决定界面形态。设备不是外部参与者：设备标识是请求中的数据，设备本身不会调用这个基线。维修平台尚未接入，因此也不为了让图看起来完整而添加一条维修通知。

上下文图把整个租赁预留系统表示为一个过程。输入有预留请求和取消请求，输出分别是预留结果和取消结果。本文约定圆角节点表示过程，矩形表示外部角色，圆柱表示数据存储；使用 Mermaid 的现成形状，是基础 DFD 语义的教学表达，不声称采用完整的某套标准符号。

flowchart LR
  Clerk["租赁经办角色"]
  System(["0 租赁预留系统"])
  Clerk -->|reserve_request| System
  System -->|reserve_result| Clerk
  Clerk -->|cancel_request| System
  System -->|cancel_result| Clerk

箭头上的名字表示数据，不表示“然后执行”。预留请求包括请求标识、设备标识和租期，取消请求只包含请求标识。两条请求流分别对应现有的 reserve 与 cancel，并不表示每个预留都会自动紧接着取消，也不表示它们部署在不同服务中。

工具作者 Excel Software 的说明把上下文图、过程分解、数据字典与层间平衡放在同一个模型中。父图出现的输入输出应能在子图中对应；如果拆分数据流，需要用字典解释组成关系。本篇只实现名称完全相同的边界核对，暂不实现组合流展开。Process Model

把系统拆成两个过程

第一层分解保留同一个外部角色，将系统展开为“处理预留”和“处理取消”。回执存储记录已经处理过的合法请求及其原结果；有效预留存储记录当前仍占用设备的请求。它们对应基线里的两个内存映射，并不意味着必须建立两张数据库表，更没有要求拆成两个服务。

flowchart LR
  Bookings[("有效预留")]
  Clerk["租赁经办角色"]
  P1(["1 处理预留"])
  P2(["2 处理取消"])
  Receipts[("请求回执")]
  Clerk -->|reserve_request| P1
  P1 -->|reserve_result| Clerk
  Clerk -->|cancel_request| P2
  P2 -->|cancel_result| Clerk
  Receipts -->|receipt_records| P1
  P1 -->|receipt_records| Receipts
  Bookings -->|booking_records| P1
  P1 -->|booking_records| Bookings
  Bookings -->|booking_records| P2
  P2 -->|release_record| Bookings

“处理取消”没有通向回执存储的写入流。这对应一个具体决定：取消释放当前预留，保留最初结果。release_record 是携带请求标识的删除依据；存储到取消过程的箭头表示所处理的当前预留信息，不能据此推断实现必须先查一次再删一次。Java 实现用一次 remove 的返回值判定是否真的释放了记录。

分解还暴露了一个值得检查的反例。如果取消过程直接删除回执，旧请求重放时就无法被识别为已处理请求，它可能重新占位。图中保留两类存储并限制取消过程的数据关系，使这个问题在写数据库映射之前就能讨论。是否实际守住了约定，仍要由行为测试判断。

这里也没有把“校验”“冲突判断”“保存结果”全部拆成节点。进一步分解只有在信息来源难以解释时才有收益。当前过程说明已经足以描述这三步，再增加节点会把判断条件误画成数据，或让图重复一份程序流程。

数据字典要能解释每条线

同一个“结果”可能指初次处理的结果、当前资源状态，或一次取消是否实际生效。这些含义不能共用一个未定义的名字。字典采用 + 表示字段组合，| 表示候选形式，花括号表示零至多条记录；这套记法只用于本篇，不作为可直接执行的类型系统。

数据流	组成与解释
`reserve_request`	请求标识 + 设备标识 + 开始时刻 + 结束时刻
`reserve_result`	`CONFIRMED`、`OVERLAP_REJECTED` 或非法输入异常
`cancel_request`	请求标识
`cancel_result`	是否释放有效预留，或非法输入异常
`receipt_records`	请求字段 + 最初结果的记录集合
`booking_records`	当前有效请求及其设备、租期的记录集合
`release_record`	待移除预留的请求标识

请求标识必须非空白；租期采用 [start,end)，要求开始早于结束。这里的时刻对应 Java Instant，没有把一天等同于固定数量的计费时长。invalid_input 是模型中的异常分支名称，实际实现抛出异常，并没有为 Outcome 增加第三个枚举值。字典保留这条区分，避免图与接口悄悄产生两个版本。

两个结果流也不能合并成“成功失败”。取消未知请求返回 false，重复取消也返回 false；预留冲突返回 OVERLAP_REJECTED，并保留拒绝回执。取消后的旧预留请求仍返回原 CONFIRMED，这只是在重放原结果，不证明当前设备仍被占用。需要查询当前占用时，应增加明确的查询契约。

数据字典完整也不等于业务信息充分。当前取消请求没有操作者身份，因此无法回答谁有权取消。把一条“权限校验通过”箭头加进图里不能弥补缺失的身份来源；必须先修改场景和输入契约，再修改图与实现。

用反例检查父子图是否平衡

层间平衡按边界核对。上下文图的两条输入、两条输出，应在分解图的边缘逐一出现；内部新增六条存储相关流不会构成外部接口变化。把所有箭头简单相加并比较总数会误报，因此检查器只取一端在系统外、一端在系统内的流。

工程中的 models/02/dfd.json 同时保存节点种类、父子图、数据字典。labs/02/check.py 把每条边界流规范化成“方向、外部角色、数据名”，用 Counter 比较两个多重集合。保留重复次数，是为了让重复画出的取消结果也被发现；普通集合会把重复流悄悄合并。

1	`sh examples/software-modeling/labs/02/run.sh`

可下载本篇模型、脚本与验证记录，解压后在解压目录执行同一命令。本次执行返回退出码 0，原始输出保存在 examples/software-modeling/evidence/02/output.txt，其中包含：

PASS balanced_boundary: 2 inputs, 2 outputs, 10 detail flows
PASS rejects_missing_output: boundary imbalance
PASS rejects_duplicate_output: boundary imbalance
PASS rejects_undefined_flow: undefined flow
PASS rejects_store_bypass: flow bypasses process
PASS diagram_source_matches_model

负例由脚本复制正式模型后主动修改：删除取消结果、重复该结果、删除一个字典定义，以及让外部角色直接连到数据存储。每个负例必须触发预期拒绝，才能算检查通过。最后一项比较 .mmd 与模型生成文本，防止图源遗漏边；它没有证明自然语言字段定义正确，也没有进行任何租赁 API 调用。

如果父图使用“租赁请求”这一组合流，子图拆成预留请求和取消请求，当前检查器会拒绝。这是实现范围限制。确实需要这种表达时，应先定义组合流包含关系，再扩展规范化规则，不能通过统一改名绕过语义差异。

从资料、模型到实现

来源	本篇模型决定	实现与证据位置
00 的 S00-01、S00-02	预留转换产生确认或冲突结果	`RentalDesk.reserve`；本篇仅表示信息来源
00 的 S00-04、S00-05	原请求字段与结果一起进入回执	`receipts` 和 `request.equals`
00 的 S00-06、S00-07	取消过程只修改有效预留	`RentalDesk.cancel`、`bookings.remove`
工具作者的分解与平衡说明	父子图边界数据守恒	`labs/02/check.py` 正例及四个负例

这张映射区分方法出处与租赁规则出处。工具说明支持如何检查图，不能证明客户真的允许随时取消；租赁约定来自系列的合成需求。当前程序对取消截止时间、认证、重启恢复都没有承诺，图也不补写这些能力。

一个变化可以检验模型是否有用：新增“查询当前有效预留”。父图需要查询请求与查询结果，子图需要从有效预留存储取数据的过程，字典需要定义返回的范围与字段。只给子图补上查询而忘记父图，平衡检查就会失败；把查询结果错误地取自历史回执，检查器可能通过，场景走查仍会发现取消后的记录被误当成有效预留。

如果系统只有一个输入、一种结果，也没有容易混淆的历史状态，一张输入输出表加过程说明通常就够了。当前案例保留 DFD 的原因，是取消与重试共同使用两类状态，图能直接呈现它们的不同去向。至于同一设备为何能关联多条请求、哪些关联可以不存在，则需要关系与基数模型进一步表达。

参考资料

Excel Software：Process Model，核对上下文图、分解、字典与平衡；采用基础数据流语义，不采用其控制流扩展。
示例模型：examples/software-modeling/models/02/；完整实验：examples/software-modeling/labs/02/check.py；命令、输出、退出码：examples/software-modeling/evidence/02/。