{ "cells": [ { "cell_type": "markdown", "id": "5cddfe20", "metadata": {}, "source": [ "# Parallel composition\n", "Using the Bird API, you can define your own parallel composition logic. This works similar to PRISM models. We give an example here. We create two MDP models `m1` and `m2`, and then we create the quotient model `q`. They synchronize on the action `r`." ] }, { "cell_type": "markdown", "id": "cdfba47e", "metadata": {}, "source": [ "## m1\n", "`m1` is a simple 2x2 grid model where taking `l` `r` `u` and `d` move to the next tile." ] }, { "cell_type": "code", "execution_count": 1, "id": "52b5dc45", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:16.240326Z", "iopub.status.busy": "2025-08-27T16:24:16.240166Z", "iopub.status.idle": "2025-08-27T16:24:19.569581Z", "shell.execute_reply": "2025-08-27T16:24:19.569017Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "36ae5829cca34dc9a7c18bcef3a854fb", "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', 'olxFlZbgwfiPoBJOSpYp', '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 = 2\n", "\n", "ACTION_SEMANTICS = {\n", " \"l\": (-1, 0),\n", " \"r\": (1, 0),\n", " \"u\": (0, -1),\n", " \"d\": (0, 1) }\n", "\n", "def available_actions_m1(s):\n", " res = []\n", " if s[0] > 0:\n", " res.append(\"l\")\n", " if s[0] < N-1:\n", " res.append(\"r\")\n", " if s[1] > 0:\n", " res.append(\"u\")\n", " if s[1] < N-1:\n", " res.append(\"d\")\n", " return res\n", "\n", "def pairwise_plus(t1, t2):\n", " return (t1[0] + t2[0], t1[1] + t2[1])\n", "\n", "def delta_m1(s, a):\n", " return [(1, pairwise_plus(s, ACTION_SEMANTICS[a]))]\n", "\n", "def labels_m1(s):\n", " return [str(s)]\n", "\n", "m1 = bird.build_bird(\n", " init=(0,0),\n", " available_actions=available_actions_m1,\n", " labels=labels_m1,\n", " delta=delta_m1)\n", "vis_m1 = show(m1)" ] }, { "cell_type": "markdown", "id": "126bdb66", "metadata": {}, "source": [ "## m2\n", "`m2` is a model that counts the number of `r` up until two, and has a faulty reset button `c` to reset the counter. It only works in 80% of the cases. It only allows `r` if the count is not already 2." ] }, { "cell_type": "code", "execution_count": 2, "id": "834f7d00", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:19.577667Z", "iopub.status.busy": "2025-08-27T16:24:19.577430Z", "iopub.status.idle": "2025-08-27T16:24:19.611477Z", "shell.execute_reply": "2025-08-27T16:24:19.610958Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "986d9c59b656475693ecbbdd75175487", "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": [ "def available_actions_m2(s):\n", " if s <= 1:\n", " return [\"r\", \"c\"]\n", " if s == 2:\n", " return [\"c\"]\n", "\n", "def delta_m2(s, a):\n", " if s <= 1:\n", " if \"r\" in a:\n", " return [(1, s+1)]\n", " elif s == 0:\n", " return [(1,0)]\n", " else:\n", " return [(.8, 0), (.2, s)]\n", " else:\n", " return [(.8, 0), (.2, s)]\n", "\n", "def labels_m2(s):\n", " return [str(s)]\n", "\n", "m2 = bird.build_bird(\n", " init=0,\n", " available_actions=available_actions_m2,\n", " labels=labels_m2,\n", " delta=delta_m2)\n", "vis_m2 = show(m2)" ] }, { "cell_type": "markdown", "id": "a2f9580c", "metadata": {}, "source": [ "## Quotient model\n", "Now we construct the quotient model." ] }, { "cell_type": "code", "execution_count": 3, "id": "b62dda78", "metadata": { "execution": { "iopub.execute_input": "2025-08-27T16:24:19.619928Z", "iopub.status.busy": "2025-08-27T16:24:19.619664Z", "iopub.status.idle": "2025-08-27T16:24:19.656192Z", "shell.execute_reply": "2025-08-27T16:24:19.655684Z" } }, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "60a7bea7279d4765831339d4926518c1", "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": [ "SYNC = [\"r\"]\n", "\n", "def prob_product(branch1, branch2):\n", " return [(p1 * p2, (r1, r2)) for p1, r1 in branch1 for p2, r2 in branch2]\n", "\n", "def available_actions(s):\n", " a1 = available_actions_m1(s[0])\n", " a2 = available_actions_m2(s[1])\n", " union = set(a1 + a2)\n", " intersection = set(a1) & set(a2)\n", " return [x for x in union if x in intersection or x not in SYNC]\n", "\n", "def delta(s, a):\n", " a1 = available_actions_m1(s[0])\n", " a2 = available_actions_m2(s[1])\n", "\n", " if a in a1 and a in a2:\n", " return prob_product(delta_m1(s[0], a), delta_m2(s[1], a))\n", " elif a in a1:\n", " return [(p, (s_, s[1])) for p,s_ in delta_m1(s[0],a)]\n", " elif a in a2:\n", " return [(p, (s[0], s_)) for p,s_ in delta_m2(s[1],a)]\n", " else:\n", " return [(1,s)]\n", "\n", "def labels(s):\n", " return labels_m1(s[0]) + labels_m2(s[1])\n", "\n", "q = bird.build_bird(\n", " init=((0,0),0),\n", " available_actions=available_actions,\n", " labels=labels,\n", " delta=delta)\n", "vis_q = show(q)" ] } ], "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": { "0a5eba3c931a434898ffdcecf75fe00c": { "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_819505b06dbe4595a3130ae67858637c", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "18e9c8a931c94a31a83d9c27c59b450a": { "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 } }, "2781207cffb641b5b54eb365a01b2a20": { "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 } }, "36ae5829cca34dc9a7c18bcef3a854fb": { "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_653094b169ec47a3a63fc3bf884565fb", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "3cfa91423e28448ba2ab7e5fb68e9ab9": { "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_2781207cffb641b5b54eb365a01b2a20", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "44219ee4e58943f5bc586de245f14902": { "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 } }, "4bcba2cd03d640e38fa45e5bcb5f7812": { "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 } }, "5301a4c464fa42bdaca4eb32a26c5d0a": { "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_9e9c519482514c07845295117679cfa6", "msg_id": "", "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "635605b944aa42f58a3f6eaca6d7c0ba", "version_major": 2, "version_minor": 0 }, "text/plain": "Output()" }, "metadata": {}, "output_type": "display_data" } ], "tabbable": null, "tooltip": null } }, "5c80bd43e3324fe7aa0b4a5ffa66246b": { "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 } }, "5f6c4d820eca497ca951b07f102dff95": { "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 } }, "60a7bea7279d4765831339d4926518c1": { "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_5f6c4d820eca497ca951b07f102dff95", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "635605b944aa42f58a3f6eaca6d7c0ba": { "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_5c80bd43e3324fe7aa0b4a5ffa66246b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "653094b169ec47a3a63fc3bf884565fb": { "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 } }, "6717eb19cf7a4404996bf34e4d6d252d": { "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_b6e225e3a16e4d409af7c7e8440e4a60", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "70358ad05a48495eb8391d6100b78401": { "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 } }, "79326fafcc9846439ef4817281a21da5": { "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_4bcba2cd03d640e38fa45e5bcb5f7812", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "819505b06dbe4595a3130ae67858637c": { "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 } }, "890ba354f038452ca7036bd5596ee489": { "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_bd39ad7991874d85a461d3bcf11ad3d8", "msg_id": "", "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "635605b944aa42f58a3f6eaca6d7c0ba", "version_major": 2, "version_minor": 0 }, "text/plain": "Output()" }, "metadata": {}, "output_type": "display_data" } ], "tabbable": null, "tooltip": null } }, "8b12ad4ee15a4999a6323c776dd16096": { "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 } }, "986d9c59b656475693ecbbdd75175487": { "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_18e9c8a931c94a31a83d9c27c59b450a", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "9e9c519482514c07845295117679cfa6": { "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 } }, "adb9711c02f04541b6a3ab0cf43f6947": { "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_70358ad05a48495eb8391d6100b78401", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "b6e225e3a16e4d409af7c7e8440e4a60": { "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 } }, "b872b7a7adbe4d67a1545f04177c0f9e": { "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_8b12ad4ee15a4999a6323c776dd16096", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "bd39ad7991874d85a461d3bcf11ad3d8": { "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 } }, "ccfa361038cc4700a52070b1714949d5": { "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_44219ee4e58943f5bc586de245f14902", "msg_id": "", "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "635605b944aa42f58a3f6eaca6d7c0ba", "version_major": 2, "version_minor": 0 }, "text/plain": "Output()" }, "metadata": {}, "output_type": "display_data" } ], "tabbable": null, "tooltip": null } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }