{ "cells": [ { "cell_type": "markdown", "id": "72b3fb19-0af4-4bc8-bc22-32e1a0c8057f", "metadata": {}, "source": [ "# Gymnasium integration\n", "[Gymnasium](https://gymnasium.farama.org/) is an API standard for reinforcement learning with a diverse collection of reference environments. Stormvogel supports some integration with gymnasium. In particular, you can construct explicit models from the gymnasium environmnents under Gymnasium's [ToyText](https://gymnasium.farama.org/environments/toy_text/) (except Blackjack). " ] }, { "cell_type": "markdown", "id": "27be6901-4d8c-407b-af77-028ff0042042", "metadata": {}, "source": [ "## FrozenLake\n", "Let us create one of these environments, called FrozenLake.\n", "Our agent wants to get to the present. Currently, it just chooses a random action." ] }, { "cell_type": "code", "execution_count": 1, "id": "88910590-1351-4842-90f5-f0c137622a41", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:11.941172Z", "iopub.status.busy": "2025-04-24T14:32:11.940999Z", "iopub.status.idle": "2025-04-24T14:32:13.034177Z", "shell.execute_reply": "2025-04-24T14:32:13.033637Z" } }, "outputs": [ { "data": { "text/html": [ "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "import gymnasium as gym\n", "from stormvogel.extensions.gym_grid import *\n", "from stormvogel import *\n", "import IPython.display as ipd\n", "\n", "env = gym.make(\"FrozenLake-v1\", render_mode=\"rgb_array\", is_slippery=False) # Set `is_slippery=True` for stochastic behavior\n", "filename = gymnasium_render_model_gif(env, filename=\"ice1\")\n", "extensions.embed_gif(filename)" ] }, { "cell_type": "markdown", "id": "8e41a630-2f18-43e4-a1d2-8d2f6dae9a19", "metadata": {}, "source": [ "We can convert it into an explicit MDP as follows. Each state has a label that relates to the coordinates of the tile." ] }, { "cell_type": "code", "execution_count": 2, "id": "29ca2085-5f8f-4b7c-9f42-1303b3a0e48a", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:13.036700Z", "iopub.status.busy": "2025-04-24T14:32:13.036241Z", "iopub.status.idle": "2025-04-24T14:32:15.091896Z", "shell.execute_reply": "2025-04-24T14:32:15.091311Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "b29773bf90f648a383ccfec87733153e", "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', 'PLfBCmauKejScegqiypE', '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": "29031150668742628481e9d4531586b6", "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": [ "sv_model = gymnasium_grid_to_stormvogel(env, GRID_ACTION_LABEL_MAP)\n", "# GRID_ACTION_LABEL_MAP = {0: \"←\", 1: \"↓\", 2: \"→\", 3: \"↑\", 4: \"pickup\", 5: \"dropoff\"} (map between gymnasium action ids and labels)\n", "vis = show(sv_model, layout=Layout(\"layouts/frozenlake.json\"))" ] }, { "cell_type": "markdown", "id": "9808734d-b750-46b4-bfb6-423e516ce257", "metadata": {}, "source": [ "Now, let's do some model checking to calculate a strategy to solve the puzzle. We will tell the model checker to maximize the probability of getting to the target state (the present)." ] }, { "cell_type": "code", "execution_count": 3, "id": "2db709fa-5735-4fd2-9b0d-e9c36c8f3ff2", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:15.124958Z", "iopub.status.busy": "2025-04-24T14:32:15.124765Z", "iopub.status.idle": "2025-04-24T14:32:15.195771Z", "shell.execute_reply": "2025-04-24T14:32:15.195195Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "73f3edf6b9dd4160b5507afae31e3951", "version_major": 2, "version_minor": 0 }, "text/plain": [ "Output()" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "fc81593f63ea4b99bae49cfc75bda7eb", "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": [ "res = model_checking(sv_model, f'Pmax=? [F \"target\"]')\n", "vis2 = show(sv_model, result=res, layout=Layout(\"layouts/frozenlake.json\"))" ] }, { "cell_type": "markdown", "id": "c3eabd69-5579-47ca-b121-aa9244d53976", "metadata": {}, "source": [ "Let's highlight the path to see what the scheduler is doing." ] }, { "cell_type": "code", "execution_count": 4, "id": "6d45cc94-244a-4d67-b32a-65762672507a", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:15.228801Z", "iopub.status.busy": "2025-04-24T14:32:15.228412Z", "iopub.status.idle": "2025-04-24T14:32:28.279839Z", "shell.execute_reply": "2025-04-24T14:32:28.279301Z" } }, "outputs": [], "source": [ "from stormvogel.stormpy_utils.simulator import simulate_path\n", "path = simulate_path(sv_model, scheduler=res.scheduler, steps=20)\n", "vis2.highlight_path(path, color=\"orange\")" ] }, { "cell_type": "markdown", "id": "e2caeb6c-294a-4707-abc0-a07907506c79", "metadata": {}, "source": [ "Alternatively, we can show what our scheduler does in the frozen lake environment itself." ] }, { "cell_type": "code", "execution_count": 5, "id": "28240a9f-c0fa-4ba5-9192-3ea47aab9a0d", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:28.282184Z", "iopub.status.busy": "2025-04-24T14:32:28.282022Z", "iopub.status.idle": "2025-04-24T14:32:28.327371Z", "shell.execute_reply": "2025-04-24T14:32:28.326890Z" } }, "outputs": [ { "data": { "text/html": [ "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "from stormvogel.extensions.gym_grid import *\n", "gs = to_gymnasium_scheduler(sv_model, res.scheduler, GRID_ACTION_LABEL_MAP)\n", "filename = gymnasium_render_model_gif(env, gs, filename=\"ice2\")\n", "extensions.embed_gif(filename)" ] }, { "cell_type": "markdown", "id": "1a4715dc-d299-45da-bc69-c0291c9d448f", "metadata": {}, "source": [ "We can also define a function to act as the scheduler on the model and convert it to a gymnasium scheduler. This one just keeps going in a loop..." ] }, { "cell_type": "code", "execution_count": 6, "id": "239c5130-8d51-4a68-bebe-f86b06430f55", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:28.329709Z", "iopub.status.busy": "2025-04-24T14:32:28.329337Z", "iopub.status.idle": "2025-04-24T14:32:28.634484Z", "shell.execute_reply": "2025-04-24T14:32:28.634009Z" } }, "outputs": [ { "data": { "text/html": [ "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "from stormvogel.model import Action\n", "\n", "def my_scheduler(s: stormvogel.model.State):\n", " # \"←\" \"↓\" \"→\" \"↑\"\n", " if s.is_initial():\n", " return Action.create(\"→\")\n", " env_id = int(s.labels[0])\n", " x,y = to_coordinate(env_id,env)\n", " if x < 2 and y == 0:\n", " return Action.create(\"→\")\n", " elif x == 2 and y < 2:\n", " return Action.create(\"↓\")\n", " elif x > 0 and y == 2:\n", " return Action.create(\"←\")\n", " else:\n", " return Action.create(\"↑\")\n", "\n", "gs = to_gymnasium_scheduler(sv_model, my_scheduler, GRID_ACTION_LABEL_MAP)\n", "filename = gymnasium_render_model_gif(env, gs, filename=\"ice3\")\n", "extensions.embed_gif(filename)" ] }, { "cell_type": "markdown", "id": "5260e1e3-9b6b-4ae6-b48e-276477ad4059", "metadata": {}, "source": [ "## CliffWalking\n", "CliffWalking is a slightly more boring version of FrozenLake. You can apply the same principles that we just applied to FrozenLake." ] }, { "cell_type": "code", "execution_count": 7, "id": "4ad97870-e088-46d8-86b1-011f82e4c6e9", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:28.636911Z", "iopub.status.busy": "2025-04-24T14:32:28.636477Z", "iopub.status.idle": "2025-04-24T14:32:28.643002Z", "shell.execute_reply": "2025-04-24T14:32:28.642610Z" } }, "outputs": [], "source": [ "import gymnasium as gym\n", "from stormvogel.extensions.gym_grid import *\n", "\n", "env = gym.make(\"CliffWalking-v0\", render_mode=\"rgb_array\")" ] }, { "cell_type": "code", "execution_count": 8, "id": "c7e7c0b1-1dbe-42a0-a0a8-da742cffc03a", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:28.645125Z", "iopub.status.busy": "2025-04-24T14:32:28.644771Z", "iopub.status.idle": "2025-04-24T14:32:28.703081Z", "shell.execute_reply": "2025-04-24T14:32:28.702576Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "80f36a27593641978f3247f3fbec9be4", "version_major": 2, "version_minor": 0 }, "text/plain": [ "Output()" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "8142d82db4d94a009688fa1a537fd26e", "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": [ "sv_model = gymnasium_grid_to_stormvogel(env, GRID_ACTION_LABEL_MAP)\n", "vis = show(sv_model, layout=Layout(\"layouts/cliffwalking.json\"))" ] }, { "cell_type": "code", "execution_count": 9, "id": "b5c3cd5a-aeb5-492c-bb30-ec37375be9ce", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:28.733844Z", "iopub.status.busy": "2025-04-24T14:32:28.733664Z", "iopub.status.idle": "2025-04-24T14:32:28.950112Z", "shell.execute_reply": "2025-04-24T14:32:28.949609Z" } }, "outputs": [ { "data": { "text/html": [ "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "from stormvogel.stormpy_utils.model_checking import model_checking\n", "res = model_checking(sv_model, f'Pmax=? [F \"target\"]')\n", "gs = to_gymnasium_scheduler(sv_model, res.scheduler, GRID_ACTION_LABEL_MAP)\n", "filename = gymnasium_render_model_gif(env, gs, filename=\"cliff\")\n", "extensions.embed_gif(filename)" ] }, { "cell_type": "markdown", "id": "4192e230-efb6-4fb4-a818-da147ca7de77", "metadata": {}, "source": [ "## Taxi\n", "In the Taxi scenario, a taxi has to pick up passengers and transport them to the hotel. The position of the target, passenger and taxi are chosen at random." ] }, { "cell_type": "code", "execution_count": 10, "id": "813a8e52-e176-4d39-a92f-3a77a40ae484", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:28.952368Z", "iopub.status.busy": "2025-04-24T14:32:28.952190Z", "iopub.status.idle": "2025-04-24T14:32:29.129424Z", "shell.execute_reply": "2025-04-24T14:32:29.128856Z" } }, "outputs": [ { "data": { "text/plain": [ "'ModelType.MDP model with name None, 505 states, 7 actions, and 1005 distinct labels.'" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "import gymnasium as gym\n", "from stormvogel.extensions.gym_grid import *\n", "env = gym.make(\"Taxi-v3\", render_mode=\"rgb_array\") # Set `is_slippery=True` for stochastic behavior\n", "sv_model = gymnasium_grid_to_stormvogel(env)\n", "# This model is so big that it is better not to display it.\n", "sv_model.summary()" ] }, { "cell_type": "code", "execution_count": 11, "id": "6c8f787c-697d-4f0a-a915-f6a943ac8254", "metadata": { "execution": { "iopub.execute_input": "2025-04-24T14:32:29.131751Z", "iopub.status.busy": "2025-04-24T14:32:29.131547Z", "iopub.status.idle": "2025-04-24T14:32:30.101828Z", "shell.execute_reply": "2025-04-24T14:32:30.101294Z" } }, "outputs": [ { "data": { "text/html": [ "" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "import IPython.display as ipd\n", "\n", "target = get_target_state(env)\n", "res = model_checking(sv_model, f'Rmax=? [S]')\n", "gs = to_gymnasium_scheduler(sv_model, res.scheduler, GRID_ACTION_LABEL_MAP)\n", "filename = gymnasium_render_model_gif(env, gs, filename=\"taxi\")\n", "extensions.embed_gif(filename)" ] }, { "cell_type": "code", "execution_count": null, "id": "89010416-e635-4bbe-b020-0107a5d586f4", "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "code", "execution_count": null, "id": "202f32f3-a381-480b-9f4c-8b5bc48e9af5", "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": { "0a25ba479a3d48718e8b9de2e0f0b837": { "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 } }, "14d87cad20c840f88ff869cd56c2f64d": { "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 } }, "1d8b612b8ece41e49d7191dd9dcc7d92": { "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 } }, "246d0e00896040d69e19f12cc96feb57": { "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 } }, "29031150668742628481e9d4531586b6": { "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_52652d12f9e44d10a97e39338bb82f27", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "31aff16530b24b62a88efbcae6eadc34": { "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 } }, "349535d7862b468d87bf6d6aab8bddaa": { "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_d2bfee97ccf84d4ab06811893711a109", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "52652d12f9e44d10a97e39338bb82f27": { "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 } }, "535536f627cd4999906dff7345903603": { "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 } }, "5f76d37cd6594d1bbe4f76438329d915": { "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 } }, "606c8a4ad16448a6adee29e2cbc9faa5": { "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_7c2ed4593bf44931b501ef16fd96d22e", "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 } }, "60954a7ff5f14566bf294eb267f37108": { "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_1d8b612b8ece41e49d7191dd9dcc7d92", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "631ecd4dab034da8adb4a6298e671fe1": { "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_14d87cad20c840f88ff869cd56c2f64d", "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 } }, "73f3edf6b9dd4160b5507afae31e3951": { "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_31aff16530b24b62a88efbcae6eadc34", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "7c2ed4593bf44931b501ef16fd96d22e": { "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 } }, "80f36a27593641978f3247f3fbec9be4": { "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_e67d286db3ad48838bf7efe90950e971", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "8142d82db4d94a009688fa1a537fd26e": { "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_da4c8b920c77491196cc19ac917b670d", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "890303247241459ea6ffd3e86490fa09": { "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_e8c59efed67b41279a84fdf9d2678b92", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "8939969e154e49c8b03dc1ea66210cb6": { "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_ccbc293719ca45e4a8ba05efedc77511", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "b29773bf90f648a383ccfec87733153e": { "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_c541f6bb07a04760a40d20a01009f3d9", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "bf4873c1eea7404397834ccde08ad247": { "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_e4a7344f8c6242029a3d21c0c60ca71b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "c541f6bb07a04760a40d20a01009f3d9": { "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 } }, "ccbc293719ca45e4a8ba05efedc77511": { "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 } }, "d2bfee97ccf84d4ab06811893711a109": { "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 } }, "da2c74e8551a44a98261851fd84fee29": { "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_5f76d37cd6594d1bbe4f76438329d915", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "da4c8b920c77491196cc19ac917b670d": { "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 } }, "dfb2cec1ebe347d5b901a3e220437eee": { "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 } }, "e07668f656e046a69461f8824d9c1ce7": { "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_f86a3f19db0c4c2781bb128a883b4956", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "e4a7344f8c6242029a3d21c0c60ca71b": { "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 } }, "e67d286db3ad48838bf7efe90950e971": { "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 } }, "e8c59efed67b41279a84fdf9d2678b92": { "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 } }, "eb7bbdb9bcd74e379b3cfa0509cef82d": { "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_0a25ba479a3d48718e8b9de2e0f0b837", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "f3171cc6ed52469f948500a8fedd7ebd": { "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_535536f627cd4999906dff7345903603", "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 } }, "f38b1a0d5ee64589aa03ebb791ab9877": { "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_dfb2cec1ebe347d5b901a3e220437eee", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "f86a3f19db0c4c2781bb128a883b4956": { "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 } }, "fc81593f63ea4b99bae49cfc75bda7eb": { "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_246d0e00896040d69e19f12cc96feb57", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }