The Timed Automata Model-Checker

TiAMo (Timed Automata Model-checker)

M. Colange
O. Sankur

TiAMo is also based on the DBM library from Uppaal (part of the udbml library), and on the timed automata parser library from Uppaal, distributed with TiAMo. The name of the authors and contributors of these libraries can be found in their respective folders. Both libraries have been adapted by M. Colange (essentially to drop dependency on Boost, and to work with C++11).

TiAMo is developed and funded by the ERC Project Equalis.

Installation Notes

Requires ocaml and ocamlbuild (you can obtain them through opam).
Requires libxml2 (for the parser).
Requires a C++11-compatible compiler (successfully tested with gcc-4.7, gcc-4.8, gcc-4.9 and gcc-5.3.0).

  • install udbml
  • install TiAMo

The script 'build.sh' retrieves udbml, compiles and installs it (locally), then compiles TiAMo. Simply run this script, or modify it if you want a custom installation.