The repository contains various Uppaal models. Everyone is welcome to contribute by sending a pull-request or the model to Marius Mikučionis to be added.
The model should fall under one or several categories below. Please note the origins of the model file (authors, companies, universities, references to papers, reports, websites, previous versions).
Demo models demonstrate concepts and/or features. They should be focused, small and easy to understand. The verification should not take much effort, a few seconds at most. The model should explain the intentions and result interpretations in the comments.
Case study models are the result of analysis of a real phenomena. The models may contain many features, details and may take a lot of resources to verify. The model should contain comments explaining the relation to the real-world situations, expected or preliminary results.
The benchmark models can easily be scaled to accomodate larger instances of the original problem. The models should contain comments about the purpose, expected results and verification effort (preliminary time and memory utilisation).
Tests exercise specific situations exposing the details of the specific modeling features. The models should be minimimalistic and take negligible time to verify. The models should contain comments about the purpose and expected results.