The purpose of the current webpage is to describe a collection of open-source tools and libraries that are written in Python language and that can be used for fast-prototyping of timed automata analysis algorithms. All these tools have been developed at Centre for Embedded Software Systems at Aalborg University.
It should be mentioned that these tools and libraries are prototypes in terms of performance and user experience. If you do not need to prototype new timed automata analysis algorithms, then you are welcome to use the UPPAAL model checker.
The tools don't provide graphical interface and it is recommended to use UPPAAL as a model editor.
Please propose patches/report bugs by contacting tools maintainers or using the Launchpad facilities (where all the tools are hosted).
PyUPPAAL is a Python library for syntactically manipulating UPPAAL timed automata models. It can import, export and layout UPPAAL models.
Current state: PyUPPAAL supports all the UPPAAL language features except that PyUPPAAL doesn't at the moment parse template-specific declarations and functions.
Maintained by: Mads Chr. Olesen and Kenneth Yrke Jorgensen.
PyDBM is a Python binding to the UPPAAL DBM library. DBMs are efficient data structures to represent clock constraints in timed automata. The UPPAAL DBM library features all the common operations such as up (delay or future), down (past), general updates, extrapolation functions on the federations of DBMs.
Current state: all the major operations are supported. Library is working only with federations of DBMs (not with single DBMs).
Maintained by: Peter Bulychev
OPAAL is a model checker whose goal is to enable rapid prototyping of new model-checking algorithms and data structures. Currently it supports discrete-time and continuous-time semantics of timed automata. OPAAL requires PyUPPAAL as a parsing library and PyDBM to handle DBMs (if continuous-time semantics is used).
Current state: supports the whole UPPAAL language except functions, typedefs and constant that are only partially supported.
Maintained by: Mads Chr. Olesen and Kenneth Yrke Jorgensen.
DBMPyUPPAAL is a modification of PyUPPAAL that substitutes all the invariants and guards in the Python representation of timed automata by their DBMs. Here is a simple implementation of reachability checking algorithm using DBMPyUPPAAL. Note, that DBMPyUPPAAL is planned to be merged with OPAAL in future.
Maintained by: Peter Bulychev
DBMPyUPPAAL with discrete variables is a branch of DBMPyUPPAAL that supports Python discrete variables (e.g. integers, strings, lists and even user-defined classes).
Current state: Unstable, undocumented, just a prototype.
Maintained by: Peter Bulychev
An unnamed implementation of the algorithm described in Peter Bulychev, Franck Cassez, Alexandre David, Kim Guldstrand Larsen, Jean-Francois Raskin and Pierre-Alain Reynier "Controllers with Minimal Observation Power (Application to Timed Systems)" ATVA 2012 paper
Current state: Just a prototype to compare the efficiency of the different algorithm options.
Maintained by: Peter Bulychev