{ "cells": [ { "cell_type": "markdown", "id": "1141da2b", "metadata": {}, "source": [ "# Working with Stormvogel and Stormpy\n", "In this notebook, we will show how to integrate stormvogel and stormpy. Stormvogel has a built in function for model checking that uses stormpy behind the scenes, but you can also use stormpy directly if you want to. In that case, you can convert your model to a stormpy model, do some model checking, and then convert it back to display the results.\n", "We first use the simple study model. The idea is that if you do not study, then you save some time, hence you will gain 15 reward. If you pass the test you get 100 reward because you want to graduate eventually. If you study, then the chance of passing the test becomes higher. Now should you study?" ] }, { "cell_type": "code", "execution_count": 1, "id": "822fbb09", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:43.708037Z", "iopub.status.busy": "2026-07-01T08:29:43.707854Z", "iopub.status.idle": "2026-07-01T08:29:44.370102Z", "shell.execute_reply": "2026-07-01T08:29:44.369559Z" } }, "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", "study = examples.create_study_mdp()\n", "show(study)" ] }, { "cell_type": "markdown", "id": "a5cb31a7", "metadata": {}, "source": [ "Now we let stormpy solve the question whether you should study. Model checking requires a *property string*. This is a string that specifies what result the model checker should aim for. Stormvogel has a graphical interface that makes it easier to create these. Try to create a property that maximizes the reward at the end. The result should be `Rmax=? [F \"end\"]`." ] }, { "cell_type": "code", "execution_count": 2, "id": "2519cae8", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.382204Z", "iopub.status.busy": "2026-07-01T08:29:44.381275Z", "iopub.status.idle": "2026-07-01T08:29:44.384982Z", "shell.execute_reply": "2026-07-01T08:29:44.384352Z" } }, "outputs": [], "source": [ "# build_property_string(study)" ] }, { "cell_type": "markdown", "id": "3dae2af8", "metadata": {}, "source": [ "Now we run our model checking, and then display the result on the model. The action that is chosen to maximize the reward is marked in red. In conclusion, you should study!
\n", "The red action is called the *scheduled action*. The star symbol indicates the *result* of a state. In this case, the result can be seen as the expected reward. The scheduler finds that going to the state with 'didn't study' results in an expected reward of 55, while the state with 'studied' results in an expected value of 90." ] }, { "cell_type": "code", "execution_count": 3, "id": "1367b412", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.386640Z", "iopub.status.busy": "2026-07-01T08:29:44.386477Z", "iopub.status.idle": "2026-07-01T08:29:44.420292Z", "shell.execute_reply": "2026-07-01T08:29:44.419614Z" } }, "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": [ "result = model_checking(\n", " study, 'Rmax=? [F \"end\"]', True\n", ") # true lets it return a scheduler as well\n", "show(study, result=result)" ] }, { "cell_type": "markdown", "id": "52b71a91", "metadata": {}, "source": [ "Now, imagine that the exam is not so important after all. Say you only get 20 reward for passing. Is it still worth studying now? It turns out not to be the case! (The turning point is 30)" ] }, { "cell_type": "code", "execution_count": 4, "id": "e13e5aa7", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.428634Z", "iopub.status.busy": "2026-07-01T08:29:44.428427Z", "iopub.status.idle": "2026-07-01T08:29:44.459938Z", "shell.execute_reply": "2026-07-01T08:29:44.459305Z" } }, "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": [ "study2 = examples.create_study_mdp()\n", "\n", "reward_model = study2.get_rewards(\"R\")\n", "pass_test = next(iter(study2.get_states_with_label(\"pass test\")))\n", "reward_model.set_state_reward(pass_test, 20)\n", "result3 = model_checking(study2, 'Rmax=? [F \"end\"]')\n", "show(study2, result=result3)" ] }, { "cell_type": "markdown", "id": "d4b38144", "metadata": {}, "source": [ "Using the simulator, we can get a path from the scheduler that we found." ] }, { "cell_type": "code", "execution_count": 5, "id": "c19e3b3c", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.468913Z", "iopub.status.busy": "2026-07-01T08:29:44.468689Z", "iopub.status.idle": "2026-07-01T08:29:44.472061Z", "shell.execute_reply": "2026-07-01T08:29:44.471446Z" } }, "outputs": [], "source": [ "from stormvogel.simulator import simulate_path\n", "\n", "path = simulate_path(study2, 5, result3.scheduler)" ] }, { "cell_type": "markdown", "id": "23e04f41", "metadata": {}, "source": [ "Let's do another example with the lion model from before. We want to minimize the chance that it dies. We do this by asking the model checker to minimize the chance of reaching 'dead'. It turns out that our lion is really doomed, it will always die eventually, no matter what it chooses... The result (☆) at the initial state is 1. This means that the probability of the forumula [F \"dead\"] (eventually, the model reaches a state with \"dead\"), is 1." ] }, { "cell_type": "code", "execution_count": 6, "id": "2ea08803", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.473853Z", "iopub.status.busy": "2026-07-01T08:29:44.473665Z", "iopub.status.idle": "2026-07-01T08:29:44.506135Z", "shell.execute_reply": "2026-07-01T08:29:44.505450Z" } }, "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": [ "lion = examples.create_lion_mdp()\n", "result = model_checking(lion, 'Pmin=? [F \"dead\"]', True)\n", "show(lion, result=result)" ] }, { "cell_type": "markdown", "id": "798d4ed5", "metadata": {}, "source": [ "On the other hand, our lion might as well have a good time while it's alive. All a lion really wants is to roar while being full. If it does this, it gets a reward of 100. Let's try to maximize this reward. The scheduler that is found always roars when it's full and hunts otherwise." ] }, { "cell_type": "code", "execution_count": 7, "id": "e3494b53", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.515250Z", "iopub.status.busy": "2026-07-01T08:29:44.515006Z", "iopub.status.idle": "2026-07-01T08:29:44.546831Z", "shell.execute_reply": "2026-07-01T08:29:44.546156Z" } }, "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": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "result2 = model_checking(lion, 'Rmax=? [ F \"dead\" ]', True)\n", "show(lion, result=result2)" ] }, { "cell_type": "markdown", "id": "c508b565", "metadata": {}, "source": [ "Do you remember our Monty Hall model?" ] }, { "cell_type": "code", "execution_count": 8, "id": "c5a68aa9", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.557868Z", "iopub.status.busy": "2026-07-01T08:29:44.557626Z", "iopub.status.idle": "2026-07-01T08:29:44.591265Z", "shell.execute_reply": "2026-07-01T08:29:44.590655Z" } }, "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": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "mdp = examples.create_monty_hall_mdp()\n", "show(mdp)" ] }, { "cell_type": "markdown", "id": "cb4e1797", "metadata": {}, "source": [ "Model checking requires a PRISM property string. In this string, it is specified what property of the model should be used for model checking. In this example, we want a property that maximizes our winning chances.
" ] }, { "cell_type": "code", "execution_count": 9, "id": "e2a1da6e", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.600254Z", "iopub.status.busy": "2026-07-01T08:29:44.600006Z", "iopub.status.idle": "2026-07-01T08:29:44.607228Z", "shell.execute_reply": "2026-07-01T08:29:44.606705Z" } }, "outputs": [], "source": [ "result = model_checking(mdp, 'Pmax=? [F \"target\"]')" ] }, { "cell_type": "code", "execution_count": 10, "id": "632cac3a", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.608987Z", "iopub.status.busy": "2026-07-01T08:29:44.608825Z", "iopub.status.idle": "2026-07-01T08:29:44.641682Z", "shell.execute_reply": "2026-07-01T08:29:44.641101Z" } }, "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": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "show(mdp, result=result)" ] }, { "cell_type": "markdown", "id": "84c90e04", "metadata": {}, "source": [ "Now, the resulting agent chooses to stay when the car is already behind the door, and to switch when it is not. It always wins... This is because in an MDP, the agent always knows where the car is. In order to solve this problem propertly, we would need model checking on POMDPs, unfortunately this is undecidable.\n", "\n", "A possible way to still use MDP model checking to solve this example, is by giving states a label 'should stay' or 'should switch', and then calculate the probablity that you reach such a state.\n", "\n", "Now we have stormpy calculate the probablity that we reach a state where we should switch. It turns out to be 2/3rd (see inital state, ☆). Confirm that this still works if you choose another favorite door." ] }, { "cell_type": "code", "execution_count": 11, "id": "8504bf0d", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.651023Z", "iopub.status.busy": "2026-07-01T08:29:44.650815Z", "iopub.status.idle": "2026-07-01T08:29:44.689908Z", "shell.execute_reply": "2026-07-01T08:29:44.689307Z" }, "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": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "favorite_door = 2 # 0, 1, or 2\n", "new_mdp = examples.create_monty_hall_mdp2()\n", "result = model_checking(\n", " new_mdp,\n", " f'Pmax=? [(((\"init\" | \"carchosen\" | \"o_{favorite_door}\") U \"should_switch\"))]',\n", ")\n", "show(new_mdp, result=result)" ] }, { "cell_type": "markdown", "id": "35aac57a", "metadata": {}, "source": [ "Models can be converted back and forth between stormvogel and stormpy with ease using the `mapping` module.
\n", "This is useful, because this allows you to combine both APIs. For example, you could create a model in stormvogel becuase it has an easy API, do some model checking in stormpy, and then convert it back to display the results. (Note that there is also a direct model checking function available that uses stormpy behind the scenes.)" ] }, { "cell_type": "code", "execution_count": 12, "id": "91bf31d2", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.699299Z", "iopub.status.busy": "2026-07-01T08:29:44.699007Z", "iopub.status.idle": "2026-07-01T08:29:44.728635Z", "shell.execute_reply": "2026-07-01T08:29:44.728036Z" } }, "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": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "\n", "stormvogel_model = examples.create_car_mdp()\n", "show(stormvogel_model)" ] }, { "cell_type": "markdown", "id": "356caaee", "metadata": {}, "source": [ "First, let's convert the stormvogel model to the same model in stormpy." ] }, { "cell_type": "code", "execution_count": 13, "id": "320f7a71", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.738046Z", "iopub.status.busy": "2026-07-01T08:29:44.737842Z", "iopub.status.idle": "2026-07-01T08:29:44.741891Z", "shell.execute_reply": "2026-07-01T08:29:44.741267Z" } }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "-------------------------------------------------------------- \n", "Model type: \tMDP (sparse)\n", "States: \t5\n", "Transitions: \t9\n", "Choices: \t9\n", "Reward Models: none\n", "State Labels: \t6 labels\n", " * red light -> 2 item(s)\n", " * moving -> 2 item(s)\n", " * still -> 2 item(s)\n", " * green light -> 2 item(s)\n", " * accident -> 1 item(s)\n", " * init -> 1 item(s)\n", "Choice Labels: \t3 labels\n", " * wait -> 4 item(s)\n", " * accelerate -> 2 item(s)\n", " * brake -> 2 item(s)\n", "-------------------------------------------------------------- \n", "\n" ] } ], "source": [ "import stormvogel.stormpy_utils.mapping as mapping\n", "\n", "stormpy_model = mapping.stormvogel_to_stormpy(stormvogel_model)\n", "print(stormpy_model)" ] }, { "cell_type": "markdown", "id": "25261343", "metadata": {}, "source": [ "And now we convert it back." ] }, { "cell_type": "code", "execution_count": 14, "id": "2935e736", "metadata": { "execution": { "iopub.execute_input": "2026-07-01T08:29:44.743679Z", "iopub.status.busy": "2026-07-01T08:29:44.743514Z", "iopub.status.idle": "2026-07-01T08:29:44.773865Z", "shell.execute_reply": "2026-07-01T08:29:44.773318Z" } }, "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": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "stormvogel_model2 = mapping.stormpy_to_stormvogel(stormpy_model)\n", "show(stormvogel_model2)" ] } ], "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": { "0065b1655e504f229e758c69eba9a58b": { "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 } }, "11de7694e04841b3849e81c54acdb06b": { "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_dd4790b113204b93b350b5b8b60a843b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "11e620e722ab4283bd9bb89b0f02191a": { "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_3b3cacac4fb74334a0a45d48fac93519", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "2a63f40c066f40e7b9ff945f58f3821f": { "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 } }, "3a30694d58714690b198d0394a37b86c": { "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 } }, "3b3cacac4fb74334a0a45d48fac93519": { "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 } }, "3f9184a60fa942a6b13cd85afbd5cd63": { "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 } }, "46b5b6f9f0da44c3836dfabedd880175": { "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_e218aaa2bd814d73a663575aed1368fd", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "498888c387334f7a9fe6f79a58a930cc": { "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_4f54236d181e4283a39391eab6364287", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "4b16f70c797d4c37a3376c08ae3835b8": { "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 } }, "4ba709b6dc904fbf915152de145d4216": { "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_69266ab27e0c49c5a1bc1d0053072fe1", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "4cb86ae06bb94e5089167ed05a5de083": { "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 } }, "4f54236d181e4283a39391eab6364287": { "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 } }, "5580bec9af364142b0c0df86522a89ed": { "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_4cb86ae06bb94e5089167ed05a5de083", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "593191682c9d4bb7b52dcad60f214568": { "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 } }, "5eb7c8b44b5a44e09c0cd96310c38eca": { "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 } }, "5ed5279369804d0d8a485ddef46d72de": { "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_2a63f40c066f40e7b9ff945f58f3821f", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "5f527eea8966431b9e4cda3ed87982f9": { "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 } }, "6857ee905dda49618bafc7abf1854f1b": { "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_3f9184a60fa942a6b13cd85afbd5cd63", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "69266ab27e0c49c5a1bc1d0053072fe1": { "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 } }, "692d0df4a6634f5d86d49d1ad2cc758b": { "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_5f527eea8966431b9e4cda3ed87982f9", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "6b567b9b1dba4370a17954448315db87": { "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_593191682c9d4bb7b52dcad60f214568", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "7e16519610584fc2a02228b2469f278c": { "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_a2e1128c2cd246bd871ad8accdc757a7", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "95df16ad899a4601bba841acd997a1b8": { "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_dfd5214432e04b53910ce5b75df2d2d0", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "a2e1128c2cd246bd871ad8accdc757a7": { "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 } }, "afc73b87fc4d46fc95861e75f9a8b11a": { "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_cd58517068c44213b9164c64229aa8c7", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "bd71668e61434b78a12d025eff5ea0d1": { "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_be45f397a6f848acbd741ade906a6210", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "be45f397a6f848acbd741ade906a6210": { "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 } }, "cabe3b03d3a540edb7dd144a6861ae9f": { "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_e7cbfd9367514f589d2899c161ab054b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "cd58517068c44213b9164c64229aa8c7": { "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 } }, "d372525bf8eb42f68f36f2cf055af627": { "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_5eb7c8b44b5a44e09c0cd96310c38eca", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "d6057bf47cc1415cab3c9165a8a3c1f6": { "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 } }, "d80a896249cb42828ce0b4daacc229ff": { "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_4b16f70c797d4c37a3376c08ae3835b8", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "dd4790b113204b93b350b5b8b60a843b": { "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 } }, "dfd5214432e04b53910ce5b75df2d2d0": { "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 } }, "e17f5747412742cb943ecfcfdbbafb0f": { "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_0065b1655e504f229e758c69eba9a58b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "e218aaa2bd814d73a663575aed1368fd": { "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 } }, "e7cbfd9367514f589d2899c161ab054b": { "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 } }, "e9f7018fcf024283aaa3491bba85126d": { "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_3a30694d58714690b198d0394a37b86c", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "ed8f67da007f49d68d5160ceb5dde55a": { "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_d6057bf47cc1415cab3c9165a8a3c1f6", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }