问题标签 [uppaal]

我目前正在尝试使用 UPPAAL 自动化模型检查实验。当我计划运行数千个测试时，GUI 不是一个选项。所以我尝试使用verifyta（版本（学术）UPPAAL 4.1.25-5（rev. 643E9477AA51E17F），2021 年 4 月）进行模型检查并生成反例跟踪，以及库中的tracer实用程序libutap（版本 0.94，3 月 20 日， 2019）以人类可读的形式转换痕迹。

显然，由 UPPAAL GUI 生成的相同跟踪verifyta不支持由生成的跟踪格式。tracer我究竟做错了什么？这是一个已知的问题？

细节：

对于我的第一个实验，我设计了一个非常简单的系统和一个非常简单的查询：

p1与流程p2如下：

CTL 属性为：

这是我所做的verifyta：

到目前为止，一切都很好。为了检查检查器，我现在想获得一个人类可读的反例跟踪，所以我使用了该tracer实用程序：

显然，由 生成的跟踪格式verifyta不受tracer.

我也对 GUI 做了同样的事情，并将跟踪保存在p.xtr. 这个支持tracer：

这是两个跟踪文件：

p-1.xtr（来自verifyta）

p.xtr（来自图形用户界面）

如您所见，内容非常相似，但格式不同，额外的空行......

有人可以花几句话向不是来自正式方法背景的人解释一下，当搜索有时间限制时，使用符号模型检查验证规范和使用具体模型检查验证规范有什么区别？我指的是 UPPAAL 中对 SMC 和 Concrete MC 的定义。

特别是，我编写了一个程序，它使用 UPPAAL Java API 来验证针对定时自动机网络的查询。如果查询被验证，UPPAAL 返回一个符号跟踪来解析，如果不是，则返回其他东西。如果验证时间太长，我决定停止验证过程，返回一条消息并继续下一个查询以进行验证。到目前为止一切都很好。

最近，我一直在玩 UPPAAL Stratego，它本机提供了选择最大时间或探索深度来限制搜索的可能性。但是，只有在使用具体模型检查执行验证时才能应用此选项。

我的问题是：停止符号验证过程有什么区别，就像我在我的 Java 程序中所做的那样，以及 UPPAAL Stratego 本身是做什么的？在这两种情况下，我都没有得到答案（或踪迹），但是探索的“可靠性”呢？

这两个选项之间哪个更好（即更完整）？停止符号验证还是停止具体验证？

到目前为止，我的理解是，在符号模型检查中，可能的状态是通过使用变量间隔来定义的，而在具体模型检查中，变量假设一个实际值。我的观点是，就“完整性”而言，在一段时间后停止 SMC 更“完整”，因为状态空间的探索是使用 BFS 或 DFS 算法系统地发生的，如果我使用 BFS，我可以“确定”在 N 步内没有任何不好的事情发生。但同样，我在模型检查方面的背景并不丰富，所以我可能完全搞错了。

此外，如果可以放弃对策略的任何引用，将不胜感激。

谢谢！

在Uppaal，有没有办法知道有多少状态存在作为位置和变量的组合