Uppaal Timed Automata Parser Library

The Uppaal Timed Automata Parser Library (libutap) is the parser library used by UPPAAL. It is distributed separately from UPPAAL under the LGPL license. On this page you can find the source code of the library and some documentation.

News

• December 1, 2021: source moved to GitHub

  The library source and issue tracker can be found at GitHub: UppaalModelChecker/utap

• March 20th, 2019: Version 0.94 released. Download.

  This is a snapshot of UTAP from UPPAAL pre-release of 4.1.20.

• October 5th, 2015: Version 0.93 released. Download.

  This is a snapshot of UTAP from UPPAAL pre-release of 4.1.20. Highlights of this release include:

  • Fixed tracer utility with respect to newer GUI trace format.
  • Fixed pretty printer of embedded queries.

• March 30th, 2015: Version 0.92 released.

  This is a snapshot of UTAP in the latest development version of UPPAAL. Highlights of this release include:

  • SMC extensions.
  • Integrated queries into main model document.
  • Various bug fixes.

• February 22nd, 2007: Version 0.91 released.

  This is a snapshot of UTAP in the latest development version of UPPAAL. Highlights of this release include:

  • Bugs fixed in this release: 322, 336, 348, 351, 352, 353, 358, 364, 367, 370, 372, 383.
  • CTL parsing has been enhanced to allow nesting of formulas.
  • TIGA support was added.
  • Improved compilation on Windows.
  • Syntax check utility was renamed to 'syntaxcheck'
  • Type checker was cleaned up
  • IO Interface utility renamed to 'taflow'
  • Improved pretty printer
  • Refactored SystemBuilder into SystemBuilder and StatementBuilder

• April 29th, 2006: Version 0.90 release.

  This is the version of UTAP used in UPPAAL 3.6 Beta 3. The tracer utility no longer uses libutap. Instead it parses the UPPAAL intermediate format introduced in UPPAAL 3.6 Beta 1.

  Position tracking (the mechanism used to map an expression to some position in the input file) has been reimplemented. The representation of types in UTAP has been reimplemented.

  The interpreter for expressions has been removed. It was broken and could not be fixed without reimplementing major parts of the UPPAAL interpreter (not included in UTAP). This also means that errors related to the range of variables or expressions are no longer detected by the TypeChecker class.

• November 23rd, 2005: Version 0.80 released.

  This is the version used in UPPAAL 3.6 Alpha 1. It contains a lot of bug fixes since version 0.70. Likely there are some API incompatibilities, but it should not be hard to adapt your program to version 0.80. Notice that configure now accepts the --enable-cora option to enable the extensions used by UPPAAL CORA.

• February 17th, 2005: Version 0.70 released.

  This is the version used in UPPAAL 3.4.8. It is a backport from our development branch. Notice that this release requires libxml2 2.6.10 or newer.

• June 17th, 2004: Version 0.60 released.

  This is the version used in UPPAAL 3.4.6. It is a backport from our development branch. Notice that this release requires libxml2 2.6.0 or newer.

• May 15th, 2004: Version 0.50 released

  This is the version used in UPPAAL 3.4.5.

• July 2nd, 2003: Version 0.40 released

This is the version used in UPPAAL 3.4 Beta 3.

• April 6th, 2003: Version 0.30 released

  This is the version used in UPPAAL 3.4 Beta 2.

• February 18th, 2003: Version 0.20 released

  This is the version used in UPPAAL 3.4 Beta 1.

• December 20th, 2002: Version 0.10 released

  Initial release.

Downloads

• libutap-0.94.tar.gz
• libutap-0.93.tar.gz
• libutap-0.92.tar.gz
• libutap-0.91.tar.gz
• libutap-0.90.tar.gz
• libutap-0.80.tar.gz
• libutap-0.70.tar.gz
• libutap-0.60.tar.gz
• libutap-0.50.tar.gz
• libutap-0.40.tar.gz
• libutap-0.30.tar.gz
• libutap-0.20.tar.gz
• libutap-0.10.tar.gz

Requirements

You need the following tools and libraries on your system in order to compile and use the library:

• gcc (3.2 or newer)
• libxml2 (2.6.10 or newer)
• GNU make (3.79 works fine; other versions of make may work, but have not been tested)
• flex - optional (2.5.4a works fine)
• bison - optional (at least version 2.0)
• gperf - optional (2.7.2 works fine)
• doxygen - optional (1.3-rc3 works fine)
• Boost C++ Libraries (versions 1.32 and 1.33 work fine)

Installation

libutap uses automake and autoconf to generate make files and configure the build process. To configure and install the library, simply run:

./configure
make
make install

You may want to specify an alternative installation path using the --prefix option.

Documentation

The following documentation of the library is available at the moment:

• Language guide
• README
• ChangeLog
• API

Traces

The above source code download contains the tracer utility which given a UPPAAL XTR trace file prints the trace to stdout. You may use this example as a starting point for writing your own trace analysis tools. This tool requires access to the UPPAAL intermediate format introduced in UPPAAL 3.6 Beta 1. Invoke it as:

UPPAAL_COMPILE_ONLY=1 verifyta model.xml - | tracer - trace.xtr

or

UPPAAL_COMPILE_ONLY=1 verifyta model.xml - > model.if
tracer model.if trace.xtr

Links

Visit us at our UPPAAL page.