Skip to main content.

Basic Information

The DBM library has now a binding to the Python language (version 2.x). This binding has been implemented using the SWIG interface generator.

See this page for the full list of Python-related timed automata analysis tools and libraries.


Download: python_dbm-0.1.tar.gz (linux source, current stable version).

Up-to-date source code can be found at Launchpad code repository.

Installing Under Linux

We tested Python binding on Linux only, GCC version 4.4.5.

If you have problems with building the binding on a 64 bit system, then you probably need to add -fPIC option to CFLAGS in UPPAAL DBM Makefile.

Before installing this binding, you need to install:

  1. UPPAAL DBM library
  2. SWIG (we used SWIG Version 1.3.40)

It's assumed that UPPAAL DBM library headers are located in "/usr/local/uppaal/include", and library itself is located in "/usr/local/uppaal/lib". If it's not the case, please modify

Please follow these steps:

Getting Started

Let's create new context with clock variables "x", "y", z":
$ python
>>> from python_dbm import Context
>>> c = Context(["x", "y", "z"], "c")
Now we can declare federations of DBMs and operate them in natural way:
>>> a = (c.x < 10) & (c.x - c.y > 1)
>>> b = (c.x < 20)
>>> print a <= b    # is a included in b
>>> print a >= b    # is b included in a
>>> print a.up() | b
(c.x < 20) | (c.x-c.y < 10 & c.x-c.z < 10 & c.y-c.x < -1)
>>> print a | b
(c.x < 20)
You can see for the complete list of implemented operations over federations of DBMs; contains more examples of usage of this binding.