{ "cells": [ { "cell_type": "markdown", "id": "b95c2a8a", "metadata": {}, "source": [ "# End component elimination\n", "End Components (ECs) are sets of states in an MDP where:\n", "* Every state can reach every other state. (Strongly Connected Component)\n", "* All actions always lead to a state that is also in the MEC (there is no escape)\n", "\n", "For analysis, it is often useful to eliminate these MECs to a single state. We will show how to do this using stormpy and stormvogel." ] }, { "cell_type": "code", "execution_count": 1, "id": "8e2b7b2e", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:06.341552Z", "iopub.status.busy": "2025-08-27T16:24:06.341381Z", "iopub.status.idle": "2025-08-27T16:24:09.663909Z", "shell.execute_reply": "2025-08-27T16:24:09.663347Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "6d002e82ed9f44cc858e4fe040aeb081", "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', 'txgjvHZmYDAXdDPAadFa', '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", "\n", "init = \"init\"\n", "\n", "def available_actions(s: bird.State):\n", " if s == \"init\":\n", " return [[\"one\"], [\"two\"]]\n", " elif s == \"mec1\" or s == \"mec2\":\n", " return [[\"one\"], [\"two\"]]\n", " return [[]]\n", "\n", "def delta(s: bird.State, a: bird.Action):\n", " if s == \"init\" and \"one\" in a:\n", " return [(0.5, \"mec1\"), (0.5, \"mec2\")]\n", " elif s == \"mec1\":\n", " return [(1, \"mec2\")]\n", " elif s == \"mec2\":\n", " return [(1, \"mec1\")]\n", " elif s == \"init\" and \"two\" in a:\n", " return [(1, \"mec1\")]\n", " return [(1,s)]\n", "\n", "labels = lambda s: s\n", "\n", "mdp = bird.build_bird(\n", " delta=delta,\n", " init=init,\n", " available_actions=available_actions,\n", " labels=labels,\n", " modeltype=ModelType.MDP,)\n", "vis = show(mdp, layout=Layout(\"layouts/mec.json\"))" ] }, { "cell_type": "markdown", "id": "ce621336", "metadata": {}, "source": [ "First, let's show the maximal end components of this model." ] }, { "cell_type": "code", "execution_count": 2, "id": "5440890d", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:09.672790Z", "iopub.status.busy": "2025-08-27T16:24:09.672575Z", "iopub.status.idle": "2025-08-27T16:24:09.678911Z", "shell.execute_reply": "2025-08-27T16:24:09.678458Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[(frozenset({1, 2}), frozenset({(1, Action(labels=frozenset({'one'}))), (2, Action(labels=frozenset({'two'}))), (2, Action(labels=frozenset({'one'}))), (1, Action(labels=frozenset({'two'})))}))]\n" ] } ], "source": [ "def stormvogel_get_maximal_end_components(sv_model):\n", " sp_model = stormpy_utils.mapping.stormvogel_to_stormpy(sv_model)\n", " f = extensions.choice_mapping(sv_model, sp_model)\n", " decomposition = stormpy.get_maximal_end_components(sp_model)\n", " res = []\n", " for mec in decomposition:\n", " states = set()\n", " actions = set()\n", " for s_id, choices in mec:\n", " states.add(s_id)\n", " actions = actions | set(map(lambda x: f.inverse[x], choices))\n", " res.append((frozenset(states), frozenset(actions)))\n", " return res\n", "\n", "decomp = stormvogel_get_maximal_end_components(mdp)\n", "print(decomp)" ] }, { "cell_type": "code", "execution_count": 3, "id": "428cfb06", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:09.680417Z", "iopub.status.busy": "2025-08-27T16:24:09.680262Z", "iopub.status.idle": "2025-08-27T16:24:09.691490Z", "shell.execute_reply": "2025-08-27T16:24:09.690968Z" } }, "outputs": [], "source": [ "vis.highlight_decomposition(decomp)" ] }, { "cell_type": "markdown", "id": "2a11461d", "metadata": {}, "source": [ "Now we perform end component elimination by converting to stormpy and back." ] }, { "cell_type": "code", "execution_count": 4, "id": "d4500996", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:09.693171Z", "iopub.status.busy": "2025-08-27T16:24:09.693003Z", "iopub.status.idle": "2025-08-27T16:24:09.698184Z", "shell.execute_reply": "2025-08-27T16:24:09.697750Z" } }, "outputs": [], "source": [ "import stormpy\n", "\n", "def map_state_labels(m, res):\n", " \"\"\"Based on the result of EC elimination, create a new state labeling that can be used for a new model that captures the result.\n", " Args:\n", " m: stormpy model\n", " res (EndComponentEliminatorReturnTypeDouble): EC result\n", " \"\"\"\n", " old_nr_columns = m.transition_matrix.nr_columns\n", " new_nr_columns = res.matrix.nr_columns\n", " sl = stormpy.StateLabeling(new_nr_columns)\n", "\n", " for s_old in range(old_nr_columns):\n", " s_new = res.old_to_new_state_mapping[s_old]\n", " for l in m.labeling.get_labels_of_state(s_old):\n", " sl.add_label(l)\n", " sl.add_label_to_state(l, s_new)\n", " return sl\n", "\n", "def map_choice_labels(m_old, m_new, res):\n", " \"\"\"Based on the result of EC elimination, create a new choice labeling that can be used for a new model that captures the result.\n", " Args:\n", " m_old: old stormpy model\n", " m_new: new strompy model that is based on res\n", " res (EndComponentEliminatorReturnTypeDouble): EC result\n", " \"\"\"\n", " new_nr_rows = m_new.transition_matrix.nr_rows\n", " cl = stormpy.storage.ChoiceLabeling(new_nr_rows)\n", " old_nr_columns = m_old.transition_matrix.nr_columns\n", "\n", " for s_old in range(old_nr_columns):\n", " s_new = res.old_to_new_state_mapping[s_old]\n", " old_no_choices = m_old.get_nr_available_actions(s_old)\n", " new_no_choices = m_new.get_nr_available_actions(s_new)\n", " if (old_no_choices == new_no_choices):\n", " for action_no in range(old_no_choices):\n", " old_index = m_old.get_choice_index(s_old, action_no)\n", " labels = m_old.choice_labeling.get_labels_of_choice(old_index)\n", " new_index = m_new.get_choice_index(s_new, action_no)\n", " for l in labels:\n", " cl.add_label(l)\n", " cl.add_label_to_choice(l, new_index)\n", " return cl\n", "\n", "def simple_ec_elimination(m):\n", " \"\"\"Perform EC elimination on a stormpy model while preserving labels.\n", " Label sets of merged states are unified.\n", " Action labels are preserved when possible.\n", " Args:\n", " m: stormpy model\n", " \"\"\"\n", " # Keep all states, and consider ecs to be possible anywhere in the model\n", " subsystem = stormpy.BitVector(m.nr_states, True)\n", " possible_ec_rows = stormpy.BitVector(m.nr_choices, True)\n", " res = stormpy.eliminate_ECs(\n", " matrix = m.transition_matrix,\n", " subsystem = subsystem,\n", " possible_ecs = possible_ec_rows,\n", " add_sink_row_states = subsystem,\n", " add_self_loop_at_sink_states=True\n", " )\n", " new_labels = map_state_labels(m, res)\n", " components = stormpy.SparseModelComponents(transition_matrix=res.matrix, state_labeling=new_labels)\n", " m_new = stormpy.storage.SparseMdp(components)\n", " components.choice_labeling = map_choice_labels(m, m_new, res)\n", " m_updated = stormpy.storage.SparseMdp(components)\n", " return m_updated" ] }, { "cell_type": "code", "execution_count": 5, "id": "c290666e", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:09.699635Z", "iopub.status.busy": "2025-08-27T16:24:09.699480Z", "iopub.status.idle": "2025-08-27T16:24:09.736101Z", "shell.execute_reply": "2025-08-27T16:24:09.735542Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "8841d2f8b93b4e2e88f6135fb4f50af5", "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": [ "sp_mdp = stormpy_utils.mapping.stormvogel_to_stormpy(mdp)\n", "sp_mdp_elim = simple_ec_elimination(sp_mdp)\n", "sv_mdp_elim = stormpy_utils.mapping.stormpy_to_stormvogel(sp_mdp_elim)\n", "vis = show(sv_mdp_elim)" ] }, { "cell_type": "markdown", "id": "8444a4ea", "metadata": {}, "source": [ "These functions are also available under stormvogel.extensions.ec_elimination." ] }, { "cell_type": "code", "execution_count": 6, "id": "27f8c93a", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:09.744178Z", "iopub.status.busy": "2025-08-27T16:24:09.744010Z", "iopub.status.idle": "2025-08-27T16:24:09.749879Z", "shell.execute_reply": "2025-08-27T16:24:09.749338Z" } }, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "sp_mdp_elim2 = extensions.simple_ec_elimination(sp_mdp)\n", "sv_mdp_elim2 = stormpy_utils.mapping.stormpy_to_stormvogel(sp_mdp_elim2)\n", "sv_mdp_elim == sv_mdp_elim2" ] } ], "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": { "0482cf8d065f470fbfea38f25dcf719f": { "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 } }, "0eb34b37ee864d5f9208941121c7d502": { "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 } }, "137081c83363466a9e98ddddd310fd53": { "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 } }, "261e96e744f74e6c98c184c226406bea": { "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_f0c87f5a41f24f869bd26bf5d163ecf8", "msg_id": "", "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "8516da3b4e7840509c9a17910bbf03ca", "version_major": 2, "version_minor": 0 }, "text/plain": "Output()" }, "metadata": {}, "output_type": "display_data" } ], "tabbable": null, "tooltip": null } }, "4172bc13143144bb8224a2949910944a": { "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 } }, "4c80a7eb25744794b03ee9202ab810dd": { "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 } }, "51e3fa129dc24667bc3ad6cf3569bc78": { "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 } }, "667c84ddf1a9489d8d0bdf094decfd0c": { "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_f5c05d04dd5c4381b3f736337e9cf404", "msg_id": "", "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "8516da3b4e7840509c9a17910bbf03ca", "version_major": 2, "version_minor": 0 }, "text/plain": "Output()" }, "metadata": {}, "output_type": "display_data" } ], "tabbable": null, "tooltip": null } }, "6a021a782cca4742b62df79fcbc11300": { "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 } }, "6d002e82ed9f44cc858e4fe040aeb081": { "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_4172bc13143144bb8224a2949910944a", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "8516da3b4e7840509c9a17910bbf03ca": { "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_0482cf8d065f470fbfea38f25dcf719f", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "8841d2f8b93b4e2e88f6135fb4f50af5": { "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_967560407d6b4f95a49979da18ea0f68", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "967560407d6b4f95a49979da18ea0f68": { "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 } }, "9eab210c419c4082b2a52f1f090b8455": { "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_51e3fa129dc24667bc3ad6cf3569bc78", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "a1e646bbbfa1478d8e33ac156955bee9": { "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_e4f00962eda54f378f0cf36f91b4cd1b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "bc8e010342194b718acafb8eb6ebade3": { "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_0eb34b37ee864d5f9208941121c7d502", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "d0504cd235684deebff4278b4003afdc": { "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_137081c83363466a9e98ddddd310fd53", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "d4ab288719e64a2a9439c82a31e1c100": { "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_6a021a782cca4742b62df79fcbc11300", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "e4f00962eda54f378f0cf36f91b4cd1b": { "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 } }, "f0c87f5a41f24f869bd26bf5d163ecf8": { "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 } }, "f403d040737a4097b1bb8a3a4b969b9a": { "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_4c80a7eb25744794b03ee9202ab810dd", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "f5c05d04dd5c4381b3f736337e9cf404": { "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 }