下午好，我正在用 UPPAAL 模型检查器做一些实验，我的理解是，当一个属性没有被验证时，验证引擎（verifyta）只能找到以下之一：
- 痕迹
- 最短轨迹（转换次数）
- Quickset Trace（具有最短相对时间的跟踪）。
这很有意义，如果我们认为模型检查关注的是健全性而不是完整性，并且至少存在一个违反特定属性的迹线这一事实意味着该属性不满足。
然而，在我的应用程序的上下文中，我需要找到多个反例来分析它们的结构等。在这个程度上，我想知道是否存在推断违反 TCTL 中定义的特定属性的所有可能跟踪的可能性，给定一个有界搜索空间（即限制搜索图的深度）。此外，如果 UPPAAL 不提供这个机会，您能否指出可能已经实现它的其他工具？
非常感谢！