{ "cells": [ { "cell_type": "markdown", "id": "5b131b8e", "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": "32d916f3", "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": "e114668f", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:41.287417Z", "iopub.status.busy": "2026-07-01T08:29:41.287231Z", "iopub.status.idle": "2026-07-01T08:29:41.952936Z", "shell.execute_reply": "2026-07-01T08:29:41.952315Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "" ] }, "execution_count": 1, "metadata": {}, "output_type": "execute_result" } ], "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):\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", "show(coin_mdp)" ] }, { "cell_type": "markdown", "id": "c25372c8", "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": "524ff83a", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:41.961757Z", "iopub.status.busy": "2026-07-01T08:29:41.961405Z", "iopub.status.idle": "2026-07-01T08:29:41.990888Z", "shell.execute_reply": "2026-07-01T08:29:41.990315Z" }, "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", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "result = model_checking(coin_mdp, \"Rmax=? [S]\")\n", "show(coin_mdp, result=result)" ] }, { "cell_type": "markdown", "id": "b13eacfc", "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": "ba3b79db", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:41.998732Z", "iopub.status.busy": "2026-07-01T08:29:41.998538Z", "iopub.status.idle": "2026-07-01T08:29:42.027098Z", "shell.execute_reply": "2026-07-01T08:29:42.026486Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "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", "show(coin_pomdp)" ] }, { "cell_type": "markdown", "id": "742377ac", "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": "0353e686", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:42.035104Z", "iopub.status.busy": "2026-07-01T08:29:42.034891Z", "iopub.status.idle": "2026-07-01T08:29:42.063236Z", "shell.execute_reply": "2026-07-01T08:29:42.062620Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "import stormvogel.result\n", "\n", "taken_actions = {}\n", "for i, state in enumerate(coin_pomdp.states):\n", " taken_actions[state] = state.available_actions()[0]\n", "scheduler2 = stormvogel.result.Scheduler(coin_pomdp, taken_actions)\n", "values = {\n", " coin_pomdp.states[0]: 50,\n", " coin_pomdp.states[1]: 50,\n", " coin_pomdp.states[2]: 50,\n", " coin_pomdp.states[3]: 100.0,\n", " coin_pomdp.states[4]: 0.0,\n", "}\n", "result2 = stormvogel.result.Result(coin_pomdp, values, scheduler2)\n", "\n", "show(coin_pomdp, result=result2)" ] }, { "cell_type": "markdown", "id": "5c6c1894", "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": "f349861a", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:42.071559Z", "iopub.status.busy": "2026-07-01T08:29:42.071327Z", "iopub.status.idle": "2026-07-01T08:29:42.102240Z", "shell.execute_reply": "2026-07-01T08:29:42.101548Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "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", " heads = Variable(\"heads\")\n", " tails = Variable(\"tails\")\n", " done = Variable(\"done\")\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", "show(coin_pomdp_stochastic)" ] }, { "cell_type": "markdown", "id": "e3bc03a4", "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": "0ee463d4", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:42.111662Z", "iopub.status.busy": "2026-07-01T08:29:42.111421Z", "iopub.status.idle": "2026-07-01T08:29:42.139721Z", "shell.execute_reply": "2026-07-01T08:29:42.139073Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "coin_pomdp_stochastic.make_observations_deterministic()\n", "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.13.14" }, "widgets": { "application/vnd.jupyter.widget-state+json": { "state": { "026c239b8fbb4bef94923a559f663368": { "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 } }, "03a1f9f92167491495e58f828af553d4": { "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_40d308f175b44628ad253fac742b5e06", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "050c0ef60ebe47648744d3555b966be0": { "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 } }, "058c039acae24c1c817dc2985b5407ee": { "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_caa1c959689f46f484f96c7717223c46", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "13c3947626aa4efd80d5c3a2be2b5e17": { "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 } }, "1910fbdce37a46c3871854f6a9863ad1": { "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_2262b5a76d5d4f919ecebab74698c0e4", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "1b0ad93278284a7cbf7c2c09e6e8fcaa": { "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_3bc4cd743e5d4359a9b9b6999d7e57e5", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "2262b5a76d5d4f919ecebab74698c0e4": { "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 } }, "24238beecdd64126a8252a7e16328c02": { "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 } }, "29e340c397f84c19b7e3e9087c8d3945": { "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_d6d0e25ca48b44adb14863ae365489c2", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "3bc4cd743e5d4359a9b9b6999d7e57e5": { "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 } }, "40d308f175b44628ad253fac742b5e06": { "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 } }, "50cca977e22e4c58bc0d5c83c5248136": { "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_741dff9687e3417ba0edf1255cbfa3af", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "519be5a796b048cf93ba57f903846ff9": { "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_f61775578c8c4f4aafca2e9f9514d8df", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "741dff9687e3417ba0edf1255cbfa3af": { "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 } }, "7431660371d042979149c5a0d7a00a4d": { "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_050c0ef60ebe47648744d3555b966be0", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "93acfca7bf1f407db567502f8ee052f3": { "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_24238beecdd64126a8252a7e16328c02", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "96f0b9975a5d430b8893505fe0ba65e5": { "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_026c239b8fbb4bef94923a559f663368", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "b6bf32dac4244641be90f1803ada74fc": { "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_13c3947626aa4efd80d5c3a2be2b5e17", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "b9e3632c4f024013a4b15988465e6a4e": { "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 } }, "bc916b12d3374de19b7fb8f91a5074f5": { "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_b9e3632c4f024013a4b15988465e6a4e", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "caa1c959689f46f484f96c7717223c46": { "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 } }, "d6d0e25ca48b44adb14863ae365489c2": { "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 } }, "f61775578c8c4f4aafca2e9f9514d8df": { "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 }