{ "cells": [ { "cell_type": "markdown", "id": "3a6a2268", "metadata": {}, "source": [ "# Building POMDPs\n", "In Stormvogel, a **Partially Observable Markov Decision Process (POMDP)** consists of\n", "* states $S$, actions $A$, an initial state $s_0$, a mapping of *enabled actions*, and a successor distribution $P(s,a)$, and a labelling function $L$ as for MDPs,\n", "* a set of observations $Z$,\n", "* and a deterministic state-observation function $O\\colon S \\rightarrow Z$.\n", "\n", "The key idea is that the observations encode what information an agent sees.\n", "An agent will have to make its decisions not based on the current state, but based on the history of observations it has seen.\n", "Note that usually when we refer to MDPs we actually mean *fully observable* MDPs, which are POMDPs with $Z = S$ and $O(s) = s$." ] }, { "cell_type": "markdown", "id": "2279418a", "metadata": {}, "source": [ "We introduce a simple example to illustrate the difference between MDPs and POMDPs.\n", "The idea is that a coin is flipped while the agent is not looking, and then the agent has to guess if it's heads or tails.\n", "We first construct an MDP." ] }, { "cell_type": "code", "execution_count": 1, "id": "3479feea", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:17.809863Z", "iopub.status.busy": "2026-03-26T10:47:17.809630Z", "iopub.status.idle": "2026-03-26T10:47:18.204528Z", "shell.execute_reply": "2026-03-26T10:47:18.203910Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "from stormvogel import *\n", "\n", "init = (\"flip\",)\n", "\n", "\n", "def available_actions(s):\n", " if \"heads\" in s or \"tails\" in s:\n", " return [\"guess_heads\", \"guess_tails\"]\n", " return [\"\"]\n", "\n", "\n", "def delta(s, a):\n", " if s == init:\n", " return [(0.5, (\"heads\",)), (0.5, (\"tails\",))]\n", " elif a.startswith(\"guess\"):\n", " if \"heads\" in s and a == \"guess_heads\" or \"tails\" in s and a == \"guess_tails\":\n", " return [(1, (\"correct\", \"done\"))]\n", " else:\n", " return [(1, (\"wrong\", \"done\"))]\n", " else:\n", " return [(1, s)]\n", "\n", "\n", "labels = lambda s: list(s)\n", "\n", "\n", "def rewards(s, a):\n", " if \"correct\" in s:\n", " return {\"R\": 100}\n", " return {\"R\": 0}\n", "\n", "\n", "coin_mdp = bird.build_bird(\n", " delta=delta,\n", " init=init,\n", " available_actions=available_actions,\n", " labels=labels,\n", " modeltype=ModelType.MDP,\n", " rewards=rewards,\n", ")\n", "vis = show(coin_mdp)" ] }, { "cell_type": "markdown", "id": "1b3e1c39", "metadata": {}, "source": [ "Since this MDP is fully observable, the agent can actually see what state the world is in. In other words, the agent *knows* whether the coin is head or tails. If we ask stormpy to calculate the policy that maximizes the reward, we see that the agent can always 'guess' correctly because of this information. The chosen actions are highlighted in red. (More on model checking later.)" ] }, { "cell_type": "code", "execution_count": 2, "id": "afade764", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:18.211868Z", "iopub.status.busy": "2026-03-26T10:47:18.211559Z", "iopub.status.idle": "2026-03-26T10:47:18.240870Z", "shell.execute_reply": "2026-03-26T10:47:18.240321Z" }, "lines_to_next_cell": 2 }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "result = model_checking(coin_mdp, \"Rmax=? [S]\")\n", "vis3 = show(coin_mdp, result=result)" ] }, { "cell_type": "markdown", "id": "116a6d5f", "metadata": { "lines_to_next_cell": 2 }, "source": [ "To model the fact that our agent does not know the state correctly, we will need to use a POMDP! (Note that we re-use a lot of code from before)" ] }, { "cell_type": "code", "execution_count": 3, "id": "97dff09d", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:18.247676Z", "iopub.status.busy": "2026-03-26T10:47:18.247493Z", "iopub.status.idle": "2026-03-26T10:47:18.275756Z", "shell.execute_reply": "2026-03-26T10:47:18.275155Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "def observations(s):\n", " return 0\n", "\n", "\n", "coin_pomdp = bird.build_bird(\n", " delta=delta,\n", " init=init,\n", " available_actions=available_actions,\n", " labels=labels,\n", " modeltype=ModelType.POMDP,\n", " rewards=rewards,\n", " observations=observations,\n", ")\n", "\n", "vis3 = show(coin_pomdp)" ] }, { "cell_type": "markdown", "id": "2fec3fad", "metadata": {}, "source": [ "Unfortunately, model checking POMDPs turns out to be very hard in general, even undecidable. For this model, the result of model checking would look similar to this. The agent doesn't know if it's currently in the state heads or tails, therefore it just guesses heads and has only a 50 percent chance of winning." ] }, { "cell_type": "code", "execution_count": 4, "id": "c29ce7f3", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:18.282693Z", "iopub.status.busy": "2026-03-26T10:47:18.282503Z", "iopub.status.idle": "2026-03-26T10:47:18.311273Z", "shell.execute_reply": "2026-03-26T10:47:18.310683Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "import stormvogel.result\n", "\n", "taken_actions = {}\n", "for id, state in coin_pomdp.states.items():\n", " taken_actions[id] = state.available_actions()[0]\n", "scheduler2 = stormvogel.result.Scheduler(coin_pomdp, taken_actions)\n", "values = {0: 50, 1: 50, 2: 50, 3: 100.0, 4: 0.0}\n", "result2 = stormvogel.result.Result(coin_pomdp, values, scheduler2)\n", "\n", "vis4 = show(coin_pomdp, result=result2)" ] }, { "cell_type": "markdown", "id": "83534f71", "metadata": { "lines_to_next_cell": 2 }, "source": [ "We can also create stochastic observations. For example, we could say that the agent sees the correct observation with probability 0.8, and the wrong one with probability 0.2.\n", "To make the observations more readable we can give them a valuation." ] }, { "cell_type": "code", "execution_count": 5, "id": "590d415d", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:18.318392Z", "iopub.status.busy": "2026-03-26T10:47:18.318184Z", "iopub.status.idle": "2026-03-26T10:47:18.348838Z", "shell.execute_reply": "2026-03-26T10:47:18.348247Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "def observations_stochastic(s):\n", " if \"heads\" in s:\n", " return [(0.8, 0), (0.2, 1)]\n", " elif \"tails\" in s:\n", " return [(0.2, 0), (0.8, 1)]\n", " else:\n", " return [(1.0, 2)]\n", "\n", "\n", "def observation_valuations(o):\n", " if o == 0:\n", " return {\"heads\": True, \"tails\": False, \"done\": False}\n", " elif o == 1:\n", " return {\"heads\": False, \"tails\": True, \"done\": False}\n", " else:\n", " return {\"done\": True, \"heads\": False, \"tails\": False}\n", "\n", "\n", "coin_pomdp_stochastic = bird.build_bird(\n", " delta=delta,\n", " init=init,\n", " available_actions=available_actions,\n", " labels=labels,\n", " modeltype=ModelType.POMDP,\n", " rewards=rewards,\n", " observations=observations_stochastic,\n", " observation_valuations=observation_valuations,\n", ")\n", "\n", "vis5 = show(coin_pomdp_stochastic)" ] }, { "cell_type": "markdown", "id": "0cff2b12", "metadata": {}, "source": [ "This model cannot be given to stormpy for model checking as is, we first need to determinize the observations." ] }, { "cell_type": "code", "execution_count": 6, "id": "1dfb1a7c", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:18.356086Z", "iopub.status.busy": "2026-03-26T10:47:18.355859Z", "iopub.status.idle": "2026-03-26T10:47:18.427984Z", "shell.execute_reply": "2026-03-26T10:47:18.427429Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "coin_pomdp_stochastic.make_observations_deterministic()\n", "vis6 = show(coin_pomdp_stochastic)" ] } ], "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.13" }, "widgets": { "application/vnd.jupyter.widget-state+json": { "state": { "03791b911d604a46ad04a92e5ff4ed7d": { "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 } }, "05375dc808f7416bbdfc459e355af01d": { "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_0b73cf97862949c2b2e48c603784f53c", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "0b73cf97862949c2b2e48c603784f53c": { "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 } }, "1c885088c2ba4c5ba51418523fe012ae": { "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_45171d1f9d754cab813481b0487bc1cf", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "216b008f0f234d4c808536eb01977cfc": { "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_f9e25f1b1b1a4a408ef0147789de9c3b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "37c37430c055489b96917cb2b626b829": { "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_492349eec0a849a09b0878ce7da653af", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "3d76a30b87a14b08b9d837f9702927d5": { "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_e5fa8474fc674e4580bb5f8d18de130a", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "422dfcc724c544f381113b600577cefc": { "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 } }, "45171d1f9d754cab813481b0487bc1cf": { "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 } }, "492349eec0a849a09b0878ce7da653af": { "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 } }, "4ad9fa7014324f6a8ab78723fdfa895e": { "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 } }, "55d90d5b404542b39d8e619cd53ce75f": { "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_03791b911d604a46ad04a92e5ff4ed7d", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "6aa50c47afe243dd8a228f980c48fa02": { "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_4ad9fa7014324f6a8ab78723fdfa895e", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "7312a37bda924c8f87d9e413ef574e80": { "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 } }, "74be7cef9506451081e3b565bcc03769": { "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_7312a37bda924c8f87d9e413ef574e80", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "90ec55ef7e0d4b80acd090c156e16c76": { "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 } }, "9caeb63ec6e04a3f8b56cf311928474b": { "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 } }, "a0b03e4bf7d4491ebcd9aa20e66c554e": { "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_422dfcc724c544f381113b600577cefc", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "a3ff6b458ed447849ac954b8a5e187eb": { "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_d52bb749a52148d0a4bb05dcbd842cc6", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "c8585a38084f437885fe8afd432f31ce": { "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_90ec55ef7e0d4b80acd090c156e16c76", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "d52bb749a52148d0a4bb05dcbd842cc6": { "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 } }, "de45d5d917b44c319eca83bf73ee3d13": { "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_9caeb63ec6e04a3f8b56cf311928474b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "e5fa8474fc674e4580bb5f8d18de130a": { "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 } }, "f9e25f1b1b1a4a408ef0147789de9c3b": { "model_module": "@jupyter-widgets/base", "model_module_version": "2.0.0", "model_name": "LayoutModel", "state": { "_model_module": "@jupyter-widgets/base", "_model_module_version": "2.0.0", "_model_name": "LayoutModel", "_view_count": null, "_view_module": "@jupyter-widgets/base", "_view_module_version": "2.0.0", "_view_name": "LayoutView", "align_content": null, "align_items": null, "align_self": null, "border_bottom": null, "border_left": null, "border_right": null, "border_top": null, "bottom": null, "display": null, "flex": null, "flex_flow": null, "grid_area": null, "grid_auto_columns": null, "grid_auto_flow": null, "grid_auto_rows": null, "grid_column": null, "grid_gap": null, "grid_row": null, "grid_template_areas": null, "grid_template_columns": null, "grid_template_rows": null, "height": null, "justify_content": null, "justify_items": null, "left": null, "margin": null, "max_height": null, "max_width": null, "min_height": null, "min_width": null, "object_fit": null, "object_position": null, "order": null, "overflow": null, "padding": null, "right": null, "top": null, "visibility": null, "width": null } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }