Search code examples
uppaal

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

I am currently trying to automate model checking experiments with UPPAAL. As I plan to run thousands of tests the GUI is not an option. So I tried to use verifyta (version (Academic) UPPAAL 4.1.25-5 (rev. 643E9477AA51E17F), April 2021) to model-check and to produce counter-example traces, and the tracer utility from the libutap library (Version 0.94, March 20th, 2019) to convert the traces in human-readable form.

Apparently the trace format generated by verifyta is not supported by tracer while the same traces generated from the UPPAAL GUI are. What am I doing wrong? Is this a known issue?

The details:

For my first experiment I designed a very simple system and a very simple query:

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

With processes p1 and p2 as follows:

p1 and p2 processes

The CTL property is:

$ cat p.ctl
A[]p1.idle

Here is what I did with 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

So far so good. In order to check the checker I'd now like to get a human-readable counter-example trace, so I used the tracer utility:

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

Apparently the trace format generated by verifyta is not supported by tracer.

I also did exactly the same with the GUI and saved the trace in p.xtr. This one is supported by 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

Here are the two trace files:

p-1.xtr (from verifyta)

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

.
1 1 
.
0 1 -10
.
.

.
1 0 ; 0 0 ; .
.

p.xtr (from GUI)

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

As one can see, the contents are very similar but with a different formatting, extra empty lines...

Solution

  • The issue seems to come from trailing spaces at the end of some lines of the trace files generated by verifyta:

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

    As a quick fix one can post-process the traces from 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

    A cleaner fix would be to trim leading and trailing spaces in the tracer utility (just submitted a patch) or to fix the trace generation in verifyta. Example of fix using 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;

    (I also changed the if (str.empty()) to while (str.empty()), which looks safer).