uppaal-py

Python library for reading, writing, analyzing, and modifying UPPAAL timed automata files. Works with Python >= 3.8.

Disclaimer

uppaal-py is a work-in-progress library. For bugs, missing features or documentation please create an issue or send me an email. API is subject to change.

Dependencies

• lxml
• NetworkX
• ortools

Installation

Via pip:

pip install uppaal-py

License

MIT

Features

• Reading and writing UPPAAL files.
• LP based path realizability analysis.
• Finding set of furthest reachable locations with respect to a set of target (unsafe) locations.
• Working with variables of type int and a subset of expressions involving ints for guards, invariants, and updates during transitions allowed in UPPAAL in addition to clocks during computations.

TODO:

• [ ] Methods for calling UPPAAL/verifyta.
• [ ] Migrate to libutap for parsing files.
• [ ] Parameter synthesis for safety property.
• [ ] lxml type annotations and type annotations for the remaining functions.
• [ ] Auto-generated documentation.

Non-features

• Analysis involving network of TA — product of two or more TA can be implemented in the future, though.
• Symbolic model checking, UPPAAL does that.