Symrob: timed automata model checker
==========
This is a prototype model checker reading a subset of Uppaal xml files
with the following features:
1) Basic zone-based model checking
2) Robust model checking algorithm of the following paper:

Ocan Sankur. Symbolic Quantitative Robustness Analysis of Timed Automata In TACAS'15 LNCS 9035, pages 484-498. Springer Berlin Heidelberg, 2015.

3) A counter-example guided abstraction refinement algorithm using BDDs (the CUDD library), described in the following paper:

Victor Roussanaly, Ocan Sankur and Nicolas Markey. Abstraction Refinement Algorithms for Timed Automata. CAV 2019.

To reproduce the results of this paper, please see the src/experiments/cav19/cav19-artifact directory.

Installation
============
All packages below are required and can be installed using opam:
- OCaml 4.0+
- ocamlbuild
- ocaml batteries included 2.2+
- xml-light
- mlcuddidl

Compilation
===========
1) Build and install uppaal_parser (make; make install)
2) Build symrob (make)

License
=============
Some of the examples in the src/experiments directory were taken from 
the Verifix tool (http://satoss.uni.lu/members/piotr/verifix/)
by Piotr Kordy.

The license for symrob is GNU GPL 3.0
See the file LICENSE or https://www.gnu.org/licenses/gpl-3.0-standalone.html

Author and Contact
============================
Ocan Sankur <[email protected]>