如何解决UPPAAL 上的反例枚举
下午好,我正在用 UPPAAL 模型检查器做一些实验,我的理解是,当一个属性未被验证时,验证引擎 (verifyta) 只能找到以下一个:
- 踪迹
- 最短跟踪(转换次数)
- Quickset Trace(具有最短相对时间的跟踪)。
如果我们认为模型检查侧重于健全性而不是完整性,并且至少存在一条违反特定属性的痕迹意味着该属性不满足这一事实,那么这很有意义。
但是,在我的应用程序上下文中,我需要找到多个反例来分析它们的结构等。就此而言,我想知道是否存在推断 ALL 的可能性在给定有界搜索空间(即限制搜索图的深度)的情况下,违反 TCTL 中定义的特定属性的可能轨迹。此外,如果 UPPAAL 不提供此机会,您能否向我指出可能已实现它的其他工具?
非常感谢!
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。