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
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.
#includes in the source sometimes include
string, which should be modified to
string.hfor some functions like
- There are missing
#includes so that certain functions do not work. E.g., the
for_eachfunction is in the
algorithmpackage of Boost but not properly included.
- Some type definitions are not found, such as
int32_t. Changing this to
intworks fine for the moment.
Once these are fixed, the installation process went through smoothly.
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
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.
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
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.