{ "cells": [ { "cell_type": "markdown", "id": "b5594ded-98b7-4aaa-8007-32f22e6b6bd6", "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": "b4889445-5f24-48a4-a5ec-31452dad1e24", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:31:58.870295Z", "iopub.status.busy": "2025-04-24T14:31:58.870123Z", "iopub.status.idle": "2025-04-24T14:32:01.582325Z", "shell.execute_reply": "2025-04-24T14:32:01.581760Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "0d3503c4e7784a06b5ac09916ffc4ead", "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": [ "return_id_result('http://127.0.0.1:8889', 'pfuQuMjZsTSPhUgZalTx', '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": "3eea2c19f0554a2cb2f8d2b1c5200296", "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" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "from stormvogel import *\n", "\n", "init = pgc.State(x=[\"init\"])\n", "\n", "def available_actions(s: pgc.State):\n", " if \"init\" in s.x:\n", " return [pgc.Action([\"one\"]), pgc.Action([\"two\"])]\n", " elif \"mec1\" in s.x or \"mec2\" in s.x:\n", " return [pgc.Action([\"one\"]), pgc.Action([\"two\"])]\n", " return [pgc.Action([])]\n", "\n", "def delta(s: pgc.State, a: pgc.Action):\n", " if \"init\" in s.x and \"one\" in a.labels:\n", " return [(0.5, pgc.State(x=[\"mec1\"])), (0.5, pgc.State(x=[\"mec2\"]))]\n", " elif \"mec1\" in s.x:\n", " return [(1, pgc.State(x=[\"mec2\"]))]\n", " elif \"mec2\" in s.x:\n", " return [(1, pgc.State(x=[\"mec1\"]))]\n", " elif \"init\" in s.x and \"two\" in a.labels:\n", " return [(1, pgc.State(x=[\"mec1\"]))]\n", " return [(1,s)]\n", "\n", "labels = lambda s: s.x\n", "\n", "mdp = pgc.build_pgc(\n", " delta=delta,\n", " initial_state_pgc=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": "92b22cf0-5a12-4652-b1ef-4b3bb5a66842", "metadata": {}, "source": [ "First, let's show the maximal end components of this model." ] }, { "cell_type": "code", "execution_count": 2, "id": "44b631e1-add4-4f45-9c4f-635fd8a12d34", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:01.616442Z", "iopub.status.busy": "2025-04-24T14:32:01.616240Z", "iopub.status.idle": "2025-04-24T14:32:01.622693Z", "shell.execute_reply": "2025-04-24T14:32:01.622176Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "[(frozenset({1, 2}), frozenset({(2, Action(labels=frozenset({'one'}))), (2, Action(labels=frozenset({'two'}))), (1, Action(labels=frozenset({'one'}))), (1, Action(labels=frozenset({'two'})))}))]\n" ] } ], "source": [ "def stormvogel_get_maximal_end_components(sv_model):\n", " sp_model = 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": "ac2073e9-1c88-4c64-937c-05eb7473933f", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:01.624782Z", "iopub.status.busy": "2025-04-24T14:32:01.624584Z", "iopub.status.idle": "2025-04-24T14:32:01.636440Z", "shell.execute_reply": "2025-04-24T14:32:01.636020Z" } }, "outputs": [], "source": [ "vis.highlight_decomposition(decomp)" ] }, { "cell_type": "markdown", "id": "66cbaa0a-1165-48c9-8529-1aa2c967defc", "metadata": {}, "source": [ "Now we perform end component elimination by converting to stormpy and back." ] }, { "cell_type": "code", "execution_count": 4, "id": "84392fb7-ab3c-4d28-993f-bebe4f72a179", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:01.638734Z", "iopub.status.busy": "2025-04-24T14:32:01.638370Z", "iopub.status.idle": "2025-04-24T14:32:01.644117Z", "shell.execute_reply": "2025-04-24T14:32:01.643606Z" } }, "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": "50ee6296-c604-4c1a-a395-52d34ad2f11c", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:01.646240Z", "iopub.status.busy": "2025-04-24T14:32:01.645811Z", "iopub.status.idle": "2025-04-24T14:32:01.698881Z", "shell.execute_reply": "2025-04-24T14:32:01.698254Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "cdaba7f3ee0c4319b01c235ee6a276cc", "version_major": 2, "version_minor": 0 }, "text/plain": [ "Output()" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "a93dc2ca12a54be8a730c1361d3e2a46", "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" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "sp_mdp = mapping.stormvogel_to_stormpy(mdp)\n", "sp_mdp_elim = simple_ec_elimination(sp_mdp)\n", "sv_mdp_elim = mapping.stormpy_to_stormvogel(sp_mdp_elim)\n", "vis = show(sv_mdp_elim)" ] }, { "cell_type": "markdown", "id": "4d2c5fd5-d566-4b6b-bb8c-729fbfac9a28", "metadata": {}, "source": [ "These functions are also available under stormvogel.extensions.ec_elimination." ] }, { "cell_type": "code", "execution_count": 6, "id": "067a6684-26b9-4ef6-ab1a-1ee969f83f8c", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:01.734243Z", "iopub.status.busy": "2025-04-24T14:32:01.734061Z", "iopub.status.idle": "2025-04-24T14:32:01.740349Z", "shell.execute_reply": "2025-04-24T14:32:01.739825Z" } }, "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 = mapping.stormpy_to_stormvogel(sp_mdp_elim2)\n", "sv_mdp_elim == sv_mdp_elim2" ] }, { "cell_type": "code", "execution_count": null, "id": "261b3e07-7a13-4f53-abb9-997ed645b5b2", "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.12.3" }, "widgets": { "application/vnd.jupyter.widget-state+json": { "state": { "012495a6f0c0433a95764846cad27581": { "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_93b24fbd6a4843309c5164288f3e6fc9", "msg_id": "", "outputs": [ { "data": { "text/html": "\n\n\n \n Network\n \n \n \n \n
\n \n \n \n\n", "text/plain": "" }, "metadata": {}, "output_type": "display_data" } ], "tabbable": null, "tooltip": null } }, "0a181083385b4313992a418ddb501e33": { "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 } }, "0ae4901fb9a5428d96ae6085e07bd594": { "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 } }, "0d3503c4e7784a06b5ac09916ffc4ead": { "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_967d2ce096f7409e9063e39a23fabb61", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "101af55554f743fc92804feba815f6f7": { "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_67a38bf5ef2a48d0a3699539caa57093", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "192b2db9fad244c8be0e4f535401a8ec": { "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 } }, "2fa5a2fe555147e09144de01a657769a": { "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 } }, "323d2faee8fa479683b34965aae646c5": { "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 } }, "3eea2c19f0554a2cb2f8d2b1c5200296": { "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_5fe83f2aae25489b8b5fd6604b52644c", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "413a6c19d3c647deb48bdc443fcbd27e": { "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 } }, "41eb497e9ffe4482b4770e41f90a091f": { "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_192b2db9fad244c8be0e4f535401a8ec", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "4b08f267a473407799ab4b24b96c3811": { "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 } }, "4f3a9b27544c42f2a1a5bfe077521d34": { "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 } }, "5434291fcf784e488eeadbd01b05ebf9": { "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 } }, "5fe83f2aae25489b8b5fd6604b52644c": { "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 } }, "67a38bf5ef2a48d0a3699539caa57093": { "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 } }, "6aa91a822fa54f29b740b71709edc6b2": { "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_c8db4d1d576041d68db029b1db7fbdd9", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "7481d0ea8b164bd2a4e97753758873c4": { "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_5434291fcf784e488eeadbd01b05ebf9", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "8667eed863494b9e9eec954060a0d692": { "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_2fa5a2fe555147e09144de01a657769a", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "93b24fbd6a4843309c5164288f3e6fc9": { "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 } }, "967d2ce096f7409e9063e39a23fabb61": { "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 } }, "a93dc2ca12a54be8a730c1361d3e2a46": { "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_0a181083385b4313992a418ddb501e33", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "b2a73a9ea17247a69bc66237130a6fa3": { "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 } }, "bb6d1a6d9c6f4827b8c5a60d81290687": { "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_0ae4901fb9a5428d96ae6085e07bd594", "msg_id": "", "outputs": [ { "data": { "text/html": "\n\n\n \n Network\n \n \n \n \n
\n \n \n \n\n", "text/plain": "" }, "metadata": {}, "output_type": "display_data" } ], "tabbable": null, "tooltip": null } }, "c4327044ecbc4cd596bafab1bbca5eb1": { "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_4f3a9b27544c42f2a1a5bfe077521d34", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "c85281acc2f04d61b66e6beecc11601b": { "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_4b08f267a473407799ab4b24b96c3811", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "c8db4d1d576041d68db029b1db7fbdd9": { "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 } }, "cdaba7f3ee0c4319b01c235ee6a276cc": { "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_413a6c19d3c647deb48bdc443fcbd27e", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "ed0e90c3629c45078e2127613e26c113": { "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_323d2faee8fa479683b34965aae646c5", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "f3ad1c5d3e1f4984b25a4884d851b715": { "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_b2a73a9ea17247a69bc66237130a6fa3", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }