来自 verifyta 的跟踪格式与 libutap 库的跟踪实用程序不兼容

Question

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

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

详情：

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

clock x;
chan e;
...
system p1, p2;

进程p1和p2如下：

CTL 属性是：

$ cat p.ctl
A[]p1.idle

这是我对 verifyta 所做的：

$ verifyta --version
(Academic) UPPAAL 4.1.25-5 (rev. 643E9477AA51E17F), April 2021
$ verifyta -t0 -fp -Xp p.xml p.ctl
Options for the verification:
  Generating some trace
  Search order is breadth first
  Using conservative space optimisation
  Seed is 1638198789
  State space representation uses minimal constraint systems

Verifying formula 1 at p.ctl:1
 -- Formula is NOT satisfied.
Writing counter example to p-1.xtr

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

$ UPPAAL_COMPILE_ONLY=1 verifyta p.xml - > p.if
$ tracer p.if p-1.xtr
State: Expecting a line with '.' but got ' '

显然 verifyta 生成的跟踪格式不受 tracer 支持。

我也对 GUI 进行了完全相同的操作，并将跟踪保存在 p.xtr 中。这个得到 tracer:

的支持

$ tracer p.if p.xtr
State: p1.idle p2.idle t(0)-x<=0 x-t(0)<=5

Transition: p2.idle -> p2.run {1; e!; 1;} p1.idle -> p1.run {x >= 5; e?; 1;}

State: p1.run p2.run t(0)-x<=-5

这是两个跟踪文件：

p-1.xtr（来自verifyta）

0 0 
.
0 1 0
.
1 0 10
.
.

.
1 1 
.
0 1 -10
.
.

.
1 0 ; 0 0 ; .
.

p.xtr（来自 GUI）

0
0
.
0
1
0
.
1
0
10
.
.
.
1
1
.
0
1
-10
.
.
.
1 0 ;
0 0 ;
.
.

可以看出，内容非常相似，但格式不同，多了一些空行...

Answer 1

问题似乎出在由 verifyta:

生成的跟踪文件的某些行末尾的尾随空格

$ head -5 p-1.xtr | cat -E
0 0 $
.$
0 1 0$
.$
1 0 10$

作为一种快速修复，可以 post- 处理来自 verifyta:

的痕迹

$ sed -E 's/^\s*(.*[^[:space:]])\s*$//' p-1.xtr > p-1-fixed.xtr
$ tracer p.if p-1-fixed.xtr
State: p1.idle p2.idle t(0)-x<=0 x-t(0)<=5 

Transition: p2.idle -> p2.run {1; e!; 1;} p1.idle -> p1.run {x >= 5; e?; 1;} 

State: p1.run p2.run t(0)-x<=-5

更清晰的修复是 trim tracer 实用程序中的前导和尾随空格（刚刚提交了补丁）或修复 verifyta 中的跟踪生成。在 utap/src/tracer.cpp 中使用 boost 的修复示例：

$ git diff src/tracer.cpp
diff --git a/src/tracer.cpp b/src/tracer.cpp
index f0a4274..4c82e22 100644
--- a/src/tracer.cpp
+++ b/src/tracer.cpp
@@ -30,6 +30,7 @@
 #include <stdexcept>
 #include <string>
 #include <vector>
+#include <boost/algorithm/string/trim.hpp>
 
 /* This utility takes an UPPAAL model in the UPPAAL intermediate
  * format and a UPPAAL XTR trace file and prints trace to stdout in a
@@ -180,10 +181,11 @@ istream& readdot(istream& is)
 {
     string str;
     getline(is, str);
-    if (str.empty())
+    while (str.empty())
     {
         getline(is, str);
     }
+    boost::algorithm::trim(str);
     if (str != ".")
     {
         cerr << "Expecting a line with '.' but got '" << str << "'" << endl;

（我也把if (str.empty())改成了while (str.empty())，这样看起来更安全）

来自 verifyta 的跟踪格式与 libutap 库的跟踪实用程序不兼容

Trace format from verifyta not compatible with tracer utility of libutap library

uppaal

详情：