如何判断Uppaal模型是否可以识别指定的执行轨迹？

原生工具实现路径 #

• 直接构造TCTL查询校验
  拿到生成的轨迹后，将轨迹的节点信息（时间戳、触发动作、变量取值、所在位置）逐段转化为TCTL可达性查询条件。例如轨迹为「触发动作a → 延迟1.5个时间单位 → 触发动作b → 变量x取值为3」，对应查询可写为E<> (action_a == true && clock >= 1.5 && action_b == true && x == 3)，调用verifyta.exe执行该查询，若返回结果为满足，则说明目标模型可复现该轨迹。
• 使用Tron工具做一致性测试
  Tron本身支持输入测试序列做在线一致性校验，将指定轨迹按Tron要求的格式整理为输入序列，把待校验的相似模型配置为被测实现，运行测试后如果没有输出不一致、动作拒绝等异常结果，就说明轨迹可被模型复现。

自定义高灵活度方案 #

如果需要批量校验大量轨迹，推荐用观测器注入方案：

• 首先调整轨迹生成逻辑，执行simulate [<=n; 1] {clock, 所有状态变量, 位置ID, 触发动作}，导出完整结构化的轨迹信息，避免后续校验缺少必要维度。
• 为待校验的目标模型新增一个观测器自动机，观测器的迁移逻辑完全匹配待校验轨迹的每一步节点约束，只有当目标模型的状态完全匹配轨迹对应节点时，观测器才能推进到下一个状态。
• 新增TCTL查询E<> 观测器到达最终状态，调用verifyta.exe执行查询，返回真则说明轨迹可复现，可通过脚本批量完成轨迹解析、观测器注入、查询执行、结果解析的全流程。

额外优化建议 #

• 生成轨迹时可固定非必要的非确定性分支的取值，减少生成边界不可复现轨迹的概率，提升校验效率。
• 若轨迹包含紧急通道、committed位置等特殊语法，构造观测器或查询时需要额外同步这些特殊状态的约束，避免校验漏判。

内容的提问来源于stack exchange，提问作者Jaime Cuartas