{ "cells": [ { "cell_type": "markdown", "id": "15723d24", "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": "a105906a", "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": "879cc7cc", "metadata": { "execution": { "iopub.execute_input": "2026-10-01T12:39:15.986631Z", "iopub.status.busy": "2026-10-01T12:39:15.986444Z", "iopub.status.idle": "2026-10-01T12:39:16.576829Z", "shell.execute_reply": "2026-10-01T12:39:16.576273Z" } }, "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": "2354c92f", "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": "2d20645e", "metadata": { "execution": { "iopub.execute_input": "2026-10-01T12:39:16.594314Z", "iopub.status.busy": "2026-10-01T12:39:16.593999Z", "iopub.status.idle": "2026-10-01T12:39:16.620967Z", "shell.execute_reply": "2026-10-01T12:39:16.620394Z" }, "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": "df2dc233", "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": "8cfd4384", "metadata": { "execution": { "iopub.execute_input": "2026-10-01T12:39:16.638160Z", "iopub.status.busy": "2026-10-01T12:39:16.637969Z", "iopub.status.idle": "2026-10-01T12:39:16.664288Z", "shell.execute_reply": "2026-10-01T12:39:16.663730Z" } }, "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 \"unknown\"\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": "71c0517d", "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": "260db743", "metadata": { "execution": { "iopub.execute_input": "2026-10-01T12:39:16.681734Z", "iopub.status.busy": "2026-10-01T12:39:16.681545Z", "iopub.status.idle": "2026-10-01T12:39:16.708213Z", "shell.execute_reply": "2026-10-01T12:39:16.707640Z" } }, "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": "a49e2b11", "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": "a551ba68", "metadata": { "execution": { "iopub.execute_input": "2026-10-01T12:39:16.725956Z", "iopub.status.busy": "2026-10-01T12:39:16.725720Z", "iopub.status.idle": "2026-10-01T12:39:16.756202Z", "shell.execute_reply": "2026-10-01T12:39:16.755658Z" } }, "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, \"heads\"), (0.2, \"tails\")]\n", " elif \"tails\" in s:\n", " return [(0.2, \"heads\"), (0.8, \"tails\")]\n", " else:\n", " return [(1.0, \"done\")]\n", "\n", "\n", "def observation_valuations(o):\n", " heads = Variable(\"heads\")\n", " tails = Variable(\"tails\")\n", " done = Variable(\"done\")\n", " if o == \"heads\":\n", " return {heads: True, tails: False, done: False}\n", " elif o == \"tails\":\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": "0725f583", "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": "3ca7ab30", "metadata": { "execution": { "iopub.execute_input": "2026-10-01T12:39:16.772490Z", "iopub.status.busy": "2026-10-01T12:39:16.772300Z", "iopub.status.idle": "2026-10-01T12:39:16.797966Z", "shell.execute_reply": "2026-10-01T12:39:16.797307Z" } }, "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.15" }, "widgets": { "application/vnd.jupyter.widget-state+json": { "state": { "002feb255f874ae0b58934a0deb89bec": { "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_fb659c91dcff430aa651ed013714d9c2", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "0cee1e3a9d404a6db1d91e49cdccbb5a": { "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 } }, "133933253a1f47049b0b7e7aa8a4692e": { "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_cf69204f64494df4869a87bdcbcef5d5", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "1fc57faeb2754d54824ceeba64000da7": { "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 } }, "2d3385aafcf24c2da6aa580fb770c222": { "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_5e5292052c0946f9a8904f1d650848b5", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "42384d0d4a6348c4bd297260f6213aa7": { "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_b10589bde4cf414289be82ffaeef1ffa", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "44f6cce065ad4dc3aed53d662b8590ff": { "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_ee6d48020f4c49429cfb113bbc5c28b7", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "4c7baa0aa58c46c285792616651522e0": { "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_1fc57faeb2754d54824ceeba64000da7", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "4d1dec73d39e4067a1da8a7102724a5b": { "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 } }, "55481847b79f4418836f3c3d5ed9d9a0": { "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_fe3471e955ae4fa29c4fbe03b06ea27e", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "5e5292052c0946f9a8904f1d650848b5": { "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 } }, "631737ccc7004faf8b63f62f3280a1a3": { "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 } }, "65b6c1db9eac499993d626e0ec217013": { "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 } }, "71f0fd56522b4bc387492dbcc8557e19": { "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_ebc3a517c17249f89d056f0b3195b1fc", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "7f9b2a462c0d4af393224be564a82c96": { "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_4d1dec73d39e4067a1da8a7102724a5b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "920e729be9514133940f6ce80a2f2cff": { "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_0cee1e3a9d404a6db1d91e49cdccbb5a", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "b10589bde4cf414289be82ffaeef1ffa": { "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 } }, "cf69204f64494df4869a87bdcbcef5d5": { "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 } }, "cfd1c548c5de42aaa6ff621c058b870f": { "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_631737ccc7004faf8b63f62f3280a1a3", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "ebc3a517c17249f89d056f0b3195b1fc": { "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 } }, "ee6d48020f4c49429cfb113bbc5c28b7": { "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 } }, "f866f53487024f03ab5e7bb3c8fd3ccb": { "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_65b6c1db9eac499993d626e0ec217013", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "fb659c91dcff430aa651ed013714d9c2": { "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 } }, "fe3471e955ae4fa29c4fbe03b06ea27e": { "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 }