Using Uppaal for trace interpretation
Uppaal is a model checking tool for timed automata.
When a counterexample is generated by Uppaal, or when a random / manual trace is
present in the Simulator, it is able to save the trace in Uppaal’s .xtr
format. However, this format is human-unreadable. This article records the steps
to compile and use the tracer utility for showing Uppaal traces outside of the
GUI. Assuming we are working under the Ubuntu 11.04 environment.
Installing Necessary Packages
The libboost-dev
and libxml2-dev
packages are needed by the Uppaal Timed
Automata Parser Library.
sudo apt-get install libboost-dev libxml2-dev
Compiling the UTAP library
The installation is a simple process as usual.
./configure
make
make check
sudo make install
For some reasons, however, there are errors when compiling the code. Essentially there are three groups of things to fix.
#include
s in the source sometimes includestring
, which should be modified tostring.h
for some functions likestrcmp
, andstrncpy
to work.- There are missing
#include
s so that certain functions do not work. E.g., thefor_each
function is in thealgorithm
package of Boost but not properly included. - Some type definitions are not found, such as
int32_t
. Changing this toint
works fine for the moment.
Once these are fixed, the installation process went through smoothly.
Using the tracer
Utility
The tracer utility takes a Uppaal intermediate format and a saved .xtr
file as
the only two inputs. To get the Uppaal intermediate format for a model in the
.xml
format, one should use
model.if
The dash here is a placeholder for the query file, which is not necessary for
intermediate format generation but helps pass syntax check by verifyta
.
With the generated intermediate format, one can reconstruct the trace is a readable format.
tracer model.if trace.xtr
Also, one can use the pretty
utility to pretty-print a Uppaal model in a
C-like format.
pretty model.xml
Update: Compiling the UTAP library under MacOSX
Under Mac OS X, the boost library is not by default available (if it is
installed separately, with MacPorts for example). If
this is the case, it is necessary to add options to ./configure
as follows.
./configure LDFLAGS=-L/opt/local/lib CXXFLAGS=-I/opt/local/include
Update: Issues with aclocal.m4
For some unknown reasons the aclocal.m4
file changes quite a bit; it even
changes from plain text to binary files. This makes the compiling process fail.
Just replace it with the pristine version that comes with the libutap
library
and the compiling should be fine.
Update: Download link
The original link to the library is broken. The new one is updated. Check this page.