0

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

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

细节：

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

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

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（来自图形用户界面）

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

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

4

1 回答 1

1

问题似乎来自生成的跟踪文件的某些行末尾的尾随空格verifyta：

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

作为一种快速修复，可以对来自以下的跟踪进行后处理verifyta：

$ sed -E 's/^\s*(.*[^[:space:]])\s*$/\1/' 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

一个更干净的修复方法是修剪实用程序中的前导和尾随空格tracer（刚刚提交了一个补丁）或修复verifyta. boost使用in修复的示例utap/src/tracer.cpp：

$ 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())，看起来更安全）。

于 2021-12-01T14:59:03.470 回答