{
"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-06-12T13:18:43.429070Z",
"iopub.status.busy": "2025-06-12T13:18:43.428903Z",
"iopub.status.idle": "2025-06-12T13:18:46.578143Z",
"shell.execute_reply": "2025-06-12T13:18:46.577586Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "2b1a746f40b64c059e76687cdbff308c",
"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', 'eROuFkRCVPnrCxnSUxOt', 'test message')"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Test request failed. See 'Communication server remark' in docs. Disable warning by use_server=False.\n"
]
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "c862a42a586f468cad0ae6897d5ae35e",
"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-06-12T13:18:46.628614Z",
"iopub.status.busy": "2025-06-12T13:18:46.628225Z",
"iopub.status.idle": "2025-06-12T13:18:46.640490Z",
"shell.execute_reply": "2025-06-12T13:18:46.639983Z"
}
},
"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-06-12T13:18:46.642307Z",
"iopub.status.busy": "2025-06-12T13:18:46.641998Z",
"iopub.status.idle": "2025-06-12T13:18:46.647216Z",
"shell.execute_reply": "2025-06-12T13:18:46.646720Z"
}
},
"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-06-12T13:18:46.648720Z",
"iopub.status.busy": "2025-06-12T13:18:46.648483Z",
"iopub.status.idle": "2025-06-12T13:18:46.719384Z",
"shell.execute_reply": "2025-06-12T13:18:46.718845Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "88bde8601f694d55a2caa9e5a23af3cc",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "a9a7fb764dcc454ba57d6d45926a553c",
"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-06-12T13:18:46.769491Z",
"iopub.status.busy": "2025-06-12T13:18:46.769313Z",
"iopub.status.idle": "2025-06-12T13:18:46.777456Z",
"shell.execute_reply": "2025-06-12T13:18:46.776999Z"
}
},
"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-06-12T13:18:46.779200Z",
"iopub.status.busy": "2025-06-12T13:18:46.778878Z",
"iopub.status.idle": "2025-06-12T13:18:46.791832Z",
"shell.execute_reply": "2025-06-12T13:18:46.791345Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 7,
"id": "ce86d73a-9a4c-4f86-bd50-1dc0ab0005b0",
"metadata": {
"execution": {
"iopub.execute_input": "2025-06-12T13:18:46.793358Z",
"iopub.status.busy": "2025-06-12T13:18:46.793193Z",
"iopub.status.idle": "2025-06-12T13:18:46.798473Z",
"shell.execute_reply": "2025-06-12T13:18:46.798086Z"
}
},
"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-06-12T13:18:46.799901Z",
"iopub.status.busy": "2025-06-12T13:18:46.799716Z",
"iopub.status.idle": "2025-06-12T13:18:46.812604Z",
"shell.execute_reply": "2025-06-12T13:18:46.812222Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 9,
"id": "7ac0992a-9ed5-4fc7-95bc-21c30656561d",
"metadata": {
"execution": {
"iopub.execute_input": "2025-06-12T13:18:46.814020Z",
"iopub.status.busy": "2025-06-12T13:18:46.813863Z",
"iopub.status.idle": "2025-06-12T13:18:46.822984Z",
"shell.execute_reply": "2025-06-12T13:18:46.822573Z"
}
},
"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-06-12T13:18:46.824372Z",
"iopub.status.busy": "2025-06-12T13:18:46.824211Z",
"iopub.status.idle": "2025-06-12T13:18:46.837060Z",
"shell.execute_reply": "2025-06-12T13:18:46.836578Z"
}
},
"outputs": [],
"source": [
"vis.clear_highlighting()"
]
},
{
"cell_type": "code",
"execution_count": 11,
"id": "a2d9a305-f120-469d-87d8-23a6610d7dcc",
"metadata": {
"execution": {
"iopub.execute_input": "2025-06-12T13:18:46.838607Z",
"iopub.status.busy": "2025-06-12T13:18:46.838448Z",
"iopub.status.idle": "2025-06-12T13:18:46.842175Z",
"shell.execute_reply": "2025-06-12T13:18:46.841815Z"
}
},
"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-06-12T13:18:46.843559Z",
"iopub.status.busy": "2025-06-12T13:18:46.843401Z",
"iopub.status.idle": "2025-06-12T13:18:46.856409Z",
"shell.execute_reply": "2025-06-12T13:18:46.855916Z"
}
},
"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": {
"08f5b189e00245d897b432b2350eb2f8": {
"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
}
},
"1cdb631c34f34487a190710234f31ee9": {
"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
}
},
"1eee888d6cc54566a7ec554063320aaa": {
"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_9e253cf52c2d44a1820f3b7175e5a83f",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"2b1a746f40b64c059e76687cdbff308c": {
"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_9fd3aa5ff7864afba632a05bc240a939",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"2ca8515f50e74f80a08709c33443ac71": {
"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
}
},
"47935610be2742e6a7b6827fcf6f7fe2": {
"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_cc3b797e6be04829bd31934390076f77",
"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
}
},
"52787e1a213e4209973361a9b9fa021a": {
"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_08f5b189e00245d897b432b2350eb2f8",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"53b64f67940d42bb931ebc27199af223": {
"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_f277a7b7fd354ac890a1873bd1e09fe0",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"57709aca032c445d9ca0d629b9dd5be2": {
"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
}
},
"57f869cc1b494f1496953aa17de9d271": {
"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
}
},
"6e4f01d6f7014b1d996fca62481a2086": {
"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
}
},
"73231a4737194944a4ef98de8cc25dc3": {
"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_1cdb631c34f34487a190710234f31ee9",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"734895af11534499a2bd870f4935125b": {
"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_f688ccc47b3e4fb38727eacd6a05a486",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"7d3737a99be44e6aa7725beb01851e24": {
"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_6e4f01d6f7014b1d996fca62481a2086",
"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
}
},
"87014c401a484d5988b6e418a1884cbc": {
"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_d229d396848a4f2094a9d76e763d3525",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"88bde8601f694d55a2caa9e5a23af3cc": {
"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_a6c13d0883ed4a98a2fc7c8ff9c0ca9c",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"9c75c20be71943729f24b3ab345a5122": {
"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
}
},
"9e253cf52c2d44a1820f3b7175e5a83f": {
"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
}
},
"9fd3aa5ff7864afba632a05bc240a939": {
"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
}
},
"a6c13d0883ed4a98a2fc7c8ff9c0ca9c": {
"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
}
},
"a9a7fb764dcc454ba57d6d45926a553c": {
"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_57709aca032c445d9ca0d629b9dd5be2",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"c862a42a586f468cad0ae6897d5ae35e": {
"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_2ca8515f50e74f80a08709c33443ac71",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"cc3b797e6be04829bd31934390076f77": {
"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
}
},
"d229d396848a4f2094a9d76e763d3525": {
"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
}
},
"d88dd0bb36394df68b8d9461d509780b": {
"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_57f869cc1b494f1496953aa17de9d271",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"e1616f4791fd492db6ea46e800db14c6": {
"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_9c75c20be71943729f24b3ab345a5122",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"f277a7b7fd354ac890a1873bd1e09fe0": {
"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
}
},
"f688ccc47b3e4fb38727eacd6a05a486": {
"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
}