UPPAAL能否获取所有反例？如何获取全部符号轨迹反例？

UPPAAL支持获取多个反例，但不会自动一次性枚举全部，需要通过以下两种方式逐步获取：

方式1：用反例查看器的「下一个反例」按钮 #

当验证A[] not Automata.locationA失败并拿到第一个反例后：

• 点击验证结果里的「Trace」按钮打开反例窗口
• 在窗口工具栏里找到Next Counterexample（图标是向右箭头，也可能藏在菜单选项里）
• 反复点击这个按钮就能依次获取不同的反例，直到按钮变灰，说明没有新的反例可返回

方式2：修改属性查询，排除已找到的反例 #

如果需要精准筛选未发现的反例，可以通过修改属性排除已有轨迹的约束：

1. 先记下第一个反例里的关键特征，比如特定变量取值、状态跳转路径
2. 在原属性基础上添加排除条件，比如第一个反例里存在x=3且经过Automata.locationB，新属性可以写为：

   A[] not (Automata.locationA or (x=3 and Automata.locationB))
   

3. 重新运行验证，若属性仍不满足，就能得到不包含之前约束的新反例
4. 重复这个过程，直到验证结果显示「满足」，说明所有能触发Automata.locationA的路径都已找到

注意点 #

• UPPAAL的符号反例基于状态空间的符号化表达，部分看似不同的反例可能属于同一等价类
• 复杂模型枚举所有反例会消耗大量资源，建议只获取对调试有实际帮助的关键反例即可

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