From 5007235965d242a6cd82ea2995c048ee0ea34881 Mon Sep 17 00:00:00 2001 From: YouGuessedMyName Date: Tue, 15 Oct 2024 13:10:35 +0200 Subject: [PATCH] fix files --- docs/getting_started/lion.html | 8 +- .../naive_value_iteration.ipynb | 2582 ++++++++--------- 2 files changed, 1295 insertions(+), 1295 deletions(-) diff --git a/docs/getting_started/lion.html b/docs/getting_started/lion.html index 5449353..23826ec 100644 --- a/docs/getting_started/lion.html +++ b/docs/getting_started/lion.html @@ -15,18 +15,18 @@ ></script> <style type="text/css"> #mynetwork { - + width: 590px; height: 406px; border: 1px solid lightgray; - + } </style> </head> <body> <div id="mynetwork"></div> <script type="text/javascript"> - + var nodes = new vis.DataSet([{ id: 0, label: `init`, group: "states", x: -218, y: 28 }, { id: 1, label: `full :D`, group: "states", x: -28, y: 57 }, { id: 2, label: `satisfied :)`, group: "states", x: -79, y: -14 }, @@ -295,4 +295,4 @@ " border:none !important; allowfullscreen webkitallowfullscreen mozallowfullscreen - > \ No newline at end of file + > diff --git a/docs/getting_started/naive_value_iteration.ipynb b/docs/getting_started/naive_value_iteration.ipynb index 2721e85..963ced2 100644 --- a/docs/getting_started/naive_value_iteration.ipynb +++ b/docs/getting_started/naive_value_iteration.ipynb @@ -1,1301 +1,1301 @@ { - "cells": [ - { - "cell_type": "markdown", - "id": "9bdef9ae-fb41-4b72-924b-93077f182178", - "metadata": {}, - "source": [ - "# Naive value iteration, using a hungry lion\n", - "We start by creating a model of a lion. Whenever it gets hungry, it will go hunting and hopefully catch a prey. However, if it fails, it might starve to death..." - ] - }, - { - "cell_type": "code", - "execution_count": 7, - "id": "7f3692d1-ad64-449d-809c-01ceb84e6bb4", - "metadata": {}, - "outputs": [ + "cells": [ + { + "cell_type": "markdown", + "id": "9bdef9ae-fb41-4b72-924b-93077f182178", + "metadata": {}, + "source": [ + "# Naive value iteration, using a hungry lion\n", + "We start by creating a model of a lion. Whenever it gets hungry, it will go hunting and hopefully catch a prey. However, if it fails, it might starve to death..." + ] + }, { - "data": { - "text/html": [ - "\n", - " " + "cell_type": "code", + "execution_count": 7, + "id": "7f3692d1-ad64-449d-809c-01ceb84e6bb4", + "metadata": {}, + "outputs": [ + { + "data": { + "text/html": [ + "\n", + " " + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } ], - "text/plain": [ - "" + "source": [ + "from stormvogel.model import Model, ModelType\n", + "\n", + "lion = Model(name=\"lion\", model_type=ModelType.DTMC)\n", + "init = lion.get_initial_state()\n", + "full = lion.new_state(\"full :D\")\n", + "satisfied = lion.new_state(\"satisfied :)\")\n", + "hungry = lion.new_state(\"hungry :(\")\n", + "starving = lion.new_state(\"starving :((\")\n", + "rawr = lion.new_state(\"rawr\")\n", + "hunt = lion.new_state(\"hunt >:D\")\n", + "desperate_hunt = lion.new_state(\"desparate hunt!\")\n", + "dead = lion.new_state(\"dead...\")\n", + "\n", + "init.set_transitions([(1, satisfied)])\n", + "satisfied.set_transitions([(1, hungry)])\n", + "hungry.set_transitions([(1, hunt)])\n", + "starving.set_transitions([(1, desperate_hunt)])\n", + "hunt.set_transitions([(0.5, full), (0.3, starving), (0.2, satisfied)])\n", + "full.set_transitions([(1, satisfied)])\n", + "desperate_hunt.set_transitions([(0.2, full), (0.3, starving), (0.1, dead), (0.4, satisfied)])\n", + "lion.add_self_loops()\n", + "\n", + "from stormvogel.show import show\n", + "from stormvogel.layout import Layout\n", + "vis = show(lion, layout=Layout(\"layouts/lion.json\"), name=\"lion\", save_and_embed=True)" ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], - "source": [ - "from stormvogel.model import Model, ModelType\n", - "\n", - "lion = Model(name=\"lion\", model_type=ModelType.DTMC)\n", - "init = lion.get_initial_state()\n", - "full = lion.new_state(\"full :D\")\n", - "satisfied = lion.new_state(\"satisfied :)\")\n", - "hungry = lion.new_state(\"hungry :(\")\n", - "starving = lion.new_state(\"starving :((\")\n", - "rawr = lion.new_state(\"rawr\")\n", - "hunt = lion.new_state(\"hunt >:D\")\n", - "desperate_hunt = lion.new_state(\"desparate hunt!\")\n", - "dead = lion.new_state(\"dead...\")\n", - "\n", - "init.set_transitions([(1, satisfied)])\n", - "satisfied.set_transitions([(1, hungry)])\n", - "hungry.set_transitions([(1, hunt)])\n", - "starving.set_transitions([(1, desperate_hunt)])\n", - "hunt.set_transitions([(0.5, full), (0.3, starving), (0.2, satisfied)])\n", - "full.set_transitions([(1, satisfied)])\n", - "desperate_hunt.set_transitions([(0.2, full), (0.3, starving), (0.1, dead), (0.4, satisfied)])\n", - "lion.add_self_loops()\n", - "\n", - "from stormvogel.show import show\n", - "from stormvogel.layout import Layout\n", - "vis = show(lion, layout=Layout(\"layouts/lion.json\"), name=\"lion\", save_and_embed=True)" - ] - }, - { - "cell_type": "markdown", - "id": "1c09fb4a-1fe9-4f76-982a-1eacd0b46a87", - "metadata": {}, - "source": [ - "Here we provide an implementation of naive value iteration using the model API." - ] - }, - { - "cell_type": "code", - "execution_count": 8, - "id": "8807425f-1d69-4522-9077-b902c90bd0b2", - "metadata": {}, - "outputs": [], - "source": [ - "def naive_value_iteration(\n", - " model: stormvogel.model.Model, steps: int, starting_state: stormvogel.model.State\n", - ") -> list[list[float]]:\n", - " \"\"\"Run naive value iteration. The result is a 2D list where result[n][m] is the probability to be in state m at step n.\n", - "\n", - " Args:\n", - " model (stormvogel.model.Model): Target model.\n", - " steps (int): Amount of steps.\n", - " starting_state (stormvogel.model.State): Starting state.\n", - "\n", - " Returns:\n", - " list[list[float]]: The result is a 2D list where result[n][m] is the probability to be in state m at step n.\n", - " \"\"\"\n", - " if steps < 2:\n", - " RuntimeError(\"Need at least two steps\")\n", - " if model.type != stormvogel.model.ModelType.DTMC:\n", - " RuntimeError(\"Only works for DTMC\")\n", - "\n", - " # Create a matrix and set the value for the starting state to 1 on the first step.\n", - " matrix_steps_states = [[0.0 for s in model.states] for x in range(steps)]\n", - " matrix_steps_states[0][starting_state.id] = 1\n", - "\n", - " # Apply the updated values for each step.\n", - " for current_step in range(steps - 1):\n", - " next_step = current_step + 1\n", - " for s_id, s in model.get_states().items():\n", - " branch = model.get_branch(s)\n", - " for transition_prob, target in branch.branch:\n", - " current_prob = matrix_steps_states[current_step][s_id]\n", - " matrix_steps_states[next_step][target.id] += current_prob * float(\n", - " transition_prob\n", - " )\n", - "\n", - " return matrix_steps_states\n", - " " - ] - }, - { - "cell_type": "markdown", - "id": "46c998da-b579-4fc8-b385-7b1b07582359", - "metadata": {}, - "source": [ - "We apply naive value iteration on our lion model with 20 steps. Then we display the result of the as a heatmap, using matplotlib." - ] - }, - { - "cell_type": "code", - "execution_count": 9, - "id": "a606dc3e-5d22-45a2-8234-30d3fe8b6bc5", - "metadata": {}, - "outputs": [ + }, { - "data": { - "image/png": "iVBORw0KGgoAAAANSUhEUgAAA6gAAAGcCAYAAADUNY26AAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjkuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8hTgPZAAAACXBIWXMAAA9hAAAPYQGoP6dpAABO6klEQVR4nO3deVxU9eL/8fcAguyGYIAiuCAu4ZKWpuUSpJaZS7fMKEVNs7Qy08qWq3ZV0qLr0moZLmm2qS12SyVxzSWV1DQ0QzHD1FIQF0A4vz/8Od8IGBbRc9DX8/GYR86Zcz7nPcMyvfmcc8ZmGIYhAAAAAABM5mR2AAAAAAAAJAoqAAAAAMAiKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALMHF7AC4MuXn5+v333+Xt7e3bDab2XEAAAAAmMQwDJ08eVLBwcFycnI8R0pBxSXx+++/KyQkxOwYAAAAACzi4MGDqlWrlsN1KKi4JLy9vSWd/yb08fExOU1hgb6+ZkcAAAAArgqGpLP6v47gCAUVl8SFw3p9fHwsWVA56BgAAAC4vEpz6h8XSQIAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFCvAh07dtSIESNKte7+/ftls9mUnJx8STMBAAAAwD+5mB0Al96iRYtUpUqVUq0bEhKi9PR0+fv7S5KSkpLUqVMnHT9+XNWqVbuEKQEAAABc7SioVwE/P79Sr+vs7KzAwMBLmAYAAAAAisYhvleBvx/iGxYWpkmTJmngwIHy9vZW7dq1NXPmTPu6fz/Ed//+/erUqZMk6ZprrpHNZlNsbKwJzwAAAADA1YCCehWKj49Xq1attG3bNj366KN65JFHlJKSUmi9kJAQffbZZ5KklJQUpaena9q0aUWOmZ2drczMzAI3AAAAACgLCupV6I477tCjjz6q+vXr65lnnpG/v79WrlxZaD1nZ2f74cE1atRQYGCgfH19ixwzLi5Ovr6+9ltISMglfQ4AAAAArjwU1KtQ06ZN7f+22WwKDAzUkSNHLmrMMWPGKCMjw347ePDgxcYEAAAAcJXhIklXoX9e0ddmsyk/P/+ixnRzc5Obm9tFjQEAAADg6sYMKhxydXWVJOXl5ZmcBAAAAMCVjoIKh0JDQ2Wz2fTVV1/p6NGjysrKMjsSAAAAgCsUBRUO1axZU+PHj9ezzz6ra6+9VsOHDzc7EgAAAIArlM0wDMPsELjyZGZmytfXVxkZGfLx8TE7TiGeNpvZEQAAAICrgiHpjFSqbsAMKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAElzMDoArW6Cvr2xmh8AV71SM2QmK5znf7ARFizA7gAM1zQ7gwJNmB3DgBbMDFKOq2QEcCDE7gANhZgdwYKvZASohP7MDOGDln9GjZgeohKz69cyV9Gkp12UGFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUCzIMQ0OGDJGfn59sNpuSk5NLtZ3NZtOSJUskSfv37y/TtgAAAABgNgqqBX3zzTeaPXu2vvrqK6Wnp+u66667LPu9UGov3Ly9vdWkSRMNGzZMe/fuvSwZAAAAAFy9KKgWtG/fPgUFBalt27YKDAyUi4vLZd3/ihUrlJ6erh9//FGTJk3S7t271axZMyUmJl7WHAAAAACuLhRUi4mNjdVjjz2mtLQ02Ww2hYWFSZLCwsI0derUAus2b95c48aNq/AM1atXV2BgoOrWrasePXpoxYoVat26tQYNGqS8vLwK3x8AAAAASBRUy5k2bZpeeukl1apVS+np6dq8efMl29e4cePsBdgRJycnPfHEEzpw4IC2bNlS5DrZ2dnKzMwscAMAAACAsqCgWoyvr6+8vb3l7OyswMBABQQEXLJ9+fv7q169eqVat2HDhpLOn6dalLi4OPn6+tpvISEhFRUTAAAAwFWCgnoVGz58eKnPKzUMQ9L5KwUXZcyYMcrIyLDfDh48WGE5AQAAAFwdLu/Vd1BuTk5O9pJ4QW5u7mXb/+7duyVJderUKfJxNzc3ubm5XbY8AAAAAK48zKBWEgEBAUpPT7ffz8zMVGpq6mXZd35+vqZPn646deqoRYsWl2WfAAAAAK4+FNRK4tZbb9W8efO0Zs0a7dixQ/3795ezs/NFjfn6668rKiqq0PI///xThw8f1q+//qovvvhC0dHR2rRpk2bNmnXR+wQAAACA4nCIbyUxZswYpaam6s4775Svr6/+85//XPQM6rFjx7Rv375Cy6OjoyVJHh4eCg0NVadOnTRz5kzVr1//ovYHAAAAAI7YjH+e2AhUgMzMTPn6+spdUtGXVQIqzqkYsxMUz3O+2QmKFmF2AAdqmh3AgSfNDuDAC2YHKEZVswM4YOXrzYeZHcCBrWYHqIT8zA7ggJV/Ro+aHaASsurXM1fSp5IyMjLk4+PjcF0O8QUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJbgYnYAwAynDMPsCEXytNnMjlApTZtvdoLinYoxO0HR7rfwa3bS7AAOHDU7gAPzzA5QjJlmB3Agx+wADtQ1O4AD15kdoBi7zA5QSQWYHaAS+svsAJXQ2TKsywwqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoF5G48aNU/PmzUu9/syZMxUSEiInJydNnTq1zNsXZf/+/bLZbEpOTi71Nrt27VKtWrV06tSpi9o3AAAAADhCQb1EbDablixZUmDZqFGjlJiYWKrtMzMzNXz4cD3zzDM6dOiQhgwZUqbtK1Ljxo3Vpk0bvfbaa5d93wAAAACuHhTUy8jLy0vVq1cv1bppaWnKzc1Vt27dFBQUJA8PjzJtX9EGDBigt956S+fOnTNl/wAAAACufBTUYnz66aeKjIyUu7u7qlevrujoaPshrps3b9Ztt90mf39/+fr6qkOHDtq6dat927CwMElSr169ZLPZ7Pf/eYhuUlKSbrzxRnl6eqpatWpq166dDhw4oNmzZysyMlKSVLduXdlsNu3fv7/IQ3zfe+89NWrUSFWrVlXDhg315ptvFnh806ZNatGihapWrapWrVpp27Zt5Xo9brvtNv31119atWpVubYHAAAAgJJQUIuQnp6uvn37auDAgdq9e7eSkpLUu3dvGYYhSTp58qT69++vtWvXasOGDQoPD9cdd9yhkydPSjpfYCUpISFB6enp9vt/d+7cOfXs2VMdOnTQ9u3b9f3332vIkCGy2Wzq06ePVqxYIel8wUxPT1dISEihMebPn69///vfmjhxonbv3q1JkybpxRdf1Jw5cyRJWVlZuvPOO9W4cWNt2bJF48aN06hRo0p8/uPGjbOX6gtcXV3VvHlzrVmzpshtsrOzlZmZWeAGAAAAAGXhYnYAK0pPT9e5c+fUu3dvhYaGSpJ9RlOSbr311gLrz5w5U9WqVdOqVat05513KiAgQJJUrVo1BQYGFrmPzMxMZWRk6M4771S9evUkSY0aNbI/fuFQ3oCAgGLHGDt2rOLj49W7d29JUp06dbRr1y6988476t+/vxYsWKD8/HzNmjVLVatWVZMmTfTbb7/pkUcecfj8/f397Zn+Ljg4WAcOHChym7i4OI0fP97huAAAAADgCDOoRWjWrJmioqIUGRmpe+65R++++66OHz9uf/yPP/7Q4MGDFR4eLl9fX/n4+CgrK0tpaWml3oefn59iY2PVpUsXde/eXdOmTVN6enqptz916pT27dunQYMGycvLy36bMGGC9u3bJ0navXu3mjZtqqpVq9q3u+mmm0oce/jw4UVejMnd3V2nT58ucpsxY8YoIyPDfjt48GCpnwsAAAAASBTUIjk7O2v58uX63//+p8aNG2vGjBmKiIhQamqqJKl///5KTk7WtGnTtH79eiUnJ6t69erKyckp034SEhL0/fffq23btvroo4/UoEEDbdiwoVTbZmVlSZLeffddJScn2287d+4s9Rhl9ddff9lnh//Jzc1NPj4+BW4AAAAAUBYU1GLYbDa1a9dO48eP17Zt2+Tq6qrFixdLktatW6fHH39cd9xxh5o0aSI3NzcdO3aswPZVqlRRXl5eiftp0aKFxowZo/Xr1+u6667TggULSpXv2muvVXBwsH799VfVr1+/wK1OnTqSzh8yvH37dp09e9a+3cWU1507d6pFixbl3h4AAAAAHKGgFmHjxo2aNGmSfvjhB6WlpWnRokU6evSo/RzR8PBwzZs3T7t379bGjRsVExMjd3f3AmOEhYUpMTFRhw8fLnB48AWpqakaM2aMvv/+ex04cEDLli3T3r17C5yHWpLx48crLi5O06dP1549e7Rjxw4lJCTYP6/0/vvvl81m0+DBg7Vr1y59/fXXevXVV0sc9/XXX1dUVFSBZfv379ehQ4cUHR1d6nwAAAAAUBYU1CL4+Pho9erVuuOOO9SgQQO98MILio+P1+233y5JmjVrlo4fP67rr79eDz74oB5//HHVqFGjwBjx8fFavny5QkJCipx19PDw0M8//6y7775bDRo00JAhQzRs2DA9/PDDpc750EMP6b333lNCQoIiIyPVoUMHzZ492z6D6uXlpS+//FI7duxQixYt9Pzzz2vy5Mkljnvs2DH7eawXfPjhh+rcubP9olEAAAAAUNFsxoXPTgGKkZOTo/DwcC1YsEDt2rUr1TaZmZny9fWVuyTbpY1XLqcs+m3vabPiq2V9k8wO4MATMWYnKNr9881OULyTZgdw4AGzAzjQyuwAxZhpdgAHynbliMurudkBHPAwO0AxdpkdoJIq+uoicOQvswNUQmclTZSUkZFR4rVqmEFFidLS0vTcc8+VupwCAAAAQHnwOago0YWLLwEAAADApcQMKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLcDE7AGAGT5vN7AhFOmUYZkcollVfM0l6zuwAjsw3O0DRFsSYnaB491v0NZOkD8wOUAkNMTuAAzPNDuBAstkBHGhudoBiNDY7gAO7zA7gwFGzAzgQYHaAYviZHcCBv8wOUAGYQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIF9SJ07NhRI0aMMDvGZZGTk6P69etr/fr1ZkcBAAAAcIWioKJU3n77bdWpU0dt27Y1OwoAAACAKxQF9QqVk5NTYWMZhqHXX39dgwYNqrAxAQAAAOCfKKgXKT8/X08//bT8/PwUGBiocePG2R/bv3+/bDabkpOT7ctOnDghm82mpKQkSVJSUpJsNpsSExPVqlUreXh4qG3btkpJSSmwnwkTJqhGjRry9vbWQw89pGeffVbNmze3Px4bG6uePXtq4sSJCg4OVkREhF566SVdd911hTI3b95cL774Yqmf45YtW7Rv3z5169at1NsAAAAAQFlRUC/SnDlz5OnpqY0bN2rKlCl66aWXtHz58jKP8/zzzys+Pl4//PCDXFxcNHDgQPtj8+fP18SJEzV58mRt2bJFtWvX1ltvvVVojMTERKWkpGj58uX66quvNHDgQO3evVubN2+2r7Nt2zZt375dAwYMKDZLWFhYgaK9Zs0aNWjQQN7e3mV+XgAAAABQWi5mB6jsmjZtqrFjx0qSwsPD9frrrysxMVG33XZbmcaZOHGiOnToIEl69tln1a1bN509e1ZVq1bVjBkzNGjQIHup/Pe//61ly5YpKyurwBienp5677335Orqal/WpUsXJSQk6IYbbpAkJSQkqEOHDqpbt26xWerVqyd/f3/7/QMHDig4ONhh/uzsbGVnZ9vvZ2ZmlvKZAwAAAMB5zKBepKZNmxa4HxQUpCNHjlzUOEFBQZJkHyclJUU33nhjgfX/eV+SIiMjC5RTSRo8eLA+/PBDnT17Vjk5OVqwYEGB2dmiJCYmavjw4fb7Z86cUdWqVR1uExcXJ19fX/stJCTE4foAAAAA8E8U1ItUpUqVAvdtNpvy8/MlSU5O519ewzDsj+fm5pY4js1mkyT7OKXl6elZaFn37t3l5uamxYsX68svv1Rubq7+9a9/lWlcf39/HT9+3OE6Y8aMUUZGhv128ODBMu0DAAAAACiol1BAQIAkKT093b7s7xdMKq2IiIgC55FKKnS/OC4uLurfv78SEhKUkJCg++67T+7u7mXaf4sWLfTzzz8XKNr/5ObmJh8fnwI3AAAAACgLzkG9hNzd3dWmTRu9/PLLqlOnjo4cOaIXXnihzOM89thjGjx4sFq1aqW2bdvqo48+0vbt2x2eR/p3Dz30kBo1aiRJWrduXYnrR0VFqVevXvbDfDt16qSsrCz99NNPRV4VGAAAAAAqAjOol9j777+vc+fOqWXLlhoxYoQmTJhQ5jFiYmI0ZswYjRo1Stdff71SU1MVGxtb4nmhF4SHh6tt27Zq2LChWrduXeL6+/bt07Fjx+z3q1evrl69emn+/Pllzg4AAAAApWUzHB23Ccu67bbbFBgYqHnz5pW4rmEYCg8P16OPPqqRI0eWa3/bt2/Xbbfdpn379snLy6vE9TMzM+Xr6yt3SbZy7fHqdMrCP46eNr6S5THJ7ADFeCLG7ATFu9/Cfws7aXYABx4wO0AxWpkdwIGZZgdwIMfsAA40NztAMTzMDuDALrMDVFIBZgeohP4yO0AxzkqaKCkjI6PEUwE5xLcSOH36tN5++2116dJFzs7O+vDDD7VixYpSfd7q0aNHtXDhQh0+fNjhZ5+WpGnTppo8ebJSU1MVGRlZ7nEAAAAAoDgU1ErAZrPp66+/1sSJE3X27FlFRETos88+U3R0dInb1qhRQ/7+/po5c6auueaai8oRGxt7UdsDAAAAgCMU1ErA3d1dK1asKNe2HMENAAAAoLLgIkkAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALMHF7AAA/o+nzWZ2hEppg9kBHGhjdoBifD3f7ATFO2p2AAd6mB3AgQlmByhGgNkBHHA2O4ADVn7d3jM7QDGqmB3AAStns/LPwWmzA1RCVv1eO1eGdcs1g7p161bt2LHDfv/zzz9Xz5499dxzzyknJ6c8QwIAAAAArnLlKqgPP/yw9uzZI0n69ddfdd9998nDw0OffPKJnn766QoNCAAAAAC4OpSroO7Zs0fNmzeXJH3yySdq3769FixYoNmzZ+uzzz6ryHwAAAAAgKtEuQqqYRjKz8+XJK1YsUJ33HGHJCkkJETHjh2ruHQAAAAAgKtGuQpqq1atNGHCBM2bN0+rVq1St27dJEmpqam69tprKzQgAAAAAODqUK6COnXqVG3dulXDhw/X888/r/r160uSPv30U7Vt27ZCAwIAAAAArg7l+piZpk2bFriK7wWvvPKKnJ2tfLFqAAAAAIBVlWsGVZJOnDih9957T2PGjNFff/0lSdq1a5eOHDlSYeEAAAAAAFePcs2gbt++XVFRUapWrZr279+vwYMHy8/PT4sWLVJaWprmzp1b0TkBAAAAAFe4cs2gjhw5UgMGDNDevXtVtWpV+/I77rhDq1evrrBwAAAAAICrR7kK6ubNm/Xwww8XWl6zZk0dPnz4okMBAAAAAK4+5Sqobm5uyszMLLR8z549CggIuOhQAAAAAICrT7kK6l133aWXXnpJubm5kiSbzaa0tDQ988wzuvvuuys0IAAAAADg6lCughofH6+srCzVqFFDZ86cUYcOHVS/fn15e3tr4sSJFZ3xqjNu3Dg1b97ctP0nJiaqUaNGysvLK7C8ffv2WrBggUmpAAAAAFzpynUVX19fXy1fvlzr1q3Tjz/+qKysLF1//fWKjo6u6HyWEBsbqxMnTmjJkiWXZX+jRo3SY489dln2VZSnn35aL7zwQoHPtP3iiy/0xx9/6L777jMtFwAAAIArW7kK6ty5c9WnTx+1a9dO7dq1sy/PycnRwoUL1a9fvwoLeCXJycmRq6triet5eXnJy8vrMiQqbO3atdq3b1+hQ7WnT5+uAQMGyMmp3B+dCwAAAAAOlattDBgwQBkZGYWWnzx5UgMGDLjoUGb49NNPFRkZKXd3d1WvXl3R0dE6deqUxo0bpzlz5ujzzz+XzWaTzWZTUlKSJOmZZ55RgwYN5OHhobp16+rFF1+0n5cr/d+huu+9957q1KmjqlWraubMmQoODlZ+fn6B/ffo0UMDBw4ssN0FsbGx6tmzp1599VUFBQWpevXqGjZsWIF9paenq1u3bnJ3d1edOnW0YMEChYWFaerUqWV6HRYuXKjbbrutwMcHHT16VN999526d+9eprEAAAAAoCzKNYNqGIZsNluh5b/99pt8fX0vOtTllp6err59+2rKlCnq1auXTp48qTVr1sgwDI0aNUq7d+9WZmamEhISJEl+fn6SJG9vb82ePVvBwcHasWOHBg8eLG9vbz399NP2sX/55Rd99tlnWrRokZydnRUSEqLHHntMK1euVFRUlCTpr7/+0jfffKOvv/662IwrV65UUFCQVq5cqV9++UV9+vRR8+bNNXjwYElSv379dOzYMSUlJalKlSoaOXKkjhw54vB5JyUlqVOnTkpNTVVYWJgkac2aNbr//vsLrLd27Vp5eHioUaNGxY6VnZ2t7Oxs+/2irvIMAAAAAI6UqaC2aNHCPosYFRUlF5f/2zwvL0+pqanq2rVrhYe81NLT03Xu3Dn17t1boaGhkqTIyEj74+7u7srOzlZgYGCB7V544QX7v8PCwjRq1CgtXLiwQEHNycnR3LlzC3z8zu23364FCxbYC+qnn34qf39/derUqdiM11xzjV5//XU5OzurYcOG6tatmxITEzV48GD9/PPPWrFihTZv3qxWrVpJkt577z2Fh4c7fN4eHh6KiIhQlSpV7MsOHDig4ODgAusdOHBA1157rcPDe+Pi4jR+/HiH+wMAAAAAR8pUUHv27ClJSk5OVpcuXQqcJ+nq6qqwsLBK+TEzzZo1U1RUlCIjI9WlSxd17txZ//rXv3TNNdc43O6jjz7S9OnTtW/fPmVlZencuXPy8fEpsE5oaGihz4aNiYnR4MGD9eabb8rNzU3z58/Xfffd57AANmnSpMBFi4KCgrRjxw5JUkpKilxcXHT99dfbH69fv36J+W+88Ub9/PPPBZadOXOmwOG9xS37pzFjxmjkyJH2+5mZmQoJCXG4DQAAAAD8XZkK6tixYyWdny3s06dPiaWlsnB2dtby5cu1fv16LVu2TDNmzNDzzz+vjRs3qk6dOkVu8/333ysmJkbjx49Xly5d5Ovrq4ULFyo+Pr7Aep6enoW27d69uwzD0NKlS3XDDTdozZo1+u9//+sw499nOaXznz37z/NYK4K/v7+OHz9e4rJ/cnNzk5ubW4XnAQAAAHD1KNdFkvr373/FlNMLbDab2rVrp/Hjx2vbtm1ydXXV4sWLJZ2fHf7nZ4KuX79eoaGhev7559WqVSuFh4frwIEDpdpX1apV1bt3b82fP18ffvihIiIiCsx+llVERITOnTunbdu22Zf98ssvJZbKorRo0UK7du0qtOzw4cPlGg8AAAAASqtcBTUvL0+vvvqqbrzxRgUGBsrPz6/ArbLZuHGjJk2apB9++EFpaWlatGiRjh49ar8oUFhYmLZv366UlBQdO3ZMubm5Cg8PV1pamhYuXKh9+/Zp+vTp9kJbGjExMVq6dKnef/99xcTEXFT+hg0bKjo6WkOGDNGmTZu0bds2DRkyRO7u7kVezOqCTZs2qWHDhjp06JB9WZcuXbR27doC67Vo0UL+/v5at27dReUEAAAAAEfKVVDHjx+v1157TX369FFGRoZGjhyp3r17y8nJSePGjavgiJeej4+PVq9erTvuuEMNGjTQCy+8oPj4eN1+++2SpMGDBysiIkKtWrVSQECA1q1bp7vuuktPPvmkhg8frubNm2v9+vV68cUXS73PW2+9VX5+fkpJSSl01dzymDt3rq699lq1b99evXr1sl9R2NFM9+nTp5WSklLg42piYmL0008/KSUlxb7M2dlZAwYM0Pz58y86JwAAAAAUx2YYhlHWjerVq6fp06erW7du8vb2VnJysn3Zhg0btGDBgkuRFWXw22+/KSQkRCtWrLBfLbi0Ro8erczMTL3zzjv2ZYcPH1aTJk20detW+5WOHcnMzJSvr6/cJRU/hwtUjA1mB3CgjdkBinGz2QEcOGp2AAd6mB3AgU/NDlCMgJJXMY1zyauYxsqv20GzAxSjSsmrmMbK2az8c3Da7ACVkFW/185JSpKUkZFR6KKy/1SuGdTDhw/bP4bFy8tLGRkZkqQ777xTS5cuLc+QuEjfffedvvjiC6Wmpmr9+vW67777FBYWpvbt25d5rOeff16hoaEFLsIUGBioWbNmKS0trSJjAwAAAIBduQpqrVq1lJ6eLun8bOqyZcskSZs3b+ZKribJzc3Vc889pyZNmqhXr14KCAhQUlJSoav/lka1atX03HPPFfrYm549e+qWW26pqMgAAAAAUECZPmbmgl69eikxMVGtW7fWY489pgceeMA+u/bkk09WdEaUQpcuXdSlSxezYwAAAABAuZWroL788sv2f/fp00ehoaFav369wsPD1b179woLBwAAAAC4epSroK5evVpt27aVi8v5zdu0aaM2bdro3LlzWr16dbnOewQAAAAAXN3KdQ5qp06d9NdffxVanpGRoU6dOl10KAAAAADA1adcBdUwDNlshT885M8//5Snp+dFhwIAAAAAXH3KdIhv7969JUk2m02xsbEFrtibl5en7du3q23bthWbEAAAAABwVShTQfX19ZV0fgbV29tb7u7u9sdcXV3Vpk0bDR48uGITAgAAAACuCmUqqAkJCZKkgIAAjRs3Th4eHpKk/fv3a8mSJWrUqJH8/f0rPiUAAAAA4IpXrnNQt23bprlz50qSTpw4oTZt2ig+Pl49e/bUW2+9VaEBAQAAAABXh3IX1FtuuUWS9Omnn+raa6/VgQMHNHfuXE2fPr1CAwIAAAAArg7lKqinT5+Wt7e3JGnZsmXq3bu3nJyc1KZNGx04cKBCAwIAAAAArg5lOgf1gvr162vJkiXq1auXvv32Wz355JOSpCNHjsjHx6dCAwJASdqYHaASWmt2gEpqitkBKqFfzQ4AADCdUYZ1yzWD+u9//1ujRo1SWFiYWrdurZtuuknS+dnUFi1alGdIAAAAAMBVzmYYRlkKrd3hw4eVnp6uZs2aycnpfM/dtGmTfHx81LBhwwoNiconMzNTvr6+cpdkMzsMAAAAANMYks5IysjIKPGI23IXVMARCioAAAAAqWwFtVyH+AIAAAAAUNEoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECuoVJCcn55LvIzc395LvAwAAAMDViYJaiXXs2FHDhw/XiBEj5O/vry5duui1115TZGSkPD09FRISokcffVRZWVmSJMMwFBAQoE8//dQ+RvPmzRUUFGS/v3btWrm5uen06dOSJJvNprfeekt33XWXPD09NXHixMv7JAEAAABcNSioldycOXPk6uqqdevW6e2335aTk5OmT5+un376SXPmzNF3332np59+WtL5stm+fXslJSVJko4fP67du3frzJkz+vnnnyVJq1at0g033CAPDw/7PsaNG6devXppx44dGjhwYJE5srOzlZmZWeAGAAAAAGXhYnYAXJzw8HBNmTLFfj8iIsL+77CwME2YMEFDhw7Vm2++Ken8rOs777wjSVq9erVatGihwMBAJSUlqWHDhkpKSlKHDh0K7OP+++/XgAEDHOaIi4vT+PHjK+ppAQAAALgKMYNaybVs2bLA/RUrVigqKko1a9aUt7e3HnzwQf3555/2Q3Y7dOigXbt26ejRo1q1apU6duyojh07KikpSbm5uVq/fr06duxYYMxWrVqVmGPMmDHKyMiw3w4ePFhhzxEAAADA1YGCWsl5enra/71//37deeedatq0qT777DNt2bJFb7zxhqT/u4BSZGSk/Pz8tGrVqgIFddWqVdq8ebNyc3PVtm3bYvdRHDc3N/n4+BS4AQAAAEBZcIjvFWTLli3Kz89XfHy8nJzO/+3h448/LrCOzWbTLbfcos8//1w//fSTbr75Znl4eCg7O1vvvPOOWrVqVapCCgAAAAAVjRnUK0j9+vWVm5urGTNm6Ndff9W8efP09ttvF1qvY8eO+vDDD9W8eXN5eXnJyclJ7du31/z58wudfwoAAAAAlwsF9QrSrFkzvfbaa5o8ebKuu+46zZ8/X3FxcYXW69Chg/Ly8gqca9qxY8dCywAAAADgcrIZhmGYHQJXnszMTPn6+spdks3sMAAAAABMY0g6IykjI6PEa9UwgwoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQXswMAqBxOGYbZEYrlabOZHaHSmWR2AAeeiDE7QfHun292guKdNDtAMR4wO4ADrcwO4MBMswM4kGN2gGI0NzuAAx5mB3Bgl9kBKqEAswNUQmckjSrlusygAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgXqSOHTtqxIgRZscAAAAAgEqPglpJjBs3Ts2bN7/k+0lKSpLNZpPNZpOTk5N8fX3VokULPf3000pPT7/k+wcAAABw9aKgXmGOHj2qs2fPXvQ4KSkp+v3337V582Y988wzWrFiha677jrt2LGjAlICAAAAQGEU1AqQn5+vp59+Wn5+fgoMDNS4cePsj+3fv182m03Jycn2ZSdOnJDNZlNSUpKk/5u1TExMVKtWreTh4aG2bdsqJSVFkjR79myNHz9eP/74o312c/bs2UVm+frrrxUUFKShQ4fq+++/L/dzqlGjhgIDA9WgQQPdd999WrdunQICAvTII4+Ue0wAAAAAcISCWgHmzJkjT09Pbdy4UVOmTNFLL72k5cuXl3mc559/XvHx8frhhx/k4uKigQMHSpL69Omjp556Sk2aNFF6errS09PVp0+fIseIiYnRBx98oOPHj+vWW29VRESEJk2apIMHDxa5fmxsrDp27FhiNnd3dw0dOlTr1q3TkSNHyvzcAAAAAKAkFNQK0LRpU40dO1bh4eHq16+fWrVqpcTExDKPM3HiRHXo0EGNGzfWs88+q/Xr1+vs2bNyd3eXl5eXXFxcFBgYqMDAQLm7uxc5houLi7p166aPPvpIhw8f1qhRo/TNN9+oTp06io6O1rx583TmzBn7+kFBQapdu3ap8jVs2FDS+Vnhf8rOzlZmZmaBGwAAAACUBQW1AjRt2rTA/aCgoHLNMv59nKCgIEm6qNlKX19fDR48WKtXr9b69euVmpqqfv366dtvv7WvExcXp7lz55ZqPMMwJEk2m63QY3FxcfL19bXfQkJCyp0bAAAAwNWJgloBqlSpUuC+zWZTfn6+JMnJ6fxLfKHcSVJubm6J41wogRfGKY+zZ8/qk08+Uffu3XXzzTfL399fb775pqKioso13u7duyVJYWFhhR4bM2aMMjIy7LfiDikGAAAAgOK4mB3gShcQECBJSk9PV4sWLSSpwAWTSsvV1VV5eXklrmcYhtauXau5c+fqk08+kbe3tx544AG98sor9kN0y+PMmTOaOXOm2rdvb39Of+fm5iY3N7dyjw8AAAAAFNRLzN3dXW3atNHLL7+sOnXq6MiRI3rhhRfKPE5YWJhSU1OVnJysWrVqydvbu8hC+MEHH+jhhx9Wr1699PHHHys6Oto+i1uUMWPG6NChQ4UO8z1y5IjOnj2rkydPasuWLZoyZYqOHTumRYsWlTk7AAAAAJQGBfUyeP/99zVo0CC1bNlSERERmjJlijp37lymMe6++24tWrRInTp10okTJ5SQkKDY2NhC60VFRenw4cPy8fEp1bjp6elKS0srtDwiIkI2m01eXl6qW7euOnfurJEjRyowMLBMuQEAAACgtGzG30+OBCpIZmamfH195S6p8CWVUBmdsvCvCs8iLtwFxyaZHcCBJ2LMTlC8++ebnaB4J80OUIwHzA7gQCuzAzgw0+wADuSYHaAYzc0O4ICH2QEc2GV2gEqo8MluKMkZSaMkZWRklDiRxkWSAAAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACW4GJ2AACVg6fNZnaESmmD2QGK0cbsAA58Pd/sBMU7anYAB3qYHaAYE8wO4ECA2QEccDY7gANWfd3eMzuAA1XMDuCAlbNZ9efgtNkBKqFzZViXGVQAAAAAgCVQUAEAAAAAlkBBBQAAAABYAgUVAAAAAGAJFFQAAAAAgCVQUAEAAAAAlkBBBQAAAABYAgUVAAAAAGAJFFQAAAAAgCVQUAEAAAAAlkBBBQAAAABYAgUVAAAAAGAJFFQAAAAAgCVYrqB27NhRI0aMMDuG5dhsNi1ZssTsGAAAAABwyViuoF5JZs+erWrVqpkdo0yK+wNBUlKSbDabTpw4cdkzAQAAALg6UFDLIScnx+wIAAAAAHDFMbWgnjp1Sv369ZOXl5eCgoIUHx9faJ3s7GyNGjVKNWvWlKenp1q3bq2kpCT74wcOHFD37t11zTXXyNPTU02aNNHXX38t6f9m/ZYuXaqmTZuqatWqatOmjXbu3Gnf/s8//1Tfvn1Vs2ZNeXh4KDIyUh9++GGBDB07dtTw4cM1YsQI+fv7q0uXLpKk1157TZGRkfL09FRISIgeffRRZWVl2fc9YMAAZWRkyGazyWazady4caV6TsU5duyYevXqJQ8PD4WHh+uLL76wP1bUbO2SJUtks9ns98eNG6fmzZtr3rx5CgsLk6+vr+677z6dPHlSkhQbG6tVq1Zp2rRp9sz79+8vMRcAAAAAVARTC+ro0aO1atUqff7551q2bJmSkpK0devWAusMHz5c33//vRYuXKjt27frnnvuUdeuXbV3715J0rBhw5Sdna3Vq1drx44dmjx5sry8vArtJz4+Xps3b1ZAQIC6d++u3NxcSdLZs2fVsmVLLV26VDt37tSQIUP04IMPatOmTQXGmDNnjlxdXbVu3Tq9/fbbkiQnJydNnz5dP/30k+bMmaPvvvtOTz/9tCSpbdu2mjp1qnx8fJSenq709HSNGjWqVM+pOOPHj9e9996r7du364477lBMTIz++uuvMr3m+/bt05IlS/TVV1/pq6++0qpVq/Tyyy9LkqZNm6abbrpJgwcPtmcOCQkp0/gAAAAAUF4uZu04KytLs2bN0gcffKCoqChJ50tgrVq17OukpaUpISFBaWlpCg4OliSNGjVK33zzjRISEjRp0iSlpaXp7rvvVmRkpCSpbt26hfY1duxY3XbbbQX2sXjxYt17772qWbOmvThK0mOPPaZvv/1WH3/8sW688Ub78vDwcE2ZMqXAuH8/VzMsLEwTJkzQ0KFD9eabb8rV1VW+vr6y2WwKDAws03MqTmxsrPr27StJmjRpkqZPn65Nmzapa9euDl7pgvLz8zV79mx5e3tLkh588EElJiZq4sSJ8vX1laurqzw8PApkLo3s7GxlZ2fb72dmZpZpewAAAAAwraDu27dPOTk5at26tX2Zn5+fIiIi7Pd37NihvLw8NWjQoMC22dnZql69uiTp8ccf1yOPPKJly5YpOjpad999t5o2bVpg/ZtuuqnQPnbv3i1JysvL06RJk/Txxx/r0KFDysnJUXZ2tjw8PAqM0bJly0LPYcWKFYqLi9PPP/+szMxMnTt3TmfPntXp06cLbV+W51Scvz8vT09P+fj46MiRIw63+aewsDB7OZWkoKCgMo9RlLi4OI0fP/6ixwEAAABw9TKtoJZGVlaWnJ2dtWXLFjk7Oxd47MJhvA899JC6dOmipUuXatmyZYqLi1N8fLwee+yxUu3jlVde0bRp0zR16lT7+aQjRowodCEkT0/PAvf379+vO++8U4888ogmTpwoPz8/rV27VoMGDVJOTk6xBbU0z6k4VapUKXDfZrMpPz9f0vnDjQ3DKPD4hcOYSzvGxRgzZoxGjhxpv5+ZmcnhwQAAAADKxLSCWq9ePVWpUkUbN25U7dq1JUnHjx/Xnj171KFDB0lSixYtlJeXpyNHjuiWW24pdqyQkBANHTpUQ4cO1ZgxY/Tuu+8WKKgbNmwotI9GjRpJktatW6cePXrogQcekHT+ENg9e/aocePGDvNv2bJF+fn5io+Pl5PT+VN5P/744wLruLq6Ki8vr8Cy0j6nsgoICNDJkyd16tQpe5lOTk4u8zhFZZbOXyjqnwX479zc3OTm5lbm/QEAAADABaZdJMnLy0uDBg3S6NGj9d1332nnzp2KjY21lz1JatCggWJiYtSvXz8tWrRIqamp2rRpk+Li4rR06VJJ588D/fbbb5WamqqtW7dq5cqV9vJ5wUsvvaTExET7Pvz9/dWzZ09J588tXb58udavX6/du3fr4Ycf1h9//FFi/vr16ys3N1czZszQr7/+qnnz5tkvnnRBWFiYsrKylJiYqGPHjun06dOlek7l0bp1a3l4eOi5557Tvn37tGDBAs2ePbvM44SFhWnjxo3av3+/jh07Zp9dXbx4sRo2bGi/4i8AAAAAVDRTr+L7yiuv6JZbblH37t0VHR2tm2++udC5ngkJCerXr5+eeuopRUREqGfPntq8ebN9RjQvL0/Dhg1To0aN1LVrVzVo0EBvvvlmgTFefvllPfHEE2rZsqUOHz6sL7/8Uq6urpKkF154Qddff726dOmijh07KjAw0F5eHWnWrJlee+01TZ48Wdddd53mz5+vuLi4Auu0bdtWQ4cOVZ8+fRQQEGC/yFJJz6k8/Pz89MEHH+jrr7+2f1TOhY+1KYtRo0bJ2dlZjRs3VkBAgNLS0iRJGRkZSklJKXJ2FQAAAAAqgs1wdNxmJZeUlKROnTrp+PHjhT4jFJdWZmamfH195S7JVuLawJVrg9kBitHG7AAO3Gx2AAeOmh3AgR5mByjGp2YHcCDA7AAOOJe8imms+rodNDuAA1VKXsU0Vs5m1Z+D02YHqITOSVqn85NePj4+Dtc1dQYVAAAAAIALKKgAAAAAAEuw9MfMXKySrjwLAAAAALAOZlABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWILNMAzD7BC48mRmZsrX11fukmxmhwFQiJ/ZASopV7MDOFDF7ADF8DY7gAPOZgdwwKpfT8m62aqaHcABq75mkrV/r7mZHaAYVn7NrPq9liNptqSMjAz5+Pg4XJcZVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQLaZjx44aMWJEpd8HAAAAAJQVBRUAAAAAYAkUVAAAAACAJVBQTXTq1Cn169dPXl5eCgoKUnx8fIHHs7OzNWrUKNWsWVOenp5q3bq1kpKS7I//+eef6tu3r2rWrCkPDw9FRkbqww8/LNM+AAAAAMAqKKgmGj16tFatWqXPP/9cy5YtU1JSkrZu3Wp/fPjw4fr++++1cOFCbd++Xffcc4+6du2qvXv3SpLOnj2rli1baunSpdq5c6eGDBmiBx98UJs2bSr1PipKdna2MjMzC9wAAAAAoCxshmEYZoe4GmVlZal69er64IMPdM8990iS/vrrL9WqVUtDhgzRyJEjVbduXaWlpSk4ONi+XXR0tG688UZNmjSpyHHvvPNONWzYUK+++mqJ+5g6dWqFPZ9x48Zp/PjxhZa7S7JV2F4AVBQ/swNUUq5mB3CgitkBiuFtdgAHnM0O4IBVv56SdbNVNTuAA1Z9zSRr/15zMztAMaz8mln1ey1H0mxJGRkZ8vHxcbiuy+UIhML27dunnJwctW7d2r7Mz89PERERkqQdO3YoLy9PDRo0KLBddna2qlevLknKy8vTpEmT9PHHH+vQoUPKyclRdna2PDw8SrWPijRmzBiNHDnSfj8zM1MhISEVvh8AAAAAVy4KqkVlZWXJ2dlZW7ZskbNzwb/xenl5SZJeeeUVTZs2TVOnTlVkZKQ8PT01YsQI5eTkXPa8bm5ucnOz6t+5AAAAAFQGnINqknr16qlKlSrauHGjfdnx48e1Z88eSVKLFi2Ul5enI0eOqH79+gVugYGBkqR169apR48eeuCBB9SsWTPVrVvXvn1p9gEAAAAAVkJBNYmXl5cGDRqk0aNH67vvvtPOnTsVGxsrJ6fzX5IGDRooJiZG/fr106JFi5SamqpNmzYpLi5OS5culSSFh4dr+fLlWr9+vXbv3q2HH35Yf/zxR6n3ccGYMWPUr18/+/1NmzapYcOGOnTokH1ZVFSUXn/99Uv5kgAAAAC4ynGIr4leeeUVZWVlqXv37vL29tZTTz2ljIwM++MJCQmaMGGCnnrqKR06dEj+/v5q06aN7rzzTknSCy+8oF9//VVdunSRh4eHhgwZop49exYYo6R9SFJ6errS0tLs90+fPq2UlBTl5ubal+3bt0/Hjh27VC8FAAAAAHAVX1wamZmZ8vX15Sq+gEVxFd/y4cqNZcdVfMvHql9PybrZuIpv+Vj595pVr25i5dfMqt9rZbmKL4f4AgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS3AxOwCuTIZhnP+vyTkAFC3f7ACVlJVftzyzAxTDqrkka79H2cwO4IBVs+WaHaCSsurXU2ImrTys+nst5///90JHcISCikvi5MmTkqSzJucAULQzZgcAAABXnZMnT8rX19fhOjajNDUWKKP8/Hz9/vvv8vb2ls128X+by8zMVEhIiA4ePCgfH58KSFhxrJrNqrkkspWXVbNZNZdEtvKyajar5pLIVl5WzWbVXBLZysuq2ayaS6rYbIZh6OTJkwoODpaTk+O5cWZQcUk4OTmpVq1aFT6uj4+P5X54L7BqNqvmkshWXlbNZtVcEtnKy6rZrJpLIlt5WTWbVXNJZCsvq2azai6p4rKVNHN6AYd2AwAAAAAsgYIKAAAAALAECioqBTc3N40dO1Zubm5mRynEqtmsmksiW3lZNZtVc0lkKy+rZrNqLols5WXVbFbNJZGtvKyazaq5JPOycZEkAAAAAIAlMIMKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgwvLeeOMNhYWFqWrVqmrdurU2bdpkdiRJ0urVq9W9e3cFBwfLZrNpyZIlZkeSJMXFxemGG26Qt7e3atSooZ49eyolJcXsWJKkt956S02bNrV/ntZNN92k//3vf2bHKuTll1+WzWbTiBEjzI6icePGyWazFbg1bNjQ7Fh2hw4d0gMPPKDq1avL3d1dkZGR+uGHH8yOpbCwsEKvm81m07Bhw0zNlZeXpxdffFF16tSRu7u76tWrp//85z+yyuUgTp48qREjRig0NFTu7u5q27atNm/efNlzlPT71TAM/fvf/1ZQUJDc3d0VHR2tvXv3WiLbokWL1LlzZ1WvXl02m03JycmXJVdJ2XJzc/XMM88oMjJSnp6eCg4OVr9+/fT777+bmks6/3uuYcOG8vT01DXXXKPo6Ght3LjxkucqTba/Gzp0qGw2m6ZOnWqJbLGxsYV+x3Xt2tX0XJK0e/du3XXXXfL19ZWnp6duuOEGpaWlmZ6tqPcFm82mV155xfRsWVlZGj58uGrVqiV3d3c1btxYb7/99iXPVZpsf/zxh2JjYxUcHCwPDw917dr1kv7OpaDC0j766CONHDlSY8eO1datW9WsWTN16dJFR44cMTuaTp06pWbNmumNN94wO0oBq1at0rBhw7RhwwYtX75cubm56ty5s06dOmV2NNWqVUsvv/yytmzZoh9++EG33nqrevTooZ9++snsaHabN2/WO++8o6ZNm5odxa5JkyZKT0+339auXWt2JEnS8ePH1a5dO1WpUkX/+9//tGvXLsXHx+uaa64xO5o2b95c4DVbvny5JOmee+4xNdfkyZP11ltv6fXXX9fu3bs1efJkTZkyRTNmzDA11wUPPfSQli9frnnz5mnHjh3q3LmzoqOjdejQocuao6Tfr1OmTNH06dP19ttva+PGjfL09FSXLl109uxZ07OdOnVKN998syZPnnzJsxS17+KynT59Wlu3btWLL76orVu3atGiRUpJSdFdd91lai5JatCggV5//XXt2LFDa9euVVhYmDp37qyjR4+anu2CxYsXa8OGDQoODr7kmS4oTbauXbsW+F334Ycfmp5r3759uvnmm9WwYUMlJSVp+/btevHFF1W1alXTs/39tUpPT9f7778vm82mu+++2/RsI0eO1DfffKMPPvhAu3fv1ogRIzR8+HB98cUXpmYzDEM9e/bUr7/+qs8//1zbtm1TaGiooqOjL93/WxqAhd14443GsGHD7Pfz8vKM4OBgIy4uzsRUhUkyFi9ebHaMIh05csSQZKxatcrsKEW65pprjPfee8/sGIZhGMbJkyeN8PBwY/ny5UaHDh2MJ554wuxIxtixY41mzZqZHaNIzzzzjHHzzTebHaNUnnjiCaNevXpGfn6+qTm6detmDBw4sMCy3r17GzExMSYl+j+nT582nJ2dja+++qrA8uuvv954/vnnTUpV+Pdrfn6+ERgYaLzyyiv2ZSdOnDDc3NyMDz/80NRsf5eammpIMrZt23ZZM11QmvelTZs2GZKMAwcOXJ5QRulyZWRkGJKMFStWXJ5Q/19x2X777TejZs2axs6dO43Q0FDjv//972XNVVy2/v37Gz169LjsWf6uqFx9+vQxHnjgAXMC/U1pvtd69Ohh3HrrrZcn0N8Ula1JkybGSy+9VGCZGb9//5ktJSXFkGTs3LnTviwvL88ICAgw3n333UuSgRlUWFZOTo62bNmi6Oho+zInJydFR0fr+++/NzFZ5ZKRkSFJ8vPzMzlJQXl5eVq4cKFOnTqlm266yew4kqRhw4apW7duBb7nrGDv3r0KDg5W3bp1FRMTc1kOkyqNL774Qq1atdI999yjGjVqqEWLFnr33XfNjlVITk6OPvjgAw0cOFA2m83ULG3btlViYqL27NkjSfrxxx+1du1a3X777abmkqRz584pLy+v0CyHu7u7ZWbtJSk1NVWHDx8u8HPq6+ur1q1b895QRhkZGbLZbKpWrZrZUexycnI0c+ZM+fr6qlmzZmbHUX5+vh588EGNHj1aTZo0MTtOIUlJSapRo4YiIiL0yCOP6M8//zQ1T35+vpYuXaoGDRqoS5cuqlGjhlq3bm2Z06D+7o8//tDSpUs1aNAgs6NIOv/+8MUXX+jQoUMyDEMrV67Unj171LlzZ1NzZWdnS1KB9wYnJye5ubldsvcGCios69ixY8rLy9O1115bYPm1116rw4cPm5SqcsnPz9eIESPUrl07XXfddWbHkSTt2LFDXl5ecnNz09ChQ7V48WI1btzY7FhauHChtm7dqri4OLOjFNC6dWvNnj1b33zzjd566y2lpqbqlltu0cmTJ82Opl9//VVvvfWWwsPD9e233+qRRx7R448/rjlz5pgdrYAlS5boxIkTio2NNTuKnn32Wd13331q2LChqlSpohYtWmjEiBGKiYkxO5q8vb1100036T//+Y9+//135eXl6YMPPtD333+v9PR0s+PZXfj9z3vDxTl79qyeeeYZ9e3bVz4+PmbH0VdffSUvLy9VrVpV//3vf7V8+XL5+/ubHUuTJ0+Wi4uLHn/8cbOjFNK1a1fNnTtXiYmJmjx5slatWqXbb79deXl5pmU6cuSIsrKy9PLLL6tr165atmyZevXqpd69e2vVqlWm5SrKnDlz5O3trd69e5sdRZI0Y8YMNW7cWLVq1ZKrq6u6du2qN954Q+3btzc1V8OGDVW7dm2NGTNGx48fV05OjiZPnqzffvvtkr03uFySUQFYwrBhw7Rz505LzX5EREQoOTlZGRkZ+vTTT9W/f3+tWrXK1JJ68OBBPfHEE1q+fPllOUemLP4+s9a0aVO1bt1aoaGh+vjjj03/q29+fr5atWqlSZMmSZJatGihnTt36u2331b//v1NzfZ3s2bN0u23335Zzx0rzscff6z58+drwYIFatKkiZKTkzVixAgFBwdb4jWbN2+eBg4cqJo1a8rZ2VnXX3+9+vbtqy1btpgdDRUoNzdX9957rwzD0FtvvWV2HElSp06dlJycrGPHjundd9/Vvffeq40bN6pGjRqmZdqyZYumTZumrVu3mn70RVHuu+8++78jIyPVtGlT1atXT0lJSYqKijIlU35+viSpR48eevLJJyVJzZs31/r16/X222+rQ4cOpuQqyvvvv6+YmBjLvO/PmDFDGzZs0BdffKHQ0FCtXr1aw4YNU3BwsKlHdlWpUkWLFi3SoEGD5OfnJ2dnZ0VHR+v222+/ZBf4YwYVluXv7y9nZ2f98ccfBZb/8ccfCgwMNClV5TF8+HB99dVXWrlypWrVqmV2HDtXV1fVr19fLVu2VFxcnJo1a6Zp06aZmmnLli06cuSIrr/+erm4uMjFxUWrVq3S9OnT5eLiYupfo/+pWrVqatCggX755RezoygoKKjQHxYaNWpkmUOQJenAgQNasWKFHnroIbOjSJJGjx5tn0WNjIzUgw8+qCeffNIyM/f16tXTqlWrlJWVpYMHD2rTpk3Kzc1V3bp1zY5md+H3P+8N5XOhnB44cEDLly+3xOypJHl6eqp+/fpq06aNZs2aJRcXF82aNcvUTGvWrNGRI0dUu3Zt+3vDgQMH9NRTTyksLMzUbEWpW7eu/P39TX1/8Pf3l4uLi+XfG9asWaOUlBTLvDecOXNGzz33nF577TV1795dTZs21fDhw9WnTx+9+uqrZsdTy5YtlZycrBMnTig9PV3ffPON/vzzz0v23kBBhWW5urqqZcuWSkxMtC/Lz89XYmKiZc5ZtCLDMDR8+HAtXrxY3333nerUqWN2JIfy8/Pt5zeYJSoqSjt27FBycrL91qpVK8XExCg5OVnOzs6m5vu7rKws7du3T0FBQWZHUbt27Qp9hNGePXsUGhpqUqLCEhISVKNGDXXr1s3sKJLOX0nVyangW6+zs7N91sEqPD09FRQUpOPHj+vbb79Vjx49zI5kV6dOHQUGBhZ4b8jMzNTGjRt5byjBhXK6d+9erVixQtWrVzc7UrGs8N7w4IMPavv27QXeG4KDgzV69Gh9++23pmYrym+//aY///zT1PcHV1dX3XDDDZZ/b5g1a5ZatmxpifOcpfM/m7m5uZZ/f/D19VVAQID27t2rH3744ZK9N3CILyxt5MiR6t+/v1q1aqUbb7xRU6dO1alTpzRgwACzoykrK6vAXylTU1OVnJwsPz8/1a5d27Rcw4YN04IFC/T555/L29vbfk6Wr6+v3N3dTcslSWPGjNHtt9+u2rVr6+TJk1qwYIGSkpJMf6P39vYudI6up6enqlevbvq5u6NGjVL37t0VGhqq33//XWPHjpWzs7P69u1rai5JevLJJ9W2bVtNmjRJ9957rzZt2qSZM2dq5syZZkeTdP5/cBMSEtS/f3+5uFjj7a579+6aOHGiateurSZNmmjbtm167bXXNHDgQLOjSZK+/fZbGYahiIgI/fLLLxo9erQaNmx42X/nlvT7dcSIEZowYYLCw8NVp04dvfjiiwoODlbPnj1Nz/bXX38pLS3N/vmiF/5HPTAw8JLP8DrKFhQUpH/961/aunWrvvrqK+Xl5dnfH/z8/OTq6mpKrurVq2vixIm66667FBQUpGPHjumNN97QoUOHLsvHQpX09fxnia9SpYoCAwMVERFhajY/Pz+NHz9ed999twIDA7Vv3z49/fTTql+/vrp06WJartq1a2v06NHq06eP2rdvr06dOumbb77Rl19+qaSkpEuaqzTZpPN/0Prkk08UHx9/yfOUJVuHDh00evRoubu7KzQ0VKtWrdLcuXP12muvmZ7tk08+UUBAgGrXrq0dO3boiSeeUM+ePS/dBZwuybWBgQo0Y8YMo3bt2oarq6tx4403Ghs2bDA7kmEYhrFy5UpDUqFb//79Tc1VVCZJRkJCgqm5DMMwBg4caISGhhqurq5GQECAERUVZSxbtszsWEWyysfM9OnTxwgKCjJcXV2NmjVrGn369DF++eUXs2PZffnll8Z1111nuLm5GQ0bNjRmzpxpdiS7b7/91pBkpKSkmB3FLjMz03jiiSeM2rVrG1WrVjXq1q1rPP/880Z2drbZ0QzDMIyPPvrIqFu3ruHq6moEBgYaw4YNM06cOHHZc5T0+zU/P9948cUXjWuvvdZwc3MzoqKiLtvXuaRsCQkJRT4+duxYU7Nd+Nibom4rV640LdeZM2eMXr16GcHBwYarq6sRFBRk3HXXXcamTZsuaabSZCvK5fyYGUfZTp8+bXTu3NkICAgwqlSpYoSGhhqDBw82Dh8+bGquC2bNmmXUr1/fqFq1qtGsWTNjyZIllzxXabO98847hru7+2X/3VZStvT0dCM2NtYIDg42qlatakRERBjx8fGX5ePRSso2bdo0o1atWkaVKlWM2rVrGy+88MIlfd+yGcYlOrsVAAAAAIAy4BxUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAECZxcbGqmfPnmbHAABcYSioAAAAAABLoKACAIBiffrpp4qMjJS7u7uqV6+u6OhojR49WnPmzNHnn38um80mm82mpKQkSdLBgwd17733qlq1avLz81OPHj20f/9++3gXZl7Hjx+vgIAA+fj4aOjQocrJyXG4z1OnTl3mZw4AMIOL2QEAAIA1paenq2/fvpoyZYp69eqlkydPas2aNerXr5/S0tKUmZmphIQESZKfn59yc3PVpUsX3XTTTVqzZo1cXFw0YcIEde3aVdu3b5erq6skKTExUVWrVlVSUpL279+vAQMGqHr16po4cWKx+zQMw8yXAgBwmVBQAQBAkdLT03Xu3Dn17t1boaGhkqTIyEhJkru7u7KzsxUYGGhf/4MPPlB+fr7ee+892Ww2SVJCQoKqVaumpKQkde7cWZLk6uqq999/Xx4eHmrSpIleeukljR49Wv/5z38c7hMAcOXjEF8AAFCkZs2aKSoqSpGRkbrnnnv07rvv6vjx48Wu/+OPP+qXX36Rt7e3vLy85OXlJT8/P509e1b79u0rMK6Hh4f9/k033aSsrCwdPHiwzPsEAFxZKKgAAKBIzs7OWr58uf73v/+pcePGmjFjhiIiIpSamlrk+llZWWrZsqWSk5ML3Pbs2aP777//kuwTAHBloaACAIBi2Ww2tWvXTuPHj9e2bdvk6uqqxYsXy9XVVXl5eQXWvf7667V3717VqFFD9evXL3Dz9fW1r/fjjz/qzJkz9vsbNmyQl5eXQkJCHO4TAHDlo6ACAIAibdy4UZMmTdIPP/ygtLQ0LVq0SEePHlWjRo0UFham7du3KyUlRceOHVNubq5iYmLk7++vHj16aM2aNUpNTVVSUpIef/xx/fbbb/Zxc3JyNGjQIO3atUtff/21xo4dq+HDh8vJycnhPgEAVz4ukgQAAIrk4+Oj1atXa+rUqcrMzFRoaKji4+N1++23q1WrVkpKSlKrVq2UlZWllStXqmPHjlq9erWeeeYZ9e7dWydPnlTNmjUVFRUlHx8f+7hRUVEKDw9X+/btlZ2drb59+2rcuHEl7hMAcOWzGVy3HQAAXCaxsbE6ceKElixZYnYUAIAFcYgvAAAAAMASKKgAAAAAAEvgEF8AAAAAgCUwgwoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsIT/Bx4Dd9RnuY5WAAAAAElFTkSuQmCC", - "text/plain": [ - "
" + "cell_type": "markdown", + "id": "1c09fb4a-1fe9-4f76-982a-1eacd0b46a87", + "metadata": {}, + "source": [ + "Here we provide an implementation of naive value iteration using the model API." ] - }, - "metadata": {}, - "output_type": "display_data" - } - ], - "source": [ - "res = naive_value_iteration(lion, 20, starting_state=lion.get_initial_state())\n", - "labels = [s.labels[0] for s in lion.get_states().values()]\n", - "stormvogel.lib.display_value_iteration_result(res, 10, labels)" - ] - }, - { - "cell_type": "markdown", - "id": "dcbef4f2-78ae-4d2c-9587-9c96becf26b1", - "metadata": {}, - "source": [ - "Note that naive_value_iteration is also available under stormvogel.lib, in case you would like to use it later. However, this implementation is very inefficient so we recommend using the value iteration algorithms from stormpy if you want good performance." - ] - }, - { - "cell_type": "code", - "execution_count": 10, - "id": "12b57306-780c-4a40-898a-f3a95f7ff9eb", - "metadata": {}, - "outputs": [], - "source": [ - "import stormvogel.lib\n", - "res2 = stormvogel.lib.naive_value_iteration(lion, 20, starting_state=lion.get_initial_state())\n", - "assert res == res2" - ] - } - ], - "metadata": { - "kernelspec": { - "display_name": "Python 3 (ipykernel)", - "language": "python", - "name": "python3" - }, - "language_info": { - "codemirror_mode": { - "name": "ipython", - "version": 3 - }, - "file_extension": ".py", - "mimetype": "text/x-python", - "name": "python", - "nbconvert_exporter": "python", - "pygments_lexer": "ipython3", - "version": "3.12.3" - }, - "widgets": { - "application/vnd.jupyter.widget-state+json": { - "state": { - "0a4470793a704b388de44c9e5f08cab8": { - "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_47da0120652c4fa4a503c52d24ee2ebc", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "115e6973c59145688509e9aa5b3010ee": { - "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 - } - }, - "132eeaf7259c4ae6b2349f17d38d49c5": { - "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 - } - }, - "3b27b22ad54446db888d0366e93642b8": { - "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 - } - }, - "3c635914241b444ab49f98bbb3c218d1": { - "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 - } - }, - "47da0120652c4fa4a503c52d24ee2ebc": { - "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 - } - }, - "52791b15670e460ba9fe9376b20cc3a8": { - "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 - } - }, - "55fa0e096dad48d992e69289fe7fdc70": { - "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_132eeaf7259c4ae6b2349f17d38d49c5", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "6c0870de174f4ed69adc6b138d5373f2": { - "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_fe8c1c71cc404d5ca3dd56ed41caf8f0", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "774c3e64c51b44d48f82a07fc88b0ac8": { - "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_ef9ef09005ec4e8a9446a35f87253aa9", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "8c26ed794da84acc93a5a7e7928b5f8c": { - "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_115e6973c59145688509e9aa5b3010ee", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "b2feb830225a4cecb139b0703c658564": { - "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 - } - }, - "b422eb4441534debb7226a46affd3242": { - "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_eaecb40d41574cf282cbba8e83608fb3", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "c22dda8a4057465c8f1af23376ed2936": { - "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 - } - }, - "c2b9fda9e1354d6ca57827715ca601ed": { - "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_52791b15670e460ba9fe9376b20cc3a8", - "msg_id": "", - "outputs": [ + }, + { + "cell_type": "code", + "execution_count": 8, + "id": "8807425f-1d69-4522-9077-b902c90bd0b2", + "metadata": {}, + "outputs": [], + "source": [ + "def naive_value_iteration(\n", + " model: stormvogel.model.Model, steps: int, starting_state: stormvogel.model.State\n", + ") -> list[list[float]]:\n", + " \"\"\"Run naive value iteration. The result is a 2D list where result[n][m] is the probability to be in state m at step n.\n", + "\n", + " Args:\n", + " model (stormvogel.model.Model): Target model.\n", + " steps (int): Amount of steps.\n", + " starting_state (stormvogel.model.State): Starting state.\n", + "\n", + " Returns:\n", + " list[list[float]]: The result is a 2D list where result[n][m] is the probability to be in state m at step n.\n", + " \"\"\"\n", + " if steps < 2:\n", + " RuntimeError(\"Need at least two steps\")\n", + " if model.type != stormvogel.model.ModelType.DTMC:\n", + " RuntimeError(\"Only works for DTMC\")\n", + "\n", + " # Create a matrix and set the value for the starting state to 1 on the first step.\n", + " matrix_steps_states = [[0.0 for s in model.states] for x in range(steps)]\n", + " matrix_steps_states[0][starting_state.id] = 1\n", + "\n", + " # Apply the updated values for each step.\n", + " for current_step in range(steps - 1):\n", + " next_step = current_step + 1\n", + " for s_id, s in model.get_states().items():\n", + " branch = model.get_branch(s)\n", + " for transition_prob, target in branch.branch:\n", + " current_prob = matrix_steps_states[current_step][s_id]\n", + " matrix_steps_states[next_step][target.id] += current_prob * float(\n", + " transition_prob\n", + " )\n", + "\n", + " return matrix_steps_states\n", + " " + ] + }, + { + "cell_type": "markdown", + "id": "46c998da-b579-4fc8-b385-7b1b07582359", + "metadata": {}, + "source": [ + "We apply naive value iteration on our lion model with 20 steps. Then we display the result of the as a heatmap, using matplotlib." + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "id": "a606dc3e-5d22-45a2-8234-30d3fe8b6bc5", + "metadata": {}, + "outputs": [ { - "data": { - "text/html": "\n ", - "text/plain": "" - }, - "metadata": {}, - "output_type": "display_data" + "data": { + "image/png": "iVBORw0KGgoAAAANSUhEUgAAA6gAAAGcCAYAAADUNY26AAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjkuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8hTgPZAAAACXBIWXMAAA9hAAAPYQGoP6dpAABO6klEQVR4nO3deVxU9eL/8fcAguyGYIAiuCAu4ZKWpuUSpJaZS7fMKEVNs7Qy08qWq3ZV0qLr0moZLmm2qS12SyVxzSWV1DQ0QzHD1FIQF0A4vz/8Od8IGBbRc9DX8/GYR86Zcz7nPcMyvfmcc8ZmGIYhAAAAAABM5mR2AAAAAAAAJAoqAAAAAMAiKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALMHF7AC4MuXn5+v333+Xt7e3bDab2XEAAAAAmMQwDJ08eVLBwcFycnI8R0pBxSXx+++/KyQkxOwYAAAAACzi4MGDqlWrlsN1KKi4JLy9vSWd/yb08fExOU1hgb6+ZkcAAAAArgqGpLP6v47gCAUVl8SFw3p9fHwsWVA56BgAAAC4vEpz6h8XSQIAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFCvAh07dtSIESNKte7+/ftls9mUnJx8STMBAAAAwD+5mB0Al96iRYtUpUqVUq0bEhKi9PR0+fv7S5KSkpLUqVMnHT9+XNWqVbuEKQEAAABc7SioVwE/P79Sr+vs7KzAwMBLmAYAAAAAisYhvleBvx/iGxYWpkmTJmngwIHy9vZW7dq1NXPmTPu6fz/Ed//+/erUqZMk6ZprrpHNZlNsbKwJzwAAAADA1YCCehWKj49Xq1attG3bNj366KN65JFHlJKSUmi9kJAQffbZZ5KklJQUpaena9q0aUWOmZ2drczMzAI3AAAAACgLCupV6I477tCjjz6q+vXr65lnnpG/v79WrlxZaD1nZ2f74cE1atRQYGCgfH19ixwzLi5Ovr6+9ltISMglfQ4AAAAArjwU1KtQ06ZN7f+22WwKDAzUkSNHLmrMMWPGKCMjw347ePDgxcYEAAAAcJXhIklXoX9e0ddmsyk/P/+ixnRzc5Obm9tFjQEAAADg6sYMKhxydXWVJOXl5ZmcBAAAAMCVjoIKh0JDQ2Wz2fTVV1/p6NGjysrKMjsSAAAAgCsUBRUO1axZU+PHj9ezzz6ra6+9VsOHDzc7EgAAAIArlM0wDMPsELjyZGZmytfXVxkZGfLx8TE7TiGeNpvZEQAAAICrgiHpjFSqbsAMKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAElzMDoArW6Cvr2xmh8AV71SM2QmK5znf7ARFizA7gAM1zQ7gwJNmB3DgBbMDFKOq2QEcCDE7gANhZgdwYKvZASohP7MDOGDln9GjZgeohKz69cyV9Gkp12UGFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUCzIMQ0OGDJGfn59sNpuSk5NLtZ3NZtOSJUskSfv37y/TtgAAAABgNgqqBX3zzTeaPXu2vvrqK6Wnp+u66667LPu9UGov3Ly9vdWkSRMNGzZMe/fuvSwZAAAAAFy9KKgWtG/fPgUFBalt27YKDAyUi4vLZd3/ihUrlJ6erh9//FGTJk3S7t271axZMyUmJl7WHAAAAACuLhRUi4mNjdVjjz2mtLQ02Ww2hYWFSZLCwsI0derUAus2b95c48aNq/AM1atXV2BgoOrWrasePXpoxYoVat26tQYNGqS8vLwK3x8AAAAASBRUy5k2bZpeeukl1apVS+np6dq8efMl29e4cePsBdgRJycnPfHEEzpw4IC2bNlS5DrZ2dnKzMwscAMAAACAsqCgWoyvr6+8vb3l7OyswMBABQQEXLJ9+fv7q169eqVat2HDhpLOn6dalLi4OPn6+tpvISEhFRUTAAAAwFWCgnoVGz58eKnPKzUMQ9L5KwUXZcyYMcrIyLDfDh48WGE5AQAAAFwdLu/Vd1BuTk5O9pJ4QW5u7mXb/+7duyVJderUKfJxNzc3ubm5XbY8AAAAAK48zKBWEgEBAUpPT7ffz8zMVGpq6mXZd35+vqZPn646deqoRYsWl2WfAAAAAK4+FNRK4tZbb9W8efO0Zs0a7dixQ/3795ezs/NFjfn6668rKiqq0PI///xThw8f1q+//qovvvhC0dHR2rRpk2bNmnXR+wQAAACA4nCIbyUxZswYpaam6s4775Svr6/+85//XPQM6rFjx7Rv375Cy6OjoyVJHh4eCg0NVadOnTRz5kzVr1//ovYHAAAAAI7YjH+e2AhUgMzMTPn6+spdUtGXVQIqzqkYsxMUz3O+2QmKFmF2AAdqmh3AgSfNDuDAC2YHKEZVswM4YOXrzYeZHcCBrWYHqIT8zA7ggJV/Ro+aHaASsurXM1fSp5IyMjLk4+PjcF0O8QUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJbgYnYAwAynDMPsCEXytNnMjlApTZtvdoLinYoxO0HR7rfwa3bS7AAOHDU7gAPzzA5QjJlmB3Agx+wADtQ1O4AD15kdoBi7zA5QSQWYHaAS+svsAJXQ2TKsywwqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoF5G48aNU/PmzUu9/syZMxUSEiInJydNnTq1zNsXZf/+/bLZbEpOTi71Nrt27VKtWrV06tSpi9o3AAAAADhCQb1EbDablixZUmDZqFGjlJiYWKrtMzMzNXz4cD3zzDM6dOiQhgwZUqbtK1Ljxo3Vpk0bvfbaa5d93wAAAACuHhTUy8jLy0vVq1cv1bppaWnKzc1Vt27dFBQUJA8PjzJtX9EGDBigt956S+fOnTNl/wAAAACufBTUYnz66aeKjIyUu7u7qlevrujoaPshrps3b9Ztt90mf39/+fr6qkOHDtq6dat927CwMElSr169ZLPZ7Pf/eYhuUlKSbrzxRnl6eqpatWpq166dDhw4oNmzZysyMlKSVLduXdlsNu3fv7/IQ3zfe+89NWrUSFWrVlXDhg315ptvFnh806ZNatGihapWrapWrVpp27Zt5Xo9brvtNv31119atWpVubYHAAAAgJJQUIuQnp6uvn37auDAgdq9e7eSkpLUu3dvGYYhSTp58qT69++vtWvXasOGDQoPD9cdd9yhkydPSjpfYCUpISFB6enp9vt/d+7cOfXs2VMdOnTQ9u3b9f3332vIkCGy2Wzq06ePVqxYIel8wUxPT1dISEihMebPn69///vfmjhxonbv3q1JkybpxRdf1Jw5cyRJWVlZuvPOO9W4cWNt2bJF48aN06hRo0p8/uPGjbOX6gtcXV3VvHlzrVmzpshtsrOzlZmZWeAGAAAAAGXhYnYAK0pPT9e5c+fUu3dvhYaGSpJ9RlOSbr311gLrz5w5U9WqVdOqVat05513KiAgQJJUrVo1BQYGFrmPzMxMZWRk6M4771S9evUkSY0aNbI/fuFQ3oCAgGLHGDt2rOLj49W7d29JUp06dbRr1y6988476t+/vxYsWKD8/HzNmjVLVatWVZMmTfTbb7/pkUcecfj8/f397Zn+Ljg4WAcOHChym7i4OI0fP97huAAAAADgCDOoRWjWrJmioqIUGRmpe+65R++++66OHz9uf/yPP/7Q4MGDFR4eLl9fX/n4+CgrK0tpaWml3oefn59iY2PVpUsXde/eXdOmTVN6enqptz916pT27dunQYMGycvLy36bMGGC9u3bJ0navXu3mjZtqqpVq9q3u+mmm0oce/jw4UVejMnd3V2nT58ucpsxY8YoIyPDfjt48GCpnwsAAAAASBTUIjk7O2v58uX63//+p8aNG2vGjBmKiIhQamqqJKl///5KTk7WtGnTtH79eiUnJ6t69erKyckp034SEhL0/fffq23btvroo4/UoEEDbdiwoVTbZmVlSZLeffddJScn2287d+4s9Rhl9ddff9lnh//Jzc1NPj4+BW4AAAAAUBYU1GLYbDa1a9dO48eP17Zt2+Tq6qrFixdLktatW6fHH39cd9xxh5o0aSI3NzcdO3aswPZVqlRRXl5eiftp0aKFxowZo/Xr1+u6667TggULSpXv2muvVXBwsH799VfVr1+/wK1OnTqSzh8yvH37dp09e9a+3cWU1507d6pFixbl3h4AAAAAHKGgFmHjxo2aNGmSfvjhB6WlpWnRokU6evSo/RzR8PBwzZs3T7t379bGjRsVExMjd3f3AmOEhYUpMTFRhw8fLnB48AWpqakaM2aMvv/+ex04cEDLli3T3r17C5yHWpLx48crLi5O06dP1549e7Rjxw4lJCTYP6/0/vvvl81m0+DBg7Vr1y59/fXXevXVV0sc9/XXX1dUVFSBZfv379ehQ4cUHR1d6nwAAAAAUBYU1CL4+Pho9erVuuOOO9SgQQO98MILio+P1+233y5JmjVrlo4fP67rr79eDz74oB5//HHVqFGjwBjx8fFavny5QkJCipx19PDw0M8//6y7775bDRo00JAhQzRs2DA9/PDDpc750EMP6b333lNCQoIiIyPVoUMHzZ492z6D6uXlpS+//FI7duxQixYt9Pzzz2vy5Mkljnvs2DH7eawXfPjhh+rcubP9olEAAAAAUNFsxoXPTgGKkZOTo/DwcC1YsEDt2rUr1TaZmZny9fWVuyTbpY1XLqcs+m3vabPiq2V9k8wO4MATMWYnKNr9881OULyTZgdw4AGzAzjQyuwAxZhpdgAHynbliMurudkBHPAwO0AxdpkdoJIq+uoicOQvswNUQmclTZSUkZFR4rVqmEFFidLS0vTcc8+VupwCAAAAQHnwOago0YWLLwEAAADApcQMKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLcDE7AGAGT5vN7AhFOmUYZkcollVfM0l6zuwAjsw3O0DRFsSYnaB491v0NZOkD8wOUAkNMTuAAzPNDuBAstkBHGhudoBiNDY7gAO7zA7gwFGzAzgQYHaAYviZHcCBv8wOUAGYQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIF9SJ07NhRI0aMMDvGZZGTk6P69etr/fr1ZkcBAAAAcIWioKJU3n77bdWpU0dt27Y1OwoAAACAKxQF9QqVk5NTYWMZhqHXX39dgwYNqrAxAQAAAOCfKKgXKT8/X08//bT8/PwUGBiocePG2R/bv3+/bDabkpOT7ctOnDghm82mpKQkSVJSUpJsNpsSExPVqlUreXh4qG3btkpJSSmwnwkTJqhGjRry9vbWQw89pGeffVbNmze3Px4bG6uePXtq4sSJCg4OVkREhF566SVdd911hTI3b95cL774Yqmf45YtW7Rv3z5169at1NsAAAAAQFlRUC/SnDlz5OnpqY0bN2rKlCl66aWXtHz58jKP8/zzzys+Pl4//PCDXFxcNHDgQPtj8+fP18SJEzV58mRt2bJFtWvX1ltvvVVojMTERKWkpGj58uX66quvNHDgQO3evVubN2+2r7Nt2zZt375dAwYMKDZLWFhYgaK9Zs0aNWjQQN7e3mV+XgAAAABQWi5mB6jsmjZtqrFjx0qSwsPD9frrrysxMVG33XZbmcaZOHGiOnToIEl69tln1a1bN509e1ZVq1bVjBkzNGjQIHup/Pe//61ly5YpKyurwBienp5677335Orqal/WpUsXJSQk6IYbbpAkJSQkqEOHDqpbt26xWerVqyd/f3/7/QMHDig4ONhh/uzsbGVnZ9vvZ2ZmlvKZAwAAAMB5zKBepKZNmxa4HxQUpCNHjlzUOEFBQZJkHyclJUU33nhjgfX/eV+SIiMjC5RTSRo8eLA+/PBDnT17Vjk5OVqwYEGB2dmiJCYmavjw4fb7Z86cUdWqVR1uExcXJ19fX/stJCTE4foAAAAA8E8U1ItUpUqVAvdtNpvy8/MlSU5O519ewzDsj+fm5pY4js1mkyT7OKXl6elZaFn37t3l5uamxYsX68svv1Rubq7+9a9/lWlcf39/HT9+3OE6Y8aMUUZGhv128ODBMu0DAAAAACiol1BAQIAkKT093b7s7xdMKq2IiIgC55FKKnS/OC4uLurfv78SEhKUkJCg++67T+7u7mXaf4sWLfTzzz8XKNr/5ObmJh8fnwI3AAAAACgLzkG9hNzd3dWmTRu9/PLLqlOnjo4cOaIXXnihzOM89thjGjx4sFq1aqW2bdvqo48+0vbt2x2eR/p3Dz30kBo1aiRJWrduXYnrR0VFqVevXvbDfDt16qSsrCz99NNPRV4VGAAAAAAqAjOol9j777+vc+fOqWXLlhoxYoQmTJhQ5jFiYmI0ZswYjRo1Stdff71SU1MVGxtb4nmhF4SHh6tt27Zq2LChWrduXeL6+/bt07Fjx+z3q1evrl69emn+/Pllzg4AAAAApWUzHB23Ccu67bbbFBgYqHnz5pW4rmEYCg8P16OPPqqRI0eWa3/bt2/Xbbfdpn379snLy6vE9TMzM+Xr6yt3SbZy7fHqdMrCP46eNr6S5THJ7ADFeCLG7ATFu9/Cfws7aXYABx4wO0AxWpkdwIGZZgdwIMfsAA40NztAMTzMDuDALrMDVFIBZgeohP4yO0AxzkqaKCkjI6PEUwE5xLcSOH36tN5++2116dJFzs7O+vDDD7VixYpSfd7q0aNHtXDhQh0+fNjhZ5+WpGnTppo8ebJSU1MVGRlZ7nEAAAAAoDgU1ErAZrPp66+/1sSJE3X27FlFRETos88+U3R0dInb1qhRQ/7+/po5c6auueaai8oRGxt7UdsDAAAAgCMU1ErA3d1dK1asKNe2HMENAAAAoLLgIkkAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALIGCCgAAAACwBAoqAAAAAMASKKgAAAAAAEugoAIAAAAALMHF7AAA/o+nzWZ2hEppg9kBHGhjdoBifD3f7ATFO2p2AAd6mB3AgQlmByhGgNkBHHA2O4ADVn7d3jM7QDGqmB3AAStns/LPwWmzA1RCVv1eO1eGdcs1g7p161bt2LHDfv/zzz9Xz5499dxzzyknJ6c8QwIAAAAArnLlKqgPP/yw9uzZI0n69ddfdd9998nDw0OffPKJnn766QoNCAAAAAC4OpSroO7Zs0fNmzeXJH3yySdq3769FixYoNmzZ+uzzz6ryHwAAAAAgKtEuQqqYRjKz8+XJK1YsUJ33HGHJCkkJETHjh2ruHQAAAAAgKtGuQpqq1atNGHCBM2bN0+rVq1St27dJEmpqam69tprKzQgAAAAAODqUK6COnXqVG3dulXDhw/X888/r/r160uSPv30U7Vt27ZCAwIAAAAArg7l+piZpk2bFriK7wWvvPKKnJ2tfLFqAAAAAIBVlWsGVZJOnDih9957T2PGjNFff/0lSdq1a5eOHDlSYeEAAAAAAFePcs2gbt++XVFRUapWrZr279+vwYMHy8/PT4sWLVJaWprmzp1b0TkBAAAAAFe4cs2gjhw5UgMGDNDevXtVtWpV+/I77rhDq1evrrBwAAAAAICrR7kK6ubNm/Xwww8XWl6zZk0dPnz4okMBAAAAAK4+5Sqobm5uyszMLLR8z549CggIuOhQAAAAAICrT7kK6l133aWXXnpJubm5kiSbzaa0tDQ988wzuvvuuys0IAAAAADg6lCughofH6+srCzVqFFDZ86cUYcOHVS/fn15e3tr4sSJFZ3xqjNu3Dg1b97ctP0nJiaqUaNGysvLK7C8ffv2WrBggUmpAAAAAFzpynUVX19fXy1fvlzr1q3Tjz/+qKysLF1//fWKjo6u6HyWEBsbqxMnTmjJkiWXZX+jRo3SY489dln2VZSnn35aL7zwQoHPtP3iiy/0xx9/6L777jMtFwAAAIArW7kK6ty5c9WnTx+1a9dO7dq1sy/PycnRwoUL1a9fvwoLeCXJycmRq6triet5eXnJy8vrMiQqbO3atdq3b1+hQ7WnT5+uAQMGyMmp3B+dCwAAAAAOlattDBgwQBkZGYWWnzx5UgMGDLjoUGb49NNPFRkZKXd3d1WvXl3R0dE6deqUxo0bpzlz5ujzzz+XzWaTzWZTUlKSJOmZZ55RgwYN5OHhobp16+rFF1+0n5cr/d+huu+9957q1KmjqlWraubMmQoODlZ+fn6B/ffo0UMDBw4ssN0FsbGx6tmzp1599VUFBQWpevXqGjZsWIF9paenq1u3bnJ3d1edOnW0YMEChYWFaerUqWV6HRYuXKjbbrutwMcHHT16VN999526d+9eprEAAAAAoCzKNYNqGIZsNluh5b/99pt8fX0vOtTllp6err59+2rKlCnq1auXTp48qTVr1sgwDI0aNUq7d+9WZmamEhISJEl+fn6SJG9vb82ePVvBwcHasWOHBg8eLG9vbz399NP2sX/55Rd99tlnWrRokZydnRUSEqLHHntMK1euVFRUlCTpr7/+0jfffKOvv/662IwrV65UUFCQVq5cqV9++UV9+vRR8+bNNXjwYElSv379dOzYMSUlJalKlSoaOXKkjhw54vB5JyUlqVOnTkpNTVVYWJgkac2aNbr//vsLrLd27Vp5eHioUaNGxY6VnZ2t7Oxs+/2irvIMAAAAAI6UqaC2aNHCPosYFRUlF5f/2zwvL0+pqanq2rVrhYe81NLT03Xu3Dn17t1boaGhkqTIyEj74+7u7srOzlZgYGCB7V544QX7v8PCwjRq1CgtXLiwQEHNycnR3LlzC3z8zu23364FCxbYC+qnn34qf39/derUqdiM11xzjV5//XU5OzurYcOG6tatmxITEzV48GD9/PPPWrFihTZv3qxWrVpJkt577z2Fh4c7fN4eHh6KiIhQlSpV7MsOHDig4ODgAusdOHBA1157rcPDe+Pi4jR+/HiH+wMAAAAAR8pUUHv27ClJSk5OVpcuXQqcJ+nq6qqwsLBK+TEzzZo1U1RUlCIjI9WlSxd17txZ//rXv3TNNdc43O6jjz7S9OnTtW/fPmVlZencuXPy8fEpsE5oaGihz4aNiYnR4MGD9eabb8rNzU3z58/Xfffd57AANmnSpMBFi4KCgrRjxw5JUkpKilxcXHT99dfbH69fv36J+W+88Ub9/PPPBZadOXOmwOG9xS37pzFjxmjkyJH2+5mZmQoJCXG4DQAAAAD8XZkK6tixYyWdny3s06dPiaWlsnB2dtby5cu1fv16LVu2TDNmzNDzzz+vjRs3qk6dOkVu8/333ysmJkbjx49Xly5d5Ovrq4ULFyo+Pr7Aep6enoW27d69uwzD0NKlS3XDDTdozZo1+u9//+sw499nOaXznz37z/NYK4K/v7+OHz9e4rJ/cnNzk5ubW4XnAQAAAHD1KNdFkvr373/FlNMLbDab2rVrp/Hjx2vbtm1ydXXV4sWLJZ2fHf7nZ4KuX79eoaGhev7559WqVSuFh4frwIEDpdpX1apV1bt3b82fP18ffvihIiIiCsx+llVERITOnTunbdu22Zf98ssvJZbKorRo0UK7du0qtOzw4cPlGg8AAAAASqtcBTUvL0+vvvqqbrzxRgUGBsrPz6/ArbLZuHGjJk2apB9++EFpaWlatGiRjh49ar8oUFhYmLZv366UlBQdO3ZMubm5Cg8PV1pamhYuXKh9+/Zp+vTp9kJbGjExMVq6dKnef/99xcTEXFT+hg0bKjo6WkOGDNGmTZu0bds2DRkyRO7u7kVezOqCTZs2qWHDhjp06JB9WZcuXbR27doC67Vo0UL+/v5at27dReUEAAAAAEfKVVDHjx+v1157TX369FFGRoZGjhyp3r17y8nJSePGjavgiJeej4+PVq9erTvuuEMNGjTQCy+8oPj4eN1+++2SpMGDBysiIkKtWrVSQECA1q1bp7vuuktPPvmkhg8frubNm2v9+vV68cUXS73PW2+9VX5+fkpJSSl01dzymDt3rq699lq1b99evXr1sl9R2NFM9+nTp5WSklLg42piYmL0008/KSUlxb7M2dlZAwYM0Pz58y86JwAAAAAUx2YYhlHWjerVq6fp06erW7du8vb2VnJysn3Zhg0btGDBgkuRFWXw22+/KSQkRCtWrLBfLbi0Ro8erczMTL3zzjv2ZYcPH1aTJk20detW+5WOHcnMzJSvr6/cJRU/hwtUjA1mB3CgjdkBinGz2QEcOGp2AAd6mB3AgU/NDlCMgJJXMY1zyauYxsqv20GzAxSjSsmrmMbK2az8c3Da7ACVkFW/185JSpKUkZFR6KKy/1SuGdTDhw/bP4bFy8tLGRkZkqQ777xTS5cuLc+QuEjfffedvvjiC6Wmpmr9+vW67777FBYWpvbt25d5rOeff16hoaEFLsIUGBioWbNmKS0trSJjAwAAAIBduQpqrVq1lJ6eLun8bOqyZcskSZs3b+ZKribJzc3Vc889pyZNmqhXr14KCAhQUlJSoav/lka1atX03HPPFfrYm549e+qWW26pqMgAAAAAUECZPmbmgl69eikxMVGtW7fWY489pgceeMA+u/bkk09WdEaUQpcuXdSlSxezYwAAAABAuZWroL788sv2f/fp00ehoaFav369wsPD1b179woLBwAAAAC4epSroK5evVpt27aVi8v5zdu0aaM2bdro3LlzWr16dbnOewQAAAAAXN3KdQ5qp06d9NdffxVanpGRoU6dOl10KAAAAADA1adcBdUwDNlshT885M8//5Snp+dFhwIAAAAAXH3KdIhv7969JUk2m02xsbEFrtibl5en7du3q23bthWbEAAAAABwVShTQfX19ZV0fgbV29tb7u7u9sdcXV3Vpk0bDR48uGITAgAAAACuCmUqqAkJCZKkgIAAjRs3Th4eHpKk/fv3a8mSJWrUqJH8/f0rPiUAAAAA4IpXrnNQt23bprlz50qSTpw4oTZt2ig+Pl49e/bUW2+9VaEBAQAAAABXh3IX1FtuuUWS9Omnn+raa6/VgQMHNHfuXE2fPr1CAwIAAAAArg7lKqinT5+Wt7e3JGnZsmXq3bu3nJyc1KZNGx04cKBCAwIAAAAArg5lOgf1gvr162vJkiXq1auXvv32Wz355JOSpCNHjsjHx6dCAwJASdqYHaASWmt2gEpqitkBKqFfzQ4AADCdUYZ1yzWD+u9//1ujRo1SWFiYWrdurZtuuknS+dnUFi1alGdIAAAAAMBVzmYYRlkKrd3hw4eVnp6uZs2aycnpfM/dtGmTfHx81LBhwwoNiconMzNTvr6+cpdkMzsMAAAAANMYks5IysjIKPGI23IXVMARCioAAAAAqWwFtVyH+AIAAAAAUNEoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECuoVJCcn55LvIzc395LvAwAAAMDViYJaiXXs2FHDhw/XiBEj5O/vry5duui1115TZGSkPD09FRISokcffVRZWVmSJMMwFBAQoE8//dQ+RvPmzRUUFGS/v3btWrm5uen06dOSJJvNprfeekt33XWXPD09NXHixMv7JAEAAABcNSioldycOXPk6uqqdevW6e2335aTk5OmT5+un376SXPmzNF3332np59+WtL5stm+fXslJSVJko4fP67du3frzJkz+vnnnyVJq1at0g033CAPDw/7PsaNG6devXppx44dGjhwYJE5srOzlZmZWeAGAAAAAGXhYnYAXJzw8HBNmTLFfj8iIsL+77CwME2YMEFDhw7Vm2++Ken8rOs777wjSVq9erVatGihwMBAJSUlqWHDhkpKSlKHDh0K7OP+++/XgAEDHOaIi4vT+PHjK+ppAQAAALgKMYNaybVs2bLA/RUrVigqKko1a9aUt7e3HnzwQf3555/2Q3Y7dOigXbt26ejRo1q1apU6duyojh07KikpSbm5uVq/fr06duxYYMxWrVqVmGPMmDHKyMiw3w4ePFhhzxEAAADA1YGCWsl5enra/71//37deeedatq0qT777DNt2bJFb7zxhqT/u4BSZGSk/Pz8tGrVqgIFddWqVdq8ebNyc3PVtm3bYvdRHDc3N/n4+BS4AQAAAEBZcIjvFWTLli3Kz89XfHy8nJzO/+3h448/LrCOzWbTLbfcos8//1w//fSTbr75Znl4eCg7O1vvvPOOWrVqVapCCgAAAAAVjRnUK0j9+vWVm5urGTNm6Ndff9W8efP09ttvF1qvY8eO+vDDD9W8eXN5eXnJyclJ7du31/z58wudfwoAAAAAlwsF9QrSrFkzvfbaa5o8ebKuu+46zZ8/X3FxcYXW69Chg/Ly8gqca9qxY8dCywAAAADgcrIZhmGYHQJXnszMTPn6+spdks3sMAAAAABMY0g6IykjI6PEa9UwgwoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQXswMAqBxOGYbZEYrlabOZHaHSmWR2AAeeiDE7QfHun292guKdNDtAMR4wO4ADrcwO4MBMswM4kGN2gGI0NzuAAx5mB3Bgl9kBKqEAswNUQmckjSrlusygAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgXqSOHTtqxIgRZscAAAAAgEqPglpJjBs3Ts2bN7/k+0lKSpLNZpPNZpOTk5N8fX3VokULPf3000pPT7/k+wcAAABw9aKgXmGOHj2qs2fPXvQ4KSkp+v3337V582Y988wzWrFiha677jrt2LGjAlICAAAAQGEU1AqQn5+vp59+Wn5+fgoMDNS4cePsj+3fv182m03Jycn2ZSdOnJDNZlNSUpKk/5u1TExMVKtWreTh4aG2bdsqJSVFkjR79myNHz9eP/74o312c/bs2UVm+frrrxUUFKShQ4fq+++/L/dzqlGjhgIDA9WgQQPdd999WrdunQICAvTII4+Ue0wAAAAAcISCWgHmzJkjT09Pbdy4UVOmTNFLL72k5cuXl3mc559/XvHx8frhhx/k4uKigQMHSpL69Omjp556Sk2aNFF6errS09PVp0+fIseIiYnRBx98oOPHj+vWW29VRESEJk2apIMHDxa5fmxsrDp27FhiNnd3dw0dOlTr1q3TkSNHyvzcAAAAAKAkFNQK0LRpU40dO1bh4eHq16+fWrVqpcTExDKPM3HiRHXo0EGNGzfWs88+q/Xr1+vs2bNyd3eXl5eXXFxcFBgYqMDAQLm7uxc5houLi7p166aPPvpIhw8f1qhRo/TNN9+oTp06io6O1rx583TmzBn7+kFBQapdu3ap8jVs2FDS+Vnhf8rOzlZmZmaBGwAAAACUBQW1AjRt2rTA/aCgoHLNMv59nKCgIEm6qNlKX19fDR48WKtXr9b69euVmpqqfv366dtvv7WvExcXp7lz55ZqPMMwJEk2m63QY3FxcfL19bXfQkJCyp0bAAAAwNWJgloBqlSpUuC+zWZTfn6+JMnJ6fxLfKHcSVJubm6J41wogRfGKY+zZ8/qk08+Uffu3XXzzTfL399fb775pqKioso13u7duyVJYWFhhR4bM2aMMjIy7LfiDikGAAAAgOK4mB3gShcQECBJSk9PV4sWLSSpwAWTSsvV1VV5eXklrmcYhtauXau5c+fqk08+kbe3tx544AG98sor9kN0y+PMmTOaOXOm2rdvb39Of+fm5iY3N7dyjw8AAAAAFNRLzN3dXW3atNHLL7+sOnXq6MiRI3rhhRfKPE5YWJhSU1OVnJysWrVqydvbu8hC+MEHH+jhhx9Wr1699PHHHys6Oto+i1uUMWPG6NChQ4UO8z1y5IjOnj2rkydPasuWLZoyZYqOHTumRYsWlTk7AAAAAJQGBfUyeP/99zVo0CC1bNlSERERmjJlijp37lymMe6++24tWrRInTp10okTJ5SQkKDY2NhC60VFRenw4cPy8fEp1bjp6elKS0srtDwiIkI2m01eXl6qW7euOnfurJEjRyowMLBMuQEAAACgtGzG30+OBCpIZmamfH195S6p8CWVUBmdsvCvCs8iLtwFxyaZHcCBJ2LMTlC8++ebnaB4J80OUIwHzA7gQCuzAzgw0+wADuSYHaAYzc0O4ICH2QEc2GV2gEqo8MluKMkZSaMkZWRklDiRxkWSAAAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACW4GJ2AACVg6fNZnaESmmD2QGK0cbsAA58Pd/sBMU7anYAB3qYHaAYE8wO4ECA2QEccDY7gANWfd3eMzuAA1XMDuCAlbNZ9efgtNkBKqFzZViXGVQAAAAAgCVQUAEAAAAAlkBBBQAAAABYAgUVAAAAAGAJFFQAAAAAgCVQUAEAAAAAlkBBBQAAAABYAgUVAAAAAGAJFFQAAAAAgCVQUAEAAAAAlkBBBQAAAABYAgUVAAAAAGAJFFQAAAAAgCVYrqB27NhRI0aMMDuG5dhsNi1ZssTsGAAAAABwyViuoF5JZs+erWrVqpkdo0yK+wNBUlKSbDabTpw4cdkzAQAAALg6UFDLIScnx+wIAAAAAHDFMbWgnjp1Sv369ZOXl5eCgoIUHx9faJ3s7GyNGjVKNWvWlKenp1q3bq2kpCT74wcOHFD37t11zTXXyNPTU02aNNHXX38t6f9m/ZYuXaqmTZuqatWqatOmjXbu3Gnf/s8//1Tfvn1Vs2ZNeXh4KDIyUh9++GGBDB07dtTw4cM1YsQI+fv7q0uXLpKk1157TZGRkfL09FRISIgeffRRZWVl2fc9YMAAZWRkyGazyWazady4caV6TsU5duyYevXqJQ8PD4WHh+uLL76wP1bUbO2SJUtks9ns98eNG6fmzZtr3rx5CgsLk6+vr+677z6dPHlSkhQbG6tVq1Zp2rRp9sz79+8vMRcAAAAAVARTC+ro0aO1atUqff7551q2bJmSkpK0devWAusMHz5c33//vRYuXKjt27frnnvuUdeuXbV3715J0rBhw5Sdna3Vq1drx44dmjx5sry8vArtJz4+Xps3b1ZAQIC6d++u3NxcSdLZs2fVsmVLLV26VDt37tSQIUP04IMPatOmTQXGmDNnjlxdXbVu3Tq9/fbbkiQnJydNnz5dP/30k+bMmaPvvvtOTz/9tCSpbdu2mjp1qnx8fJSenq709HSNGjWqVM+pOOPHj9e9996r7du364477lBMTIz++uuvMr3m+/bt05IlS/TVV1/pq6++0qpVq/Tyyy9LkqZNm6abbrpJgwcPtmcOCQkp0/gAAAAAUF4uZu04KytLs2bN0gcffKCoqChJ50tgrVq17OukpaUpISFBaWlpCg4OliSNGjVK33zzjRISEjRp0iSlpaXp7rvvVmRkpCSpbt26hfY1duxY3XbbbQX2sXjxYt17772qWbOmvThK0mOPPaZvv/1WH3/8sW688Ub78vDwcE2ZMqXAuH8/VzMsLEwTJkzQ0KFD9eabb8rV1VW+vr6y2WwKDAws03MqTmxsrPr27StJmjRpkqZPn65Nmzapa9euDl7pgvLz8zV79mx5e3tLkh588EElJiZq4sSJ8vX1laurqzw8PApkLo3s7GxlZ2fb72dmZpZpewAAAAAwraDu27dPOTk5at26tX2Zn5+fIiIi7Pd37NihvLw8NWjQoMC22dnZql69uiTp8ccf1yOPPKJly5YpOjpad999t5o2bVpg/ZtuuqnQPnbv3i1JysvL06RJk/Txxx/r0KFDysnJUXZ2tjw8PAqM0bJly0LPYcWKFYqLi9PPP/+szMxMnTt3TmfPntXp06cLbV+W51Scvz8vT09P+fj46MiRIw63+aewsDB7OZWkoKCgMo9RlLi4OI0fP/6ixwEAAABw9TKtoJZGVlaWnJ2dtWXLFjk7Oxd47MJhvA899JC6dOmipUuXatmyZYqLi1N8fLwee+yxUu3jlVde0bRp0zR16lT7+aQjRowodCEkT0/PAvf379+vO++8U4888ogmTpwoPz8/rV27VoMGDVJOTk6xBbU0z6k4VapUKXDfZrMpPz9f0vnDjQ3DKPD4hcOYSzvGxRgzZoxGjhxpv5+ZmcnhwQAAAADKxLSCWq9ePVWpUkUbN25U7dq1JUnHjx/Xnj171KFDB0lSixYtlJeXpyNHjuiWW24pdqyQkBANHTpUQ4cO1ZgxY/Tuu+8WKKgbNmwotI9GjRpJktatW6cePXrogQcekHT+ENg9e/aocePGDvNv2bJF+fn5io+Pl5PT+VN5P/744wLruLq6Ki8vr8Cy0j6nsgoICNDJkyd16tQpe5lOTk4u8zhFZZbOXyjqnwX479zc3OTm5lbm/QEAAADABaZdJMnLy0uDBg3S6NGj9d1332nnzp2KjY21lz1JatCggWJiYtSvXz8tWrRIqamp2rRpk+Li4rR06VJJ588D/fbbb5WamqqtW7dq5cqV9vJ5wUsvvaTExET7Pvz9/dWzZ09J588tXb58udavX6/du3fr4Ycf1h9//FFi/vr16ys3N1czZszQr7/+qnnz5tkvnnRBWFiYsrKylJiYqGPHjun06dOlek7l0bp1a3l4eOi5557Tvn37tGDBAs2ePbvM44SFhWnjxo3av3+/jh07Zp9dXbx4sRo2bGi/4i8AAAAAVDRTr+L7yiuv6JZbblH37t0VHR2tm2++udC5ngkJCerXr5+eeuopRUREqGfPntq8ebN9RjQvL0/Dhg1To0aN1LVrVzVo0EBvvvlmgTFefvllPfHEE2rZsqUOHz6sL7/8Uq6urpKkF154Qddff726dOmijh07KjAw0F5eHWnWrJlee+01TZ48Wdddd53mz5+vuLi4Auu0bdtWQ4cOVZ8+fRQQEGC/yFJJz6k8/Pz89MEHH+jrr7+2f1TOhY+1KYtRo0bJ2dlZjRs3VkBAgNLS0iRJGRkZSklJKXJ2FQAAAAAqgs1wdNxmJZeUlKROnTrp+PHjhT4jFJdWZmamfH195S7JVuLawJVrg9kBitHG7AAO3Gx2AAeOmh3AgR5mByjGp2YHcCDA7AAOOJe8imms+rodNDuAA1VKXsU0Vs5m1Z+D02YHqITOSVqn85NePj4+Dtc1dQYVAAAAAIALKKgAAAAAAEuw9MfMXKySrjwLAAAAALAOZlABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWILNMAzD7BC48mRmZsrX11fukmxmhwFQiJ/ZASopV7MDOFDF7ADF8DY7gAPOZgdwwKpfT8m62aqaHcABq75mkrV/r7mZHaAYVn7NrPq9liNptqSMjAz5+Pg4XJcZVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQAQAAAACWQEEFAAAAAFgCBRUAAAAAYAkUVAAAAACAJVBQLaZjx44aMWJEpd8HAAAAAJQVBRUAAAAAYAkUVAAAAACAJVBQTXTq1Cn169dPXl5eCgoKUnx8fIHHs7OzNWrUKNWsWVOenp5q3bq1kpKS7I//+eef6tu3r2rWrCkPDw9FRkbqww8/LNM+AAAAAMAqKKgmGj16tFatWqXPP/9cy5YtU1JSkrZu3Wp/fPjw4fr++++1cOFCbd++Xffcc4+6du2qvXv3SpLOnj2rli1baunSpdq5c6eGDBmiBx98UJs2bSr1PipKdna2MjMzC9wAAAAAoCxshmEYZoe4GmVlZal69er64IMPdM8990iS/vrrL9WqVUtDhgzRyJEjVbduXaWlpSk4ONi+XXR0tG688UZNmjSpyHHvvPNONWzYUK+++mqJ+5g6dWqFPZ9x48Zp/PjxhZa7S7JV2F4AVBQ/swNUUq5mB3CgitkBiuFtdgAHnM0O4IBVv56SdbNVNTuAA1Z9zSRr/15zMztAMaz8mln1ey1H0mxJGRkZ8vHxcbiuy+UIhML27dunnJwctW7d2r7Mz89PERERkqQdO3YoLy9PDRo0KLBddna2qlevLknKy8vTpEmT9PHHH+vQoUPKyclRdna2PDw8SrWPijRmzBiNHDnSfj8zM1MhISEVvh8AAAAAVy4KqkVlZWXJ2dlZW7ZskbNzwb/xenl5SZJeeeUVTZs2TVOnTlVkZKQ8PT01YsQI5eTkXPa8bm5ucnOz6t+5AAAAAFQGnINqknr16qlKlSrauHGjfdnx48e1Z88eSVKLFi2Ul5enI0eOqH79+gVugYGBkqR169apR48eeuCBB9SsWTPVrVvXvn1p9gEAAAAAVkJBNYmXl5cGDRqk0aNH67vvvtPOnTsVGxsrJ6fzX5IGDRooJiZG/fr106JFi5SamqpNmzYpLi5OS5culSSFh4dr+fLlWr9+vXbv3q2HH35Yf/zxR6n3ccGYMWPUr18/+/1NmzapYcOGOnTokH1ZVFSUXn/99Uv5kgAAAAC4ynGIr4leeeUVZWVlqXv37vL29tZTTz2ljIwM++MJCQmaMGGCnnrqKR06dEj+/v5q06aN7rzzTknSCy+8oF9//VVdunSRh4eHhgwZop49exYYo6R9SFJ6errS0tLs90+fPq2UlBTl5ubal+3bt0/Hjh27VC8FAAAAAHAVX1wamZmZ8vX15Sq+gEVxFd/y4cqNZcdVfMvHql9PybrZuIpv+Vj595pVr25i5dfMqt9rZbmKL4f4AgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgAgAAAAAsgYIKAAAAALAECioAAAAAwBIoqAAAAAAAS3AxOwCuTIZhnP+vyTkAFC3f7ACVlJVftzyzAxTDqrkka79H2cwO4IBVs+WaHaCSsurXU2ImrTys+nst5///90JHcISCikvi5MmTkqSzJucAULQzZgcAAABXnZMnT8rX19fhOjajNDUWKKP8/Hz9/vvv8vb2ls128X+by8zMVEhIiA4ePCgfH58KSFhxrJrNqrkkspWXVbNZNZdEtvKyajar5pLIVl5WzWbVXBLZysuq2ayaS6rYbIZh6OTJkwoODpaTk+O5cWZQcUk4OTmpVq1aFT6uj4+P5X54L7BqNqvmkshWXlbNZtVcEtnKy6rZrJpLIlt5WTWbVXNJZCsvq2azai6p4rKVNHN6AYd2AwAAAAAsgYIKAAAAALAECioqBTc3N40dO1Zubm5mRynEqtmsmksiW3lZNZtVc0lkKy+rZrNqLols5WXVbFbNJZGtvKyazaq5JPOycZEkAAAAAIAlMIMKAAAAALAECioAAAAAwBIoqAAAAAAAS6CgwvLeeOMNhYWFqWrVqmrdurU2bdpkdiRJ0urVq9W9e3cFBwfLZrNpyZIlZkeSJMXFxemGG26Qt7e3atSooZ49eyolJcXsWJKkt956S02bNrV/ntZNN92k//3vf2bHKuTll1+WzWbTiBEjzI6icePGyWazFbg1bNjQ7Fh2hw4d0gMPPKDq1avL3d1dkZGR+uGHH8yOpbCwsEKvm81m07Bhw0zNlZeXpxdffFF16tSRu7u76tWrp//85z+yyuUgTp48qREjRig0NFTu7u5q27atNm/efNlzlPT71TAM/fvf/1ZQUJDc3d0VHR2tvXv3WiLbokWL1LlzZ1WvXl02m03JycmXJVdJ2XJzc/XMM88oMjJSnp6eCg4OVr9+/fT777+bmks6/3uuYcOG8vT01DXXXKPo6Ght3LjxkucqTba/Gzp0qGw2m6ZOnWqJbLGxsYV+x3Xt2tX0XJK0e/du3XXXXfL19ZWnp6duuOEGpaWlmZ6tqPcFm82mV155xfRsWVlZGj58uGrVqiV3d3c1btxYb7/99iXPVZpsf/zxh2JjYxUcHCwPDw917dr1kv7OpaDC0j766CONHDlSY8eO1datW9WsWTN16dJFR44cMTuaTp06pWbNmumNN94wO0oBq1at0rBhw7RhwwYtX75cubm56ty5s06dOmV2NNWqVUsvv/yytmzZoh9++EG33nqrevTooZ9++snsaHabN2/WO++8o6ZNm5odxa5JkyZKT0+339auXWt2JEnS8ePH1a5dO1WpUkX/+9//tGvXLsXHx+uaa64xO5o2b95c4DVbvny5JOmee+4xNdfkyZP11ltv6fXXX9fu3bs1efJkTZkyRTNmzDA11wUPPfSQli9frnnz5mnHjh3q3LmzoqOjdejQocuao6Tfr1OmTNH06dP19ttva+PGjfL09FSXLl109uxZ07OdOnVKN998syZPnnzJsxS17+KynT59Wlu3btWLL76orVu3atGiRUpJSdFdd91lai5JatCggV5//XXt2LFDa9euVVhYmDp37qyjR4+anu2CxYsXa8OGDQoODr7kmS4oTbauXbsW+F334Ycfmp5r3759uvnmm9WwYUMlJSVp+/btevHFF1W1alXTs/39tUpPT9f7778vm82mu+++2/RsI0eO1DfffKMPPvhAu3fv1ogRIzR8+HB98cUXpmYzDEM9e/bUr7/+qs8//1zbtm1TaGiooqOjL93/WxqAhd14443GsGHD7Pfz8vKM4OBgIy4uzsRUhUkyFi9ebHaMIh05csSQZKxatcrsKEW65pprjPfee8/sGIZhGMbJkyeN8PBwY/ny5UaHDh2MJ554wuxIxtixY41mzZqZHaNIzzzzjHHzzTebHaNUnnjiCaNevXpGfn6+qTm6detmDBw4sMCy3r17GzExMSYl+j+nT582nJ2dja+++qrA8uuvv954/vnnTUpV+Pdrfn6+ERgYaLzyyiv2ZSdOnDDc3NyMDz/80NRsf5eammpIMrZt23ZZM11QmvelTZs2GZKMAwcOXJ5QRulyZWRkGJKMFStWXJ5Q/19x2X777TejZs2axs6dO43Q0FDjv//972XNVVy2/v37Gz169LjsWf6uqFx9+vQxHnjgAXMC/U1pvtd69Ohh3HrrrZcn0N8Ula1JkybGSy+9VGCZGb9//5ktJSXFkGTs3LnTviwvL88ICAgw3n333UuSgRlUWFZOTo62bNmi6Oho+zInJydFR0fr+++/NzFZ5ZKRkSFJ8vPzMzlJQXl5eVq4cKFOnTqlm266yew4kqRhw4apW7duBb7nrGDv3r0KDg5W3bp1FRMTc1kOkyqNL774Qq1atdI999yjGjVqqEWLFnr33XfNjlVITk6OPvjgAw0cOFA2m83ULG3btlViYqL27NkjSfrxxx+1du1a3X777abmkqRz584pLy+v0CyHu7u7ZWbtJSk1NVWHDx8u8HPq6+ur1q1b895QRhkZGbLZbKpWrZrZUexycnI0c+ZM+fr6qlmzZmbHUX5+vh588EGNHj1aTZo0MTtOIUlJSapRo4YiIiL0yCOP6M8//zQ1T35+vpYuXaoGDRqoS5cuqlGjhlq3bm2Z06D+7o8//tDSpUs1aNAgs6NIOv/+8MUXX+jQoUMyDEMrV67Unj171LlzZ1NzZWdnS1KB9wYnJye5ubldsvcGCios69ixY8rLy9O1115bYPm1116rw4cPm5SqcsnPz9eIESPUrl07XXfddWbHkSTt2LFDXl5ecnNz09ChQ7V48WI1btzY7FhauHChtm7dqri4OLOjFNC6dWvNnj1b33zzjd566y2lpqbqlltu0cmTJ82Opl9//VVvvfWWwsPD9e233+qRRx7R448/rjlz5pgdrYAlS5boxIkTio2NNTuKnn32Wd13331q2LChqlSpohYtWmjEiBGKiYkxO5q8vb1100036T//+Y9+//135eXl6YMPPtD333+v9PR0s+PZXfj9z3vDxTl79qyeeeYZ9e3bVz4+PmbH0VdffSUvLy9VrVpV//3vf7V8+XL5+/ubHUuTJ0+Wi4uLHn/8cbOjFNK1a1fNnTtXiYmJmjx5slatWqXbb79deXl5pmU6cuSIsrKy9PLLL6tr165atmyZevXqpd69e2vVqlWm5SrKnDlz5O3trd69e5sdRZI0Y8YMNW7cWLVq1ZKrq6u6du2qN954Q+3btzc1V8OGDVW7dm2NGTNGx48fV05OjiZPnqzffvvtkr03uFySUQFYwrBhw7Rz505LzX5EREQoOTlZGRkZ+vTTT9W/f3+tWrXK1JJ68OBBPfHEE1q+fPllOUemLP4+s9a0aVO1bt1aoaGh+vjjj03/q29+fr5atWqlSZMmSZJatGihnTt36u2331b//v1NzfZ3s2bN0u23335Zzx0rzscff6z58+drwYIFatKkiZKTkzVixAgFBwdb4jWbN2+eBg4cqJo1a8rZ2VnXX3+9+vbtqy1btpgdDRUoNzdX9957rwzD0FtvvWV2HElSp06dlJycrGPHjundd9/Vvffeq40bN6pGjRqmZdqyZYumTZumrVu3mn70RVHuu+8++78jIyPVtGlT1atXT0lJSYqKijIlU35+viSpR48eevLJJyVJzZs31/r16/X222+rQ4cOpuQqyvvvv6+YmBjLvO/PmDFDGzZs0BdffKHQ0FCtXr1aw4YNU3BwsKlHdlWpUkWLFi3SoEGD5OfnJ2dnZ0VHR+v222+/ZBf4YwYVluXv7y9nZ2f98ccfBZb/8ccfCgwMNClV5TF8+HB99dVXWrlypWrVqmV2HDtXV1fVr19fLVu2VFxcnJo1a6Zp06aZmmnLli06cuSIrr/+erm4uMjFxUWrVq3S9OnT5eLiYupfo/+pWrVqatCggX755RezoygoKKjQHxYaNWpkmUOQJenAgQNasWKFHnroIbOjSJJGjx5tn0WNjIzUgw8+qCeffNIyM/f16tXTqlWrlJWVpYMHD2rTpk3Kzc1V3bp1zY5md+H3P+8N5XOhnB44cEDLly+3xOypJHl6eqp+/fpq06aNZs2aJRcXF82aNcvUTGvWrNGRI0dUu3Zt+3vDgQMH9NRTTyksLMzUbEWpW7eu/P39TX1/8Pf3l4uLi+XfG9asWaOUlBTLvDecOXNGzz33nF577TV1795dTZs21fDhw9WnTx+9+uqrZsdTy5YtlZycrBMnTig9PV3ffPON/vzzz0v23kBBhWW5urqqZcuWSkxMtC/Lz89XYmKiZc5ZtCLDMDR8+HAtXrxY3333nerUqWN2JIfy8/Pt5zeYJSoqSjt27FBycrL91qpVK8XExCg5OVnOzs6m5vu7rKws7du3T0FBQWZHUbt27Qp9hNGePXsUGhpqUqLCEhISVKNGDXXr1s3sKJLOX0nVyangW6+zs7N91sEqPD09FRQUpOPHj+vbb79Vjx49zI5kV6dOHQUGBhZ4b8jMzNTGjRt5byjBhXK6d+9erVixQtWrVzc7UrGs8N7w4IMPavv27QXeG4KDgzV69Gh9++23pmYrym+//aY///zT1PcHV1dX3XDDDZZ/b5g1a5ZatmxpifOcpfM/m7m5uZZ/f/D19VVAQID27t2rH3744ZK9N3CILyxt5MiR6t+/v1q1aqUbb7xRU6dO1alTpzRgwACzoykrK6vAXylTU1OVnJwsPz8/1a5d27Rcw4YN04IFC/T555/L29vbfk6Wr6+v3N3dTcslSWPGjNHtt9+u2rVr6+TJk1qwYIGSkpJMf6P39vYudI6up6enqlevbvq5u6NGjVL37t0VGhqq33//XWPHjpWzs7P69u1rai5JevLJJ9W2bVtNmjRJ9957rzZt2qSZM2dq5syZZkeTdP5/cBMSEtS/f3+5uFjj7a579+6aOHGiateurSZNmmjbtm167bXXNHDgQLOjSZK+/fZbGYahiIgI/fLLLxo9erQaNmx42X/nlvT7dcSIEZowYYLCw8NVp04dvfjiiwoODlbPnj1Nz/bXX38pLS3N/vmiF/5HPTAw8JLP8DrKFhQUpH/961/aunWrvvrqK+Xl5dnfH/z8/OTq6mpKrurVq2vixIm66667FBQUpGPHjumNN97QoUOHLsvHQpX09fxnia9SpYoCAwMVERFhajY/Pz+NHz9ed999twIDA7Vv3z49/fTTql+/vrp06WJartq1a2v06NHq06eP2rdvr06dOumbb77Rl19+qaSkpEuaqzTZpPN/0Prkk08UHx9/yfOUJVuHDh00evRoubu7KzQ0VKtWrdLcuXP12muvmZ7tk08+UUBAgGrXrq0dO3boiSeeUM+ePS/dBZwuybWBgQo0Y8YMo3bt2oarq6tx4403Ghs2bDA7kmEYhrFy5UpDUqFb//79Tc1VVCZJRkJCgqm5DMMwBg4caISGhhqurq5GQECAERUVZSxbtszsWEWyysfM9OnTxwgKCjJcXV2NmjVrGn369DF++eUXs2PZffnll8Z1111nuLm5GQ0bNjRmzpxpdiS7b7/91pBkpKSkmB3FLjMz03jiiSeM2rVrG1WrVjXq1q1rPP/880Z2drbZ0QzDMIyPPvrIqFu3ruHq6moEBgYaw4YNM06cOHHZc5T0+zU/P9948cUXjWuvvdZwc3MzoqKiLtvXuaRsCQkJRT4+duxYU7Nd+Nibom4rV640LdeZM2eMXr16GcHBwYarq6sRFBRk3HXXXcamTZsuaabSZCvK5fyYGUfZTp8+bXTu3NkICAgwqlSpYoSGhhqDBw82Dh8+bGquC2bNmmXUr1/fqFq1qtGsWTNjyZIllzxXabO98847hru7+2X/3VZStvT0dCM2NtYIDg42qlatakRERBjx8fGX5ePRSso2bdo0o1atWkaVKlWM2rVrGy+88MIlfd+yGcYlOrsVAAAAAIAy4BxUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAAAAAJZAQQUAAAAAWAIFFQAAAABgCRRUAAAAAIAlUFABAECZxcbGqmfPnmbHAABcYSioAAAAAABLoKACAIBiffrpp4qMjJS7u7uqV6+u6OhojR49WnPmzNHnn38um80mm82mpKQkSdLBgwd17733qlq1avLz81OPHj20f/9++3gXZl7Hjx+vgIAA+fj4aOjQocrJyXG4z1OnTl3mZw4AMIOL2QEAAIA1paenq2/fvpoyZYp69eqlkydPas2aNerXr5/S0tKUmZmphIQESZKfn59yc3PVpUsX3XTTTVqzZo1cXFw0YcIEde3aVdu3b5erq6skKTExUVWrVlVSUpL279+vAQMGqHr16po4cWKx+zQMw8yXAgBwmVBQAQBAkdLT03Xu3Dn17t1boaGhkqTIyEhJkru7u7KzsxUYGGhf/4MPPlB+fr7ee+892Ww2SVJCQoKqVaumpKQkde7cWZLk6uqq999/Xx4eHmrSpIleeukljR49Wv/5z38c7hMAcOXjEF8AAFCkZs2aKSoqSpGRkbrnnnv07rvv6vjx48Wu/+OPP+qXX36Rt7e3vLy85OXlJT8/P509e1b79u0rMK6Hh4f9/k033aSsrCwdPHiwzPsEAFxZKKgAAKBIzs7OWr58uf73v/+pcePGmjFjhiIiIpSamlrk+llZWWrZsqWSk5ML3Pbs2aP777//kuwTAHBloaACAIBi2Ww2tWvXTuPHj9e2bdvk6uqqxYsXy9XVVXl5eQXWvf7667V3717VqFFD9evXL3Dz9fW1r/fjjz/qzJkz9vsbNmyQl5eXQkJCHO4TAHDlo6ACAIAibdy4UZMmTdIPP/ygtLQ0LVq0SEePHlWjRo0UFham7du3KyUlRceOHVNubq5iYmLk7++vHj16aM2aNUpNTVVSUpIef/xx/fbbb/Zxc3JyNGjQIO3atUtff/21xo4dq+HDh8vJycnhPgEAVz4ukgQAAIrk4+Oj1atXa+rUqcrMzFRoaKji4+N1++23q1WrVkpKSlKrVq2UlZWllStXqmPHjlq9erWeeeYZ9e7dWydPnlTNmjUVFRUlHx8f+7hRUVEKDw9X+/btlZ2drb59+2rcuHEl7hMAcOWzGVy3HQAAXCaxsbE6ceKElixZYnYUAIAFcYgvAAAAAMASKKgAAAAAAEvgEF8AAAAAgCUwgwoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsAQKKgAAAADAEiioAAAAAABLoKACAAAAACyBggoAAAAAsIT/Bx4Dd9RnuY5WAAAAAElFTkSuQmCC", + "text/plain": [ + "
" + ] + }, + "metadata": {}, + "output_type": "display_data" } - ], - "tabbable": null, - "tooltip": null - } - }, - "d58ebfdf143a49bc9915bc2048b64f6a": { - "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_3c635914241b444ab49f98bbb3c218d1", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "df806a0b556d433ba1de5dee8fe1b750": { - "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_b2feb830225a4cecb139b0703c658564", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "e8d161eb329f402fbc87cb3346fd20f2": { - "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_c22dda8a4057465c8f1af23376ed2936", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "e9fff04f857c4a9d9b9bce4415808f18": { - "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_3b27b22ad54446db888d0366e93642b8", - "msg_id": "", - "outputs": [], - "tabbable": null, - "tooltip": null - } - }, - "eaecb40d41574cf282cbba8e83608fb3": { - "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 - } - }, - "ef9ef09005ec4e8a9446a35f87253aa9": { - "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 - } - }, - "fe8c1c71cc404d5ca3dd56ed41caf8f0": { - "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 - } - } + ], + "source": [ + "res = naive_value_iteration(lion, 20, starting_state=lion.get_initial_state())\n", + "labels = [s.labels[0] for s in lion.get_states().values()]\n", + "stormvogel.lib.display_value_iteration_result(res, 10, labels)" + ] }, - "version_major": 2, - "version_minor": 0 - } - } - }, - "nbformat": 4, - "nbformat_minor": 5 + { + "cell_type": "markdown", + "id": "dcbef4f2-78ae-4d2c-9587-9c96becf26b1", + "metadata": {}, + "source": [ + "Note that naive_value_iteration is also available under stormvogel.lib, in case you would like to use it later. However, this implementation is very inefficient so we recommend using the value iteration algorithms from stormpy if you want good performance." + ] + }, + { + "cell_type": "code", + "execution_count": 10, + "id": "12b57306-780c-4a40-898a-f3a95f7ff9eb", + "metadata": {}, + "outputs": [], + "source": [ + "import stormvogel.lib\n", + "res2 = stormvogel.lib.naive_value_iteration(lion, 20, starting_state=lion.get_initial_state())\n", + "assert res == res2" + ] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3 (ipykernel)", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.12.3" + }, + "widgets": { + "application/vnd.jupyter.widget-state+json": { + "state": { + "0a4470793a704b388de44c9e5f08cab8": { + "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_47da0120652c4fa4a503c52d24ee2ebc", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "115e6973c59145688509e9aa5b3010ee": { + "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 + } + }, + "132eeaf7259c4ae6b2349f17d38d49c5": { + "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 + } + }, + "3b27b22ad54446db888d0366e93642b8": { + "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 + } + }, + "3c635914241b444ab49f98bbb3c218d1": { + "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 + } + }, + "47da0120652c4fa4a503c52d24ee2ebc": { + "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 + } + }, + "52791b15670e460ba9fe9376b20cc3a8": { + "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 + } + }, + "55fa0e096dad48d992e69289fe7fdc70": { + "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_132eeaf7259c4ae6b2349f17d38d49c5", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "6c0870de174f4ed69adc6b138d5373f2": { + "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_fe8c1c71cc404d5ca3dd56ed41caf8f0", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "774c3e64c51b44d48f82a07fc88b0ac8": { + "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_ef9ef09005ec4e8a9446a35f87253aa9", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "8c26ed794da84acc93a5a7e7928b5f8c": { + "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_115e6973c59145688509e9aa5b3010ee", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "b2feb830225a4cecb139b0703c658564": { + "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 + } + }, + "b422eb4441534debb7226a46affd3242": { + "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_eaecb40d41574cf282cbba8e83608fb3", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "c22dda8a4057465c8f1af23376ed2936": { + "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 + } + }, + "c2b9fda9e1354d6ca57827715ca601ed": { + "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_52791b15670e460ba9fe9376b20cc3a8", + "msg_id": "", + "outputs": [ + { + "data": { + "text/html": "\n ", + "text/plain": "" + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "tabbable": null, + "tooltip": null + } + }, + "d58ebfdf143a49bc9915bc2048b64f6a": { + "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_3c635914241b444ab49f98bbb3c218d1", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "df806a0b556d433ba1de5dee8fe1b750": { + "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_b2feb830225a4cecb139b0703c658564", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "e8d161eb329f402fbc87cb3346fd20f2": { + "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_c22dda8a4057465c8f1af23376ed2936", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "e9fff04f857c4a9d9b9bce4415808f18": { + "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_3b27b22ad54446db888d0366e93642b8", + "msg_id": "", + "outputs": [], + "tabbable": null, + "tooltip": null + } + }, + "eaecb40d41574cf282cbba8e83608fb3": { + "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 + } + }, + "ef9ef09005ec4e8a9446a35f87253aa9": { + "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 + } + }, + "fe8c1c71cc404d5ca3dd56ed41caf8f0": { + "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 }