{
"cells": [
{
"cell_type": "markdown",
"id": "41c5e14b",
"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": "6d4224f6",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:23:59.325377Z",
"iopub.status.busy": "2025-08-27T16:23:59.325220Z",
"iopub.status.idle": "2025-08-27T16:24:02.639719Z",
"shell.execute_reply": "2025-08-27T16:24:02.639210Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "ea86a7a31bd547428a6ea1f1717ec8f9",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/javascript": [
"\n",
"function return_id_result(url, id, data) {\n",
" fetch(url, {\n",
" method: 'POST',\n",
" body: JSON.stringify({\n",
" 'id': id,\n",
" 'data': data\n",
" })\n",
" })\n",
" }\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/javascript": [
"return_id_result('http://127.0.0.1:8889', 'DylMbUgSTgkYbTBmBaZv', 'test message')"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Test request failed. See 'Implementation details' in docs. Disable warning by use_server=False.\n"
]
},
{
"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",
"mdp = examples.create_debugging_mdp()\n",
"vis = show(mdp, layout=Layout(\"layouts/mec.json\"))"
]
},
{
"cell_type": "markdown",
"id": "67ab2aa8",
"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": "cc6e1a4c",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.647512Z",
"iopub.status.busy": "2025-08-27T16:24:02.647344Z",
"iopub.status.idle": "2025-08-27T16:24:02.659116Z",
"shell.execute_reply": "2025-08-27T16:24:02.658629Z"
}
},
"outputs": [],
"source": [
"decomp = extensions.stormvogel_get_maximal_end_components(mdp)\n",
"vis.highlight_decomposition(decomp)"
]
},
{
"cell_type": "markdown",
"id": "a9bf6e23",
"metadata": {},
"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": "2b301642",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.660704Z",
"iopub.status.busy": "2025-08-27T16:24:02.660538Z",
"iopub.status.idle": "2025-08-27T16:24:02.665609Z",
"shell.execute_reply": "2025-08-27T16:24:02.665185Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"0 ['init', 'A']\n",
"1 ['X', 'mec']\n"
]
}
],
"source": [
"from stormvogel.extensions import to_bit_vector as bv\n",
"\n",
"sp_mdp = stormpy_utils.mapping.stormvogel_to_stormpy(mdp)\n",
"max_res = stormpy.compute_prob01max_states(sp_mdp, bv({0, 1}, sp_mdp), bv({2}, sp_mdp))\n",
"min_res = stormpy.compute_prob01min_states(sp_mdp, bv({0, 1}, sp_mdp), bv({2}, sp_mdp))\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": "f43fd46e",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.667053Z",
"iopub.status.busy": "2025-08-27T16:24:02.666887Z",
"iopub.status.idle": "2025-08-27T16:24:02.699379Z",
"shell.execute_reply": "2025-08-27T16:24:02.698887Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "c1646bda5e3b42e681310947f2cae74f",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"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": "16f81631",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.707102Z",
"iopub.status.busy": "2025-08-27T16:24:02.706933Z",
"iopub.status.idle": "2025-08-27T16:24:02.715109Z",
"shell.execute_reply": "2025-08-27T16:24:02.714592Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(max_0, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "d8a1ad44",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.716583Z",
"iopub.status.busy": "2025-08-27T16:24:02.716435Z",
"iopub.status.idle": "2025-08-27T16:24:02.729641Z",
"shell.execute_reply": "2025-08-27T16:24:02.729161Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "41f3a01b",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.731227Z",
"iopub.status.busy": "2025-08-27T16:24:02.731068Z",
"iopub.status.idle": "2025-08-27T16:24:02.736227Z",
"shell.execute_reply": "2025-08-27T16:24:02.735748Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(max_1, color=\"orange\")"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "43fb4a10",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.737663Z",
"iopub.status.busy": "2025-08-27T16:24:02.737507Z",
"iopub.status.idle": "2025-08-27T16:24:02.750315Z",
"shell.execute_reply": "2025-08-27T16:24:02.749822Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "c1194840",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.751697Z",
"iopub.status.busy": "2025-08-27T16:24:02.751539Z",
"iopub.status.idle": "2025-08-27T16:24:02.760488Z",
"shell.execute_reply": "2025-08-27T16:24:02.760018Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(min_0, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "63d86d14",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.761881Z",
"iopub.status.busy": "2025-08-27T16:24:02.761697Z",
"iopub.status.idle": "2025-08-27T16:24:02.774782Z",
"shell.execute_reply": "2025-08-27T16:24:02.774274Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "612dc43d",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.776271Z",
"iopub.status.busy": "2025-08-27T16:24:02.776123Z",
"iopub.status.idle": "2025-08-27T16:24:02.779955Z",
"shell.execute_reply": "2025-08-27T16:24:02.779449Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(min_1, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 12,
"id": "8675e662",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:24:02.781426Z",
"iopub.status.busy": "2025-08-27T16:24:02.781269Z",
"iopub.status.idle": "2025-08-27T16:24:02.793983Z",
"shell.execute_reply": "2025-08-27T16:24:02.793492Z"
}
},
"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.13.3"
},
"widgets": {
"application/vnd.jupyter.widget-state+json": {
"state": {
"05cd2c66875748c1b1380d5b919fb171": {
"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_e0cf7abc19644f1e95335fd3c58fca72",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"1671a9e96bd1435f8d66fd800b04b8c7": {
"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
}
},
"22b5a70bcab5477d9e19e54fa648c4bb": {
"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
}
},
"35c9598e4e70465ca8d799c87b3efb24": {
"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
}
},
"3684322c400e4a0f8f15ddea8d880ed2": {
"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_b6cc397d5b4b45ad940ca2c3637b494e",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "792bb51665864323aba36be2ba00b0f2",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"436d0e0ef36e4a4f9a23dd27f7dcba87": {
"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
}
},
"45bf1fca1ab24cf78c81b27a6c2332fd": {
"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_35c9598e4e70465ca8d799c87b3efb24",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"58f772f9a17f494b98dd6286edc94cca": {
"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
}
},
"61bc68161d4b4ed880df6a9f1a9ff81e": {
"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
}
},
"63d562a2bdbd49ae8758747947e38686": {
"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_d0ddbb16b9324ead936f9dd31225325d",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"7139c8823a9b4120b13288fe58c6c3e4": {
"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
}
},
"792bb51665864323aba36be2ba00b0f2": {
"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_7139c8823a9b4120b13288fe58c6c3e4",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"7ff252c5665444a0a09d261c9203696d": {
"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_dc8128473f5a4fc093c3ec8f875b4089",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "792bb51665864323aba36be2ba00b0f2",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"b6cc397d5b4b45ad940ca2c3637b494e": {
"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
}
},
"c1646bda5e3b42e681310947f2cae74f": {
"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_58f772f9a17f494b98dd6286edc94cca",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"c9ab03c0dd354f7db94347bbe6135e68": {
"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_61bc68161d4b4ed880df6a9f1a9ff81e",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"d0ddbb16b9324ead936f9dd31225325d": {
"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
}
},
"dc8128473f5a4fc093c3ec8f875b4089": {
"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
}
},
"e0cf7abc19644f1e95335fd3c58fca72": {
"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
}
},
"ea86a7a31bd547428a6ea1f1717ec8f9": {
"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_436d0e0ef36e4a4f9a23dd27f7dcba87",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"f42d2d47f2e647edaba5272cae1793ce": {
"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_22b5a70bcab5477d9e19e54fa648c4bb",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"ffcb326c743b490cb635306aaecf2bc6": {
"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_1671a9e96bd1435f8d66fd800b04b8c7",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}