{
"cells": [
{
"cell_type": "markdown",
"id": "bc2df244",
"metadata": {},
"source": [
"# Welcome to Stormvogel!\n",
"\n",
"\n",
"This notebook provides an introduction to the stormvogel project, a first example, and pointers to further material. We recommend to also look at\n",
"\n",
"- The source code, hosted at [Github](https://github.com/stormchecker/stormvogel)\n",
"- The python packages, hosted at [Pypi](https://pypi.org/project/stormvogel/)\n",
"- User documentation, which includes this notebook [Docs](https://stormchecker.github.io/stormvogel/)\n",
"- Reach out to us at our [Discord Server](https://discord.gg/byeKSasJY6)\n"
]
},
{
"cell_type": "markdown",
"id": "d89194b1",
"metadata": {},
"source": [
"## Installing with pip\n",
"\n",
"The easiest way to install stormvogel is by pip:\n",
"```\n",
"pip install stormvogel\n",
"pip install stormpy # Optional, for efficient model checking algorithms\n",
"```"
]
},
{
"cell_type": "markdown",
"id": "23e9d31d",
"metadata": {},
"source": [
"## Running the Docker container\n",
"\n",
"Another way to run stormvogel is by running our [Docker](https://www.docker.com) container on your local machine.\n",
"```\n",
"docker pull stormvogel/stormvogel\n",
"docker run -it -p 8080:8080 stormvogel/stormvogel\n",
"```\n",
"\n",
"See the GitHub repository for more advanced installation options."
]
},
{
"cell_type": "markdown",
"id": "b8074c5d",
"metadata": {},
"source": [
"## What is probabilistic model checking?\n",
"\n",
"### Qualitative model checking\n",
"Model checking, in this context, refers to methods and techniques to exhaustively analyze whether a model of system behavior satisfies a given formal specification. For the (initial) development of such techniques, Clarke, Emerson and Sifakis were awarded the ACM Turing Award in 2007. Specifically, these models are typically state-based formalism that describe the dynamics of a system, such as a hardware circuit or a computer program. Simple specifications ask: *Is it possible to reach this error state?*, *Is it possible to simultaneously open the microwave while it is active?*, *Can one throw 3 sixes in a row?* etc. Traditionally, the outcome is a yes/no answer, but typically, model checking techniques output some kind of witness that certifies why the answer is yes or provides a counterexample when the answer is no.\n",
"\n",
"Below we have a toy model of a car. The idea is that the car always choose whether to 'wait' (that is, continue driving), or to 'brake'. This car does not satisfy the specification to never reach the state 'accident' as a driver could choose to consistently continue driving."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "15c73405",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:47:23.382487Z",
"iopub.status.busy": "2026-03-26T10:47:23.382221Z",
"iopub.status.idle": "2026-03-26T10:47:23.776470Z",
"shell.execute_reply": "2026-03-26T10:47:23.775838Z"
},
"jupyter": {
"is_executing": true
}
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"from stormvogel import *\n",
"\n",
"vis = show(\n",
" examples.create_car_mdp(), layout=stormvogel.layout.Layout(\"layouts/car.json\")\n",
")"
]
},
{
"cell_type": "markdown",
"id": "47f041cc",
"metadata": {},
"source": [
"### Probabilistic Model Checking\n",
"Model checking asks whether something is possible (or dually, whether something always holds). Its perspective cannot distinguish between likely and unlikely events. However, often it is not possible to completely rule out unwanted behavior. In those cases, one may still want to assert that it the unwanted behavior is unlikely to occur: It is possible that all packets are dropped when communicating over ethernet, but it is highly unlikely, just like it is possible but highly unlikely to throw 100 sixes in a row.\n",
"\n",
"Probabilistic model checking therefore analyses Markov models, state-based formalisms that describe the dynamics of probabilistic processes. It yields guarantees that, e.g., *the probability to reach a dangerous state is sufficiently small*, but also that *the expected energy consumption is low*, or that *the probability that a battery depletes during a drone lands* is tiny.\n",
"\n",
"Probabilistic model checking is a general technique and can be applied to any problem which can be modelled as Markov model, such as an Markov decision process (MDP). Given that these models are used in many different domains, the use of probabilistic model checking is not limited to software and hardware verification.\n",
"\n",
"## Tools for Probabilistic Model Checking\n",
"The research community in probabilistic model checking is largely tool driven. While many smaller prototype implementations exist, some larger ecosystems have emerged, in particular PRISM, Modest, and Storm. For an overview of the field, we refer to [this recent paper](https://www.prismmodelchecker.org/papers/pfqa-pmc-appls.pdf). Stormvogel, as the name suggests, has been primarily developed on top of the ecosystem that the model checker Storm provides.\n",
"\n",
"\n",
"### Storm, Stormpy and Stormvogel\n",
"* [Storm](https://www.stormchecker.org/) is a probabilistic model checker, written in C++, whose primary goal is to provide the fastest algorithms for standard probabilistic model checking queries. This goal comes at a cost of a steep learning curve.\n",
"* [Stormpy](https://moves-rwth.github.io/stormpy/) is an low-level API with Python bindings for Storm that allows developers working with Storm to quickly prototype new algorithms. It is structured mostly similarly to Storm itself.\n",
"* Stormvogel is a collection of Python APIs and visualization tools with ease-of-use as top priority: The goal of Stormvogel is to provide an accessible way to do probabilistic model checking and to provide educational tools about model checking. It can be easily interfaced with Stormpy to profit from high-performance model checking.\n",
"\n",
"## What does Stormvogel provide?\n",
"While Stormvogel is still under active development, these are the current key features.\n",
"\n",
"* APIs for constructing Markov models in dedicated data structures. Currently, DTMCs, MDPs, CTMCs, MAs and POMDPs are supported.\n",
" - The *model* API can be used to construct a model directly by explicitely defining a set of states and transitions.\n",
" - The *bird* API can be used to construct a model by defining a delta function. The structure is similar to PRISM.\n",
"* Seamless conversion between stormvogel and stormpy models with some runtime overhead. This allows, e.g., also using formats such as PRISM and JANI that are not supported by stormvogel directly.\n",
"* Visualization in notebooks.\n",
" - Visualize models by displaying the states, actions and edges.\n",
" - Edit and save/load the layout of models interactively using a GUI.\n",
" - Display model checking results in an interactive way.\n",
" - Visualize a simulation of a model.\n",
"* An interface for model checking.\n",
" - A function for model checking that takes a PRISM property string. This uses Storm under the hood, so it is efficient.\n",
" - A GUI for making it easier to construct property strings for beginners (the *property builder*).\n",
"* An extensive documentation, with ample examples.\n",
"\n",
"Details about these can be found in the remaining notebooks.\n",
"\n",
"## Questions/help, bugs & contributing\n",
"To suggest a feature or report a bug, simply create an issue on [Github](https://github.com/stormchecker/stormvogel). If you would like to contribute to the project yourself, you can always create a pull request or join our [public Discord server](https://discord.gg/byeKSasJY6).\n",
"\n",
"Stormvogel was developed at the Radboud University in 2024-2025 by Linus Heck, Pim Leerkes and Ivo Melse under the supervision of Sebastian Junges (Radboud) and Matthias Volk (Eindhoven University of Technology). We would like to thank the Dutch Research Council (NWO) for providing funding for the project via the NWO Open Science Fund Grant StormAE.\n",
"\n",
"Furthermore, we would like to thank our contributers Luko van der Maas, Nicklas Osmers.\n",
"\n",
"Good luck using stormvogel!"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "fc4fa69c",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:47:23.787525Z",
"iopub.status.busy": "2026-03-26T10:47:23.787154Z",
"iopub.status.idle": "2026-03-26T10:47:23.826051Z",
"shell.execute_reply": "2026-03-26T10:47:23.825499Z"
}
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"bird = show_bird()"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.13"
},
"widgets": {
"application/vnd.jupyter.widget-state+json": {
"state": {
"25cd9255103f4108bdb7f5f9901562a9": {
"model_module": "@jupyter-widgets/output",
"model_module_version": "1.0.0",
"model_name": "OutputModel",
"state": {
"_dom_classes": [],
"_model_module": "@jupyter-widgets/output",
"_model_module_version": "1.0.0",
"_model_name": "OutputModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/output",
"_view_module_version": "1.0.0",
"_view_name": "OutputView",
"layout": "IPY_MODEL_fd8fe9b7edf54e1f90adf51faf7d2391",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"29ae79715422451aa46aa5d5a76409fe": {
"model_module": "@jupyter-widgets/output",
"model_module_version": "1.0.0",
"model_name": "OutputModel",
"state": {
"_dom_classes": [],
"_model_module": "@jupyter-widgets/output",
"_model_module_version": "1.0.0",
"_model_name": "OutputModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/output",
"_view_module_version": "1.0.0",
"_view_name": "OutputView",
"layout": "IPY_MODEL_8754631787c9465ab396656c9597b6ea",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"31e57c98fdbb495e8080469c17d03382": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
},
"5a4fd008e9f248b7ba7c93b2aff1748e": {
"model_module": "@jupyter-widgets/output",
"model_module_version": "1.0.0",
"model_name": "OutputModel",
"state": {
"_dom_classes": [],
"_model_module": "@jupyter-widgets/output",
"_model_module_version": "1.0.0",
"_model_name": "OutputModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/output",
"_view_module_version": "1.0.0",
"_view_name": "OutputView",
"layout": "IPY_MODEL_31e57c98fdbb495e8080469c17d03382",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"8754631787c9465ab396656c9597b6ea": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
},
"abb94c1455b44965ab4477907e8c0eef": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
},
"e85d138b31524ceaa6d44172bc3aff0c": {
"model_module": "@jupyter-widgets/output",
"model_module_version": "1.0.0",
"model_name": "OutputModel",
"state": {
"_dom_classes": [],
"_model_module": "@jupyter-widgets/output",
"_model_module_version": "1.0.0",
"_model_name": "OutputModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/output",
"_view_module_version": "1.0.0",
"_view_name": "OutputView",
"layout": "IPY_MODEL_abb94c1455b44965ab4477907e8c0eef",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"fd8fe9b7edf54e1f90adf51faf7d2391": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}