{
"cells": [
{
"cell_type": "markdown",
"id": "f6e688db",
"metadata": {},
"source": [
"# Debugging models\n",
"Using stormvogel and stormpy, you can do a number of things to debug your models.\n",
"\n",
"* Showing End Components\n",
"* Showing Prob01 sets\n",
"* Showing shortest stochastic paths\n",
"* Adding assertions to your models\n",
"\n",
"We will demonstrate this with this simple toy MDP model."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "59837ab4",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:25.903334Z",
"iopub.status.busy": "2026-03-26T10:48:25.903140Z",
"iopub.status.idle": "2026-03-26T10:48:26.298860Z",
"shell.execute_reply": "2026-03-26T10:48:26.298317Z"
}
},
"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",
"mdp = examples.create_debugging_mdp()\n",
"vis = show(mdp, layout=Layout(\"layouts/mec.json\"))"
]
},
{
"cell_type": "markdown",
"id": "bd4b5d91",
"metadata": {},
"source": [
"## Showing Maximal End Components\n",
"(This is already included in another notebook, but also here for completeness)"
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "7de6f942",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.306043Z",
"iopub.status.busy": "2026-03-26T10:48:26.305739Z",
"iopub.status.idle": "2026-03-26T10:48:26.317323Z",
"shell.execute_reply": "2026-03-26T10:48:26.316767Z"
}
},
"outputs": [],
"source": [
"decomp = extensions.stormvogel_get_maximal_end_components(mdp)\n",
"vis.highlight_decomposition(decomp)"
]
},
{
"cell_type": "markdown",
"id": "c89b18e1",
"metadata": {
"lines_to_next_cell": 2
},
"source": [
"## Showing Prob01 sets\n",
"Given an MDP, a set of states $\\phi$, and a set of states $\\psi$.\n",
"\n",
"* The Prob01 **maximal** set is the set of states where $\\phi$ until $\\psi$ holds under **all** policies (schedulers).\n",
"* The Prob01 **minimal** set is the set of states where $\\phi$ until $\\psi$ holds under **some** policy (scheduler).\n",
"\n",
"In a DTMC the concept of maximal or minmal does not make sense, so we simply talk about the Prob01 set.\n",
"\n",
"Let us calculate the prob01 max states and min states for our model."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "4becec2c",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.319081Z",
"iopub.status.busy": "2026-03-26T10:48:26.318903Z",
"iopub.status.idle": "2026-03-26T10:48:26.323767Z",
"shell.execute_reply": "2026-03-26T10:48:26.323205Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"0 ['init', 'A']\n",
"1 ['X', 'mec']\n"
]
}
],
"source": [
"def to_bit_vector(state_set: set[int], model: Any):\n",
" assert stormpy is not None\n",
" return stormpy.BitVector(model.transition_matrix.nr_columns, list(state_set))\n",
"\n",
"\n",
"sp_mdp = stormpy_utils.mapping.stormvogel_to_stormpy(mdp)\n",
"max_res = stormpy.compute_prob01max_states(\n",
" sp_mdp, to_bit_vector({0, 1}, sp_mdp), to_bit_vector({2}, sp_mdp)\n",
")\n",
"min_res = stormpy.compute_prob01min_states(\n",
" sp_mdp, to_bit_vector({0, 1}, sp_mdp), to_bit_vector({2}, sp_mdp)\n",
")\n",
"print(0, mdp[0].labels)\n",
"print(1, mdp[1].labels)\n",
"# Note that for a DTMC, we can use `compute_prob01_states`.\n",
"max_0 = set(max_res[0])\n",
"max_1 = set(max_res[1])\n",
"min_0 = set(min_res[0])\n",
"min_1 = set(min_res[1])"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "1e3dfb7c",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.325343Z",
"iopub.status.busy": "2026-03-26T10:48:26.325162Z",
"iopub.status.idle": "2026-03-26T10:48:26.352733Z",
"shell.execute_reply": "2026-03-26T10:48:26.352189Z"
}
},
"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": [
"vis = show(mdp, layout=Layout(\"layouts/mec.json\"))"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "50063d6e",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.359736Z",
"iopub.status.busy": "2026-03-26T10:48:26.359558Z",
"iopub.status.idle": "2026-03-26T10:48:26.368215Z",
"shell.execute_reply": "2026-03-26T10:48:26.367708Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(max_0, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "4de3acac",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.369879Z",
"iopub.status.busy": "2026-03-26T10:48:26.369712Z",
"iopub.status.idle": "2026-03-26T10:48:26.384193Z",
"shell.execute_reply": "2026-03-26T10:48:26.383663Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "7c290cda",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.385739Z",
"iopub.status.busy": "2026-03-26T10:48:26.385569Z",
"iopub.status.idle": "2026-03-26T10:48:26.391204Z",
"shell.execute_reply": "2026-03-26T10:48:26.390686Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(max_1, color=\"orange\")"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "feab552b",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.392741Z",
"iopub.status.busy": "2026-03-26T10:48:26.392573Z",
"iopub.status.idle": "2026-03-26T10:48:26.406784Z",
"shell.execute_reply": "2026-03-26T10:48:26.406233Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "6a6f8e39",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.408445Z",
"iopub.status.busy": "2026-03-26T10:48:26.408242Z",
"iopub.status.idle": "2026-03-26T10:48:26.418818Z",
"shell.execute_reply": "2026-03-26T10:48:26.418374Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(min_0, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "337c1022",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.420366Z",
"iopub.status.busy": "2026-03-26T10:48:26.420177Z",
"iopub.status.idle": "2026-03-26T10:48:26.434699Z",
"shell.execute_reply": "2026-03-26T10:48:26.434159Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "255a3f70",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.436379Z",
"iopub.status.busy": "2026-03-26T10:48:26.436200Z",
"iopub.status.idle": "2026-03-26T10:48:26.440507Z",
"shell.execute_reply": "2026-03-26T10:48:26.440034Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(min_1, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 12,
"id": "c6e22126",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:26.442093Z",
"iopub.status.busy": "2026-03-26T10:48:26.441934Z",
"iopub.status.idle": "2026-03-26T10:48:26.456777Z",
"shell.execute_reply": "2026-03-26T10:48:26.456341Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
}
],
"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": {
"12de1ccb04db44b58a666ad1132fccad": {
"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
}
},
"7d0928c0caeb45ed93c257a3eebcede5": {
"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
}
},
"8c1988ef45ee41a08163fdf159945cf4": {
"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_7d0928c0caeb45ed93c257a3eebcede5",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"9ce2968e962d41a798475cd62e3bae5e": {
"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
}
},
"9f0e49bcfde24098929d8c15e819924f": {
"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_12de1ccb04db44b58a666ad1132fccad",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"b934c2b686ee4cbf83ff9bd0a91a4f7f": {
"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
}
},
"bec9a3f8523647dd955db37d7e4c9f8d": {
"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_b934c2b686ee4cbf83ff9bd0a91a4f7f",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"d9d212f48ba94736945dd151d264f945": {
"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_9ce2968e962d41a798475cd62e3bae5e",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}