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.

1. #includes in the source sometimes include string, which should be modified to string.h for some functions like strcmp, and strncpy to work.
2. There are missing #includes so that certain functions do not work. E.g., the for_each function is in the algorithm package of Boost but not properly included.
3. Some type definitions are not found, such as int32_t. Changing this to int 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

UPPAAL_COMPILE_ONLY=1 verifyta model.xml - > 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.

Advertisement