01 / COMPARE THE CHECKS
绿色仅代表一条路径
标准跟踪系统沿已完成表单的路径运行并报告 COMPLIANT。状态探索则探寻是否存在另一条可能失效的可达分支。在同一套人工编写的表单后模型上，它报告 NON-COMPLIANT （不符合已配置规则）。
这两个结果回答了不同的问题。基准测试表明其选定的路径通过了；但对于在调查前偏离该路径的通知，它没有提供任何信息。
录制演练内部细节
审视路径，而非仅看判定结论
这些界面来自所提供的合成工作流。首先查看基准的绿色通过结果，然后追踪它从未检查过的分支。每张图片均可全屏打开。
02 / FIND THE BRANCH
二级表单即为分叉点
在状态图中，建模的通知从 Messages Submitted 转移至 Secondary Form Requested。完成表单将继续走向路由和调查。而超时则会到达 Closed Incomplete。检验器在该输入模型中探索了 93 个可达状态，并发现 4 项配置属性未通过。
03 / INSPECT THE WITNESS
执行轨迹为审查人员提供了质询的路径依据
未通过的属性会附带一个有序的反例。在此处，建模序列记录了第 0 天的提交、第 1 天请求二级表单以及第 6 天超时关闭。在该路径上，通知从未到达调查阶段。
- Day 0: 建模的账单错误通知已提交。
- Day 1: 工作流请求二级表单。
- Day 6: 超时将案件转移至 ClosedIncomplete，且从该状态起无任何调查路径。
04 / CHECK THE CHANGE
为未完成表单重新规划路由
独立的修复模型将未完成表单的通知送入路由和调查，而不是将其关闭。随着该路径的更改，所有 4 项配置属性均为 PROVEN ，覆盖 153 个可达状态。该结论属于所提供的有限模型及其编码属性。
A SECOND WORKFLOW / TIMING
批处理延迟具有不同的失效形态
夜间批处理示例测试了在另一个独立合成模型中编码的条件性临时贷记假设。其中一条路径在第 14 个营业日才首次记入建模的贷记金额，超出了该模型的 10 个营业日限制。检验器在 79 个可达状态中，从 7 项配置属性里返回了一个反例。实际的 Reg E 例外情况和适用期限需要单独审查。
