{
"cells": [
{
"cell_type": "markdown",
"id": "fe3f725a-e324-4b85-87e7-ad4483812ff3",
"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": "10e462d5-8aaf-46ec-ae1f-f15fda069d4c",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:09.629441Z",
"iopub.status.busy": "2025-07-21T08:30:09.629253Z",
"iopub.status.idle": "2025-07-21T08:30:12.821791Z",
"shell.execute_reply": "2025-07-21T08:30:12.821251Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "96c312f5321f4c1b8d5ad065b5fd0171",
"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', 'XXmxhcvFlEMCjeLYFZQJ', '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": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "f4c929c956e1419f8ccca7500f2fb4be",
"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": [
"from stormvogel import *\n",
"mdp = examples.create_debugging_mdp()\n",
"vis = show(mdp, layout=Layout(\"layouts/mec.json\"))"
]
},
{
"cell_type": "markdown",
"id": "04e9cf3a-39f7-4fd1-b611-483a489d625c",
"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": "0c523d2b-6bb1-440f-8ef1-85119a270093",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:12.873514Z",
"iopub.status.busy": "2025-07-21T08:30:12.873104Z",
"iopub.status.idle": "2025-07-21T08:30:12.884698Z",
"shell.execute_reply": "2025-07-21T08:30:12.884283Z"
}
},
"outputs": [],
"source": [
"decomp = extensions.stormvogel_get_maximal_end_components(mdp)\n",
"vis.highlight_decomposition(decomp)"
]
},
{
"cell_type": "markdown",
"id": "9941e0eb-dc0b-4b87-bef0-dc7a095ce920",
"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": "4dd4b3bc-27b6-4923-858c-81359f108fb4",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:12.886531Z",
"iopub.status.busy": "2025-07-21T08:30:12.886167Z",
"iopub.status.idle": "2025-07-21T08:30:12.892037Z",
"shell.execute_reply": "2025-07-21T08:30:12.891624Z"
}
},
"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": "dc08f122-9830-415a-be7f-6bcfa0b9aaef",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:12.893746Z",
"iopub.status.busy": "2025-07-21T08:30:12.893386Z",
"iopub.status.idle": "2025-07-21T08:30:12.961618Z",
"shell.execute_reply": "2025-07-21T08:30:12.961098Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "c7d15df8187b4c97a75bbbdf993bb31e",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "8c91df7e3e64431ab92b9e897a2f65ec",
"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": "b58ee8d5-1013-4470-9dd1-c02a8fc7002b",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.010335Z",
"iopub.status.busy": "2025-07-21T08:30:13.010099Z",
"iopub.status.idle": "2025-07-21T08:30:13.018595Z",
"shell.execute_reply": "2025-07-21T08:30:13.018089Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(max_0, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "697e2e3e-87d2-476e-8fb8-6649a7d511af",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.020466Z",
"iopub.status.busy": "2025-07-21T08:30:13.020135Z",
"iopub.status.idle": "2025-07-21T08:30:13.033702Z",
"shell.execute_reply": "2025-07-21T08:30:13.033283Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "ce86d73a-9a4c-4f86-bd50-1dc0ab0005b0",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.035501Z",
"iopub.status.busy": "2025-07-21T08:30:13.035098Z",
"iopub.status.idle": "2025-07-21T08:30:13.040679Z",
"shell.execute_reply": "2025-07-21T08:30:13.040163Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(max_1, color=\"orange\")"
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "a21ddfb2-cbd1-44ea-9411-e9b82423d194",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.042460Z",
"iopub.status.busy": "2025-07-21T08:30:13.042095Z",
"iopub.status.idle": "2025-07-21T08:30:13.055030Z",
"shell.execute_reply": "2025-07-21T08:30:13.054637Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "7ac0992a-9ed5-4fc7-95bc-21c30656561d",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.056710Z",
"iopub.status.busy": "2025-07-21T08:30:13.056377Z",
"iopub.status.idle": "2025-07-21T08:30:13.065625Z",
"shell.execute_reply": "2025-07-21T08:30:13.065234Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(min_0, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 10,
"id": "17ccb3f3-1e53-4e81-8536-9053f3a3d39a",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.067147Z",
"iopub.status.busy": "2025-07-21T08:30:13.066979Z",
"iopub.status.idle": "2025-07-21T08:30:13.079873Z",
"shell.execute_reply": "2025-07-21T08:30:13.079483Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "a2d9a305-f120-469d-87d8-23a6610d7dcc",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.081493Z",
"iopub.status.busy": "2025-07-21T08:30:13.081188Z",
"iopub.status.idle": "2025-07-21T08:30:13.085085Z",
"shell.execute_reply": "2025-07-21T08:30:13.084608Z"
}
},
"outputs": [],
"source": [
"vis.highlight_state_set(min_1, color=\"pink\")"
]
},
{
"cell_type": "code",
"execution_count": 12,
"id": "0345bd89-4a61-49d7-be3d-2071fb8077a3",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:30:13.086792Z",
"iopub.status.busy": "2025-07-21T08:30:13.086424Z",
"iopub.status.idle": "2025-07-21T08:30:13.099264Z",
"shell.execute_reply": "2025-07-21T08:30:13.098790Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "19d18729-4579-4dff-a1bd-d5f95e48e3f5",
"metadata": {},
"outputs": [],
"source": []
}
],
"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": {
"1671513a4968402a93fa75706675accb": {
"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
}
},
"198ec8df58b64d1789191c5934c07cf3": {
"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_e4f7182841dc41a3bc4530c4f6f071c1",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"2391e5a5333c488f86e39deba1782ade": {
"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
}
},
"3e1582f0cc444b9da24bcfe61a160364": {
"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
}
},
"474e462cc6dd40388379ec34cabad7d3": {
"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
}
},
"4d33dd0b4ea44cc18cef791e41ac463d": {
"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_3e1582f0cc444b9da24bcfe61a160364",
"msg_id": "",
"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"
}
],
"tabbable": null,
"tooltip": null
}
},
"57a1422a56194e0385cc9d3c28ba6b9a": {
"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
}
},
"5bb33d28c3b44f69a63ff9f671926e7e": {
"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_9d240d95327a4007b0bd7e2614562736",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"5ffd58d469e94c4db08dc7eed54e1ce3": {
"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_d4df3b1e6ed2484c8cc23b95d741a6a4",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"62aa306f914340d7ae70d5b0d857a461": {
"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_c72995ff51ee4fca850fe3828b0d69b8",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"62d0485118d240ac942062b71b691d99": {
"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
}
},
"8c91df7e3e64431ab92b9e897a2f65ec": {
"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_f431114be0504766b0bce51171ffea30",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"96c312f5321f4c1b8d5ad065b5fd0171": {
"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_1671513a4968402a93fa75706675accb",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"9d240d95327a4007b0bd7e2614562736": {
"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
}
},
"a0e25892d1a8417283486ad1132bc094": {
"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_62d0485118d240ac942062b71b691d99",
"msg_id": "",
"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"
}
],
"tabbable": null,
"tooltip": null
}
},
"b128145eaae34a298838d2ff7cd63a6b": {
"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_2391e5a5333c488f86e39deba1782ade",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"b6001dea7e7c4841b84bebca6f6fa616": {
"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
}
},
"c27ab7ad86a64d4793493c26ddcdb681": {
"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_d24116504331452f857cd6353241254d",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"c72995ff51ee4fca850fe3828b0d69b8": {
"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
}
},
"c7d15df8187b4c97a75bbbdf993bb31e": {
"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_b6001dea7e7c4841b84bebca6f6fa616",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"c91582570a924fe1b541067b947af0cf": {
"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_57a1422a56194e0385cc9d3c28ba6b9a",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"d24116504331452f857cd6353241254d": {
"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
}
},
"d4df3b1e6ed2484c8cc23b95d741a6a4": {
"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
}
},
"e4f7182841dc41a3bc4530c4f6f071c1": {
"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
}
},
"e9cf5a8c48d741ad87ac3ccdac927fdd": {
"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_474e462cc6dd40388379ec34cabad7d3",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"ead296060e904c1c81fd514ca7aaae64": {
"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
}
},
"f431114be0504766b0bce51171ffea30": {
"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
}
},
"f4c929c956e1419f8ccca7500f2fb4be": {
"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_ead296060e904c1c81fd514ca7aaae64",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}