{ "cells": [ { "cell_type": "markdown", "id": "0a7e6243", "metadata": {}, "source": [ "# Visual value iteration and Markov Chain evolution\n", "This notebook provides an example of using the stormvogel API for naive value iteration and Markov Chain evolution, and a way to visualize these algorithms.
" ] }, { "cell_type": "markdown", "id": "60e04cbe", "metadata": {}, "source": [ "## Value iteration\n", "This algorithm takes a model and a target state. It then calculates the probability of reaching the target state from all other states iteratively. If a choice has to be made for an action, the action that gives the best result in the previous iteration is chosen. It also takes an additional parameter epsilon, which indicates the target accuracy. A lower value of epsilon gives a more accurate result with more iterations." ] }, { "cell_type": "code", "execution_count": 1, "id": "98a0b860", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:35.686559Z", "iopub.status.busy": "2026-03-26T10:47:35.686331Z", "iopub.status.idle": "2026-03-26T10:47:35.882645Z", "shell.execute_reply": "2026-03-26T10:47:35.882155Z" } }, "outputs": [], "source": [ "from stormvogel import *\n", "\n", "\n", "def naive_value_iteration(\n", " model: Model, epsilon: float, target_state: 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", " target_state (stormvogel.model.State): Target state of the model.\n", "\n", " Returns:\n", " list[list[float]]: The result is a 2D list where result[n][m] is the value of state m at iteration n.\n", " \"\"\"\n", " if epsilon <= 0:\n", " RuntimeError(\"The algorithm will not terminate if epsilon is zero.\")\n", "\n", " # Create a dynamic matrix (list of lists) to store the result.\n", " values_matrix = [[0 for state in model.get_states()]]\n", " values_matrix[0][target_state.id] = 1\n", "\n", " terminate = False\n", " while not terminate:\n", " old_values = values_matrix[len(values_matrix) - 1]\n", " new_values = [None for state in model.get_states()]\n", " for sid, state in model.states.items():\n", " choice = model.get_choice(state)\n", " # Now we have to take a decision for an action.\n", " actions = choice.choice.keys()\n", " action_values = {}\n", " for action, branch in choice.choice.items():\n", " branch_value = sum(\n", " [prob * old_values[state.id] for (prob, state) in branch.branch]\n", " )\n", " action_values[action] = branch_value\n", " # We take the action with the highest value.\n", " highest_value = max(action_values.values())\n", " new_values[sid] = highest_value\n", " values_matrix.append(new_values)\n", " terminate = (\n", " sum([abs(x - y) for (x, y) in zip(new_values, old_values)]) < epsilon\n", " )\n", " return values_matrix" ] }, { "cell_type": "markdown", "id": "1df5d0d0", "metadata": {}, "source": [ "To demonstrate the workings of this algorithm, we use the lion model again." ] }, { "cell_type": "code", "execution_count": 2, "id": "412dabda", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:35.884707Z", "iopub.status.busy": "2026-03-26T10:47:35.884480Z", "iopub.status.idle": "2026-03-26T10:47:36.088405Z", "shell.execute_reply": "2026-03-26T10:47:36.087830Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "lion = examples.create_lion_mdp()\n", "vis = show(lion, layout=Layout(\"layouts/lion.json\"))" ] }, { "cell_type": "markdown", "id": "affb0b3a", "metadata": {}, "source": [ "Now we can display the inner workings of a value iteration algorithm: At the beginning we give the target state a value of 1, then we work backwards, always choosing the action that would maximize the value in the previous iteration. In the end, we always end up converging (This was mathematically proven). The brighter the cell is at the end, the higher the chance that we reach the target state from this state." ] }, { "cell_type": "code", "execution_count": 3, "id": "a0bb03c7", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:36.095640Z", "iopub.status.busy": "2026-03-26T10:47:36.095334Z", "iopub.status.idle": "2026-03-26T10:47:36.477156Z", "shell.execute_reply": "2026-03-26T10:47:36.476611Z" } }, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/tmp/ipykernel_873/351540826.py:29: DeprecationWarning: Call to deprecated method get_choice. (use get_choices instead) -- Deprecated since version 0.10.0.\n", " choice = model.get_choice(state)\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAA5cAAAFUCAYAAACwdsjWAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjcsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvTLEjVAAAAAlwSFlzAAAPYQAAD2EBqD+naQAAM5lJREFUeJzt3Xl8FPXh//H3JjEXuQhXEiBZDkXkFFNOq8EgiAgGFAGp3FQUKoEvCqhAuERUKAiCBS1RBFERsEWRS85auQNBFBAJpBCKiCSEI0Ayvz/8sXXlyDG7mWR5PR+PfcjMzs68P4SYfeczM2szDMMQAAAAAAAmeFkdAAAAAABQ+lEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACm+VgdACVTXl6ejh8/ruDgYNlsNqvjAAAAALCIYRg6e/asoqKi5OV14/lJyiWu6/jx46patarVMQAAAACUEOnp6apSpcoNn6dc4rqCg4MlSf6SPHHecq3VAdysTnOrE7jRfVYHcKPbrQ7gZpFWB3CjUKsDuFGg1QHc7DarA7iRt9UB3IyLu4Bik5UtVb3nfx3hRiiXuK6rp8La5JnlMsjqAG4W4snf2f5WB3AjT38TX8bqAG7kyf9T8eSvm0S5LM0ol0Cxy+9yOb4tAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS7dJC4uTjabTTabTSkpKdc8n5ycrLCwsELvMzExsVCvSU5OduQo7GsBAAAAoKAol27Uv39/ZWRkqG7dukpLS5PNZnM816VLFx04cKBQ+1uyZInGjx/vWLbb7Zo2bZrTNuvXr5fdbnc6TkZGhpo1a1akMQAAAABAQfhYHcCTBQYGKiIi4rrPBQQEKCAgoFD7Cw8PL3SGq8fx9fUt9GsBAAAAoKCYubTI70+LTUpKUsOGDTV//nzZ7XaFhoaqa9euOnv2rGOb354WGxcXpyNHjmjIkCGO014BAAAAwCqUyxLk0KFDWrZsmZYvX67ly5drw4YNevXVV6+77ZIlS1SlShWNGzdOGRkZysjIKOa0AAAAAPA/nBZbTOx2uwzDuOk2eXl5Sk5OVnBwsCTpqaee0tq1azVx4sRrtg0PD5e3t7eCg4OdTr2Ni4tTWlpaofPl5OQoJyfHsZyVlVXofQAAAAC4dTFzWYLY7XZHsZSkyMhInTx5sliOPWnSJIWGhjoeVatWLZbjAgAAAPAMlMsS5LbbbnNattlsysvLK5Zjjxw5UpmZmY5Henp6sRwXAAAAgGfgtNhSzNfXV7m5uS7Zl5+fn/z8/FyyLwAAAAC3HmYuSzG73a6NGzfq2LFjOnXqlNVxAAAAANzCKJel2Lhx45SWlqYaNWqoQoUKVscBAAAAcAuzGfndwhRFEhcXp4YNG2ratGlWR5FU+DxZWVkKDQ1VgCRP/ATNb6wO4Gb17rM6gRs9YHUAN6pldQA3i7I6gBuFWR3AjcpYHcDNbst/k1LL2+oAbsYUCVBsss5KobWkzMxMhYSE3HA7vi3daNasWQoKClJqaqplGRYsWKCgoCBt2rTJsgwAAAAAPB839HGTBQsW6MKFC5Kk6Ohoy3J06NBBTZo0kSSFhYVZlgMAAACAZ6NcuknlypWtjiBJCg4OdvrsTAAAAABwB06LBQAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmOZjdQCUbCcyMxUSEmJ1DDd41+oAbvYvqwO40X6rA7jRCasDuNkpqwO40UWrA7iPccnqBO6Va3UAN8qzOoCbefLXzpPH5uk89fuugP8mmbkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuXSTuLg42Ww22Ww2paSkXHebZcuWqWbNmvL29lZiYmKB9turVy8lJCQ4Hedmr7Xb7Y4cZ86cKXB+AAAAACgMyqUb9e/fXxkZGapbt67S0tJks9mcnn/66af1+OOPKz09XePHj3fJMePi4pScnOxY3rZtmz799FOX7BsAAAAAbsTH6gCeLDAwUBEREdd9Ljs7WydPnlSbNm0UFRXltgwVKlRQeHi42/YPAAAAABIzl5ZYv369goODJUkPPPCAbDab1q9fr6SkJDVs2NBp22nTpslutxd/SAAAAAAoBMqlBZo3b679+/dLkj799FNlZGSoefPmlmbKyclRVlaW0wMAAAAACorTYouJ3W6XYRiSJF9fX1WsWFGSFB4efsNTZ4ti/fr1RXrdpEmTNHbsWJflAAAAAHBrYeYSkqSRI0cqMzPT8UhPT7c6EgAAAIBShJnLEsTLy8sxu3nV5cuXi+XYfn5+8vPzK5ZjAQAAAPA8zFyWIBUqVNCJEyecCuaNPiMTAAAAAEoSymUJEhcXp59++kmvvfaaDh06pLfeeksrVqywOhYAAAAA5ItyWYLUrl1bs2bN0ltvvaUGDRpo69atGjZsmNWxAAAAACBfXHNpkbCwsGuur5SkAQMGaMCAAU7rXnzxRcefk5OTnZ4r6t1hAQAAAMCVmLl0o1mzZikoKEipqamWZahTp47atm1r2fEBAAAA3BqYuXSTBQsW6MKFC5Kk6Ohoy3J88cUXjjvOhoSEWJYDAAAAgGejXLpJ5cqVrY4gSYqJibE6AgAAAIBbAKfFAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATPOxOgBKtojQUNmsDuEGr1gdwM0Ge/KvjTpaHcCNGlkdwM3sVgdwo3CrA7hRsNUB3Mzf6gBu5G11ADfz5J91nv61Q+mTXbDNPPnbEgAAAABQTCiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTilQud+7cqdTUVMfyZ599poSEBL344ou6dOmSy8IBAAAAAEqHIpXLp59+WgcOHJAk/fjjj+ratasCAwP1ySef6IUXXnBpQAAAAABAyVekcnngwAE1bNhQkvTJJ5/ovvvu08KFC5WcnKxPP/3UlfkAAAAAAKVAkcqlYRjKy8uTJK1Zs0YPP/ywJKlq1ao6deqU69IBAAAAAEqFIpXL2NhYTZgwQfPnz9eGDRvUrl07SdLhw4dVqVIllwYEAAAAAJR8RSqX06ZN086dOzVo0CC99NJLqlmzpiRp8eLFat68uUsDAgAAAABKPp+ivKh+/fpOd4u96vXXX5e3t7fpUAAAAACA0qXIn3N55swZvfPOOxo5cqROnz4tSdq3b59OnjzpsnAAAAAAgNKhSDOXe/bsUXx8vMLCwpSWlqb+/fsrPDxcS5Ys0dGjR/X++++7OicAAAAAoAQr0szl0KFD1bt3bx08eFD+/v6O9Q8//LA2btzosnAAAAAAgNKhSOVy27Ztevrpp69ZX7lyZZ04ccJ0KAAAAABA6VKkcunn56esrKxr1h84cEAVKlQwHQoAAAAAULoUqVx26NBB48aN0+XLlyVJNptNR48e1fDhw/XYY4+5NCAAAAAAoOQrUrmcMmWKsrOzVbFiRV24cEH333+/atasqeDgYE2cONHVGZ3ExcXJZrPJZrMpJSXlutskJycrLCzMrTlKklGjRunPf/7zDZ8vyN8ZAAAAAJhRpLvFhoaGavXq1frXv/6l3bt3Kzs7W40aNVKrVq1cne+6+vfvr3Hjxql8+fKSpLS0NFWrVk2GYRTL8UuSEydOaPr06U6fO9qrVy/Z7XYlJSVJkpYsWaJDhw6pcePGFqUEAAAA4OmKVC7ff/99denSRS1atFCLFi0c6y9duqRFixapR48eLgt4PYGBgYqIiHDrMdzFMAzl5ubKx6dIf/XXeOedd9S8eXPFxMTccJvw8PDrXiMLAAAAAK5SpNNie/furczMzGvWnz17Vr179zYdylVWrlyp2rVrKygoSA899JAyMjIcz8XFxSkxMdFp+4SEBPXq1cuxbLfb9corr6hPnz4KDg5WdHS05syZ4/Sar7/+Wg0bNpS/v79iY2O1bNkyp9NP169fL5vNphUrVuiee+6Rn5+fPvjgA3l5eWn79u1O+5o2bZpiYmKUl5dX4DEuWrRI7du3L/D2AAAAAOAORSqXhmHIZrNds/4///mPQkNDTYdyhfPnz+uNN97Q/PnztXHjRh09elTDhg0r9H6mTJmi2NhY7dq1S88++6yeeeYZ7d+/X5KUlZWl9u3bq169etq5c6fGjx+v4cOHX3c/I0aM0KuvvqrvvvtOHTp0UKtWrTRv3jynbebNm6devXrJy+v6X5akpCTZ7XbH8unTp7Vv3z7FxsYWely/l5OTo6ysLKcHAAAAABRUoc7NvPvuux03homPj3c6tTM3N1eHDx/WQw895PKQ+bHb7ddcb3n58mW9/fbbqlGjhiRp0KBBGjduXKH3/fDDD+vZZ5+VJA0fPlx//etftW7dOtWqVUsLFy6UzWbT3Llz5e/vr7vuukvHjh1T//79r9nPuHHj9OCDDzqW+/XrpwEDBmjq1Kny8/PTzp07lZqaqs8+++yGWcqXL+8YjyQdPXpUhmEoKirKabvk5ORCj3PSpEkaO3ZsoV8HAAAAAFIhy2VCQoIkKSUlRW3atFFQUJDjOV9fX9nt9hLzUSSBgYFORSwyMlInT54s9H7q16/v+LPNZlNERIRjP/v371f9+vXl7+/v2OZGN835/exiQkKCBg4cqKVLl6pr165KTk5Wy5YtnWYmf2/QoEEaNGiQY/nChQuS5HT8oho5cqSGDh3qWM7KylLVqlVN7xcAAADAraFQ5XLMmDGSfp0p7NKli0tKjbvcdtttTss2m81pdtPLy+u6s50F2U9hrom8qkyZMk7Lvr6+6tGjh+bNm6dOnTpp4cKFmj59eqH2efVuub/88osqVKhQ6Ey/5efnJz8/P1P7AAAAAHDrKtI1lz179izRxbIgKlSo4HSDn9zcXO3du7dQ+6hVq5ZSU1OVk5PjWLdt27YCv75fv35as2aNZs2apStXrqhTp06FOn6NGjUUEhKiffv2Fep1AAAAAOBqRSqXubm5euONN9S4cWNFREQoPDzc6VEaPPDAA/r888/1+eef6/vvv9czzzyjM2fOFGofTz75pPLy8vTnP/9Z3333nVauXKk33nhDkq57w6Pfq127tpo2barhw4erW7duCggIuOn2M2fOVHx8vGPZy8tLrVq10ubNmwuVGwAAAABcrUjlcuzYsZo6daq6dOmizMxMDR06VJ06dZKXl5eSkpJcHNE9+vTpo549e6pHjx66//77Vb16dbVs2bJQ+wgJCdE///lPpaSkqGHDhnrppZc0evRoSQW/DrJv3766dOmS+vTpk++2p06d0qFDh5zW9evXT4sWLSrSqboAAAAA4Co24/cXHhZAjRo19Oabb6pdu3YKDg5WSkqKY90333yjhQsXuiOrpF8/n7Jhw4aaNm2a245hxoIFCxyfA5rfTKQkjR8/Xp988on27NlTpOMZhqEmTZpoyJAh6tat2w23S0tLU7Vq1bRr1y41bNgw3/1mZWUpNDRUAZLyn4MtfV6xOoCbDS7Sr41KiY5WB3CjRlYHcDO71QHcqHSctFM0wVYHcLPSfZXPzXlbHcDNPPlnnad/7VDqZGVLoU2lzMxMhYSE3HC7In1bnjhxQvXq1ZMkBQUFKTMzU5L0yCOP6PPPPy/KLgtl1qxZCgoKUmpqqtuPlZ/3339fmzdv1uHDh7Vs2TINHz5cTzzxRL7FMjs7W3v37tXMmTP1l7/8pcjHt9lsmjNnjq5cuXLDbdq2bas6deoU+RgAAAAAkJ9C3S32qipVqigjI0PR0dGqUaOGVq1apUaNGmnbtm1uv+PoggULHB/BER0d7dZjFcSJEyc0evRonThxQpGRkercubMmTpyY7+sGDRqkDz/8UAkJCQU6JfZmGjZseNPZyHfeeadE/Z0BAAAA8DxFOi12xIgRCgkJ0YsvvqiPPvpIf/rTn2S323X06FENGTJEr776qjuyohhxWmzpxmmxpRSnxZZenBZbenFabOnlyT/rPP1rh1KnoKfFFmnm8rflsUuXLoqJidHXX3+t22+/Xe3bty/KLgEAAAAApViRyuXGjRvVvHlz+fj8+vKmTZuqadOmunLlijZu3Kj77rvPpSEBAAAAACVbkU4oaNmypU6fPn3N+szMzEJ/nAcAAAAAoPQrUrk0DEM227VX4v38888qU6aM6VAAAAAAgNKlUKfFdurUSdKvH3/Rq1cvpzvD5ubmas+ePWrevLlrEwIAAAAASrxClcvQ0FBJv85cBgcHO32Wo6+vr5o2bar+/fu7NiEAAAAAoMQrVLmcN2+eJKlChQpKSkpSYGCgJCktLU3Lli1T7dq1Vb58edenBAAAAACUaEW65nLXrl16//33JUlnzpxR06ZNNWXKFCUkJGj27NkuDQgAAAAAKPmKXC7/+Mc/SpIWL16sSpUq6ciRI3r//ff15ptvujQgAAAAAKDkK1K5PH/+vIKDgyVJq1atUqdOneTl5aWmTZvqyJEjLg0IAAAAACj5ilQua9asqWXLlik9PV0rV65U69atJUknT55USEiISwMCAAAAAEq+IpXL0aNHa9iwYbLb7WrSpImaNWsm6ddZzLvvvtulAQEAAAAAJV+h7hZ71eOPP657771XGRkZatCggWN9fHy8Onbs6LJwAAAAAIDSoUjlUpIiIiIUERHhtK5x48amAwEAAAAASp8inRYLAAAAAMBvUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmFfmGPkBptsbqAG4Wm2d1Avdp4clfvP9aHcDNqlodwI3CrQ7gRoFWB3Azf6sDuJG31QHczJPHx/QPSpqLBduMf7oAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTLC2XcXFxstlsstlsSklJsTJKgaSlpVma9dKlS6pZs6a+/vprp/XvvvuuWrdufcPX9erVy/H3vGzZMjenBAAAAHArsnzmsn///srIyFDdunUl/a/AFcT69etls9l05swZNyb8n6pVqzplLW5vv/22qlWrpubNmzvWXbx4UaNGjdKYMWMc65KSktSrVy/H8vTp05WRkVGcUQEAAADcYiwvl4GBgYqIiJCPj4+lOS5fvpzvNt7e3pZlNQxDM2fOVN++fZ3WL168WCEhIWrRosUNXxsaGqqIiAh3RwQAAABwC7O8XObnyJEjat++vcqWLasyZcqoTp06+uKLL5SWlqaWLVtKksqWLSubzeaYrfvyyy917733KiwsTOXKldMjjzyiQ4cOOfZ5dXb0o48+0v333y9/f3/Nnj1bAQEBWrFihdPxly5dquDgYJ0/f/6a02KvzpyuXbtWsbGxCgwMVPPmzbV//36nfUyYMEEVK1ZUcHCw+vXrpxEjRqhhw4aF+nvYsWOHDh06pHbt2jmtX7Rokdq3b1+ofQEAAACAq5X4cjlw4EDl5ORo48aNSk1N1eTJkxUUFKSqVavq008/lSTt379fGRkZmj59uiTp3LlzGjp0qLZv3661a9fKy8tLHTt2VF5entO+R4wYocGDB+u7775T586d9cgjj2jhwoVO2yxYsEAJCQkKDAy8YcaXXnpJU6ZM0fbt2+Xj46M+ffo4vX7ixImaPHmyduzYoejoaM2ePTvfcdvtdiUlJTmWN23apDvuuEPBwcFO223evFmxsbH57g8AAAAA3Mnac1Gvw263yzAMx/LRo0f12GOPqV69epKk6tWrO54LDw+XJFWsWFFhYWGO9Y899pjTPv/+97+rQoUK2rdvn9P1komJierUqZNjuXv37nrqqad0/vx5BQYGKisrS59//rmWLl1608wTJ07U/fffL+nXwtquXTtdvHhR/v7+mjFjhvr27avevXtLkkaPHq1Vq1YpOzv7pvusUaOGypcv71g+cuSIoqKinLY5c+aMMjMzr1n/21JaUDk5OcrJyXEsZ2VlFXofAAAAAG5dJX7m8rnnntOECRPUokULjRkzRnv27Mn3NQcPHlS3bt1UvXp1hYSEyG63S/q1qP7W72f8Hn74Yd122236xz/+IUn69NNPFRISolatWt30ePXr13f8OTIyUpJ08uRJSb/OqjZu3Nhp+98vX8/atWs1aNAgx/KFCxfk7+/vtM2FCxck6Zr1RTFp0iSFhoY6HlWrVjW9TwAAAAC3jhJfLvv166cff/xRTz31lFJTUxUbG6sZM2bc9DXt27fX6dOnNXfuXG3ZskVbtmyR9OtHefxWmTJlnJZ9fX31+OOPO06NXbhwobp06ZLvDXxuu+02x5+v3un296fgmlW+fHn98ssvTuvKlSsnm812zfqiGDlypDIzMx2P9PR00/sEAAAAcOso8eVS+vUjQAYMGKAlS5bo//7v/zR37lxJv5ZBScrNzXVs+/PPP2v//v16+eWXFR8fr9q1axeqfHXv3l1ffvmlvv32W3311Vfq3r27qey1atXStm3bnNb9frkg7r77bn3//fdOpwz7+vrqrrvu0r59+0xllCQ/Pz+FhIQ4PQAAAACgoEp8uUxMTNTKlSt1+PBh7dy5U+vWrVPt2rUlSTExMbLZbFq+fLl++uknZWdnq2zZsipXrpzmzJmjH374QV999ZWGDh1a4OPdd999ioiIUPfu3VWtWjU1adLEVP6//OUvevfdd/Xee+/p4MGDmjBhgvbs2ZPvZ3nGx8dr5syZjuWWLVsqOztb3377rdN2bdq00ebNm01lBAAAAACzSny5zM3N1cCBA1W7dm099NBDuuOOOzRr1ixJUuXKlTV27FiNGDFClSpV0qBBg+Tl5aVFixZpx44dqlu3roYMGaLXX3+9wMez2Wzq1q2bdu/ebXrWUvp1JnTkyJEaNmyYGjVqpMOHD6tXr175Xid56NAhnTp1yrFcrlw5dezYUQsWLHDarm/fvvriiy+UmZlpOisAAAAAFJXN+O15lsUsLi5ODRs21LRp06yKYIkHH3xQERERmj9/fqFet2fPHj344IM6dOiQgoKCHOs7d+6sRo0aaeTIkTd9vc1m09KlS5WQkJDvsbKyshQaGqoASTefYy2dHrA6gJuNsDqAG7UItTqBG9WzOoCbefJ9wsKtDuBGN/4kLs9g/p54JZe31QHczJPHV+Knf3CryboohY6XMjMzb3r5nOX/dGfNmqWgoCClpqZaHcUtzp8/r6lTp+rbb7/V999/rzFjxmjNmjXq2bNnofdVv359TZ48WYcPH3Za//rrrzuVzd8bMGDATZ8HAAAAALMsnbk8duyY4+M0oqOjHTfo8SQXLlxQ+/bttWvXLl28eFG1atXSyy+/7PT5mu528uRJx+dWRkZGXnOX3Oth5rJ0Y+aylGLmsvRi5rL0Yuay9PLk8Vk+/QM4K+jM5c0/Y8PNKleubOXhi0VAQIDWrFljaYaKFSuqYsWKlmYAAAAA4Nn4vQgAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0m2EYhtUhUPJkZWUpNDRUAZJsVocBAAAAYBlD0gVJmZmZCgkJueF2zFwCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXBZAXFycbDabbDabUlJSCvSa5ORkhYWFuTVXQY6TlJTkyD5t2jS35wEAAABwa6JcFlD//v2VkZGhunXrKi0tTTabzepI15WcnKy4uDjH8rBhw5SRkaEqVapYFwoAAACAx/OxOkBpERgYqIiICKtjFFpQUJCCgoLk7e1tdRQAAAAAHoyZSxdJTk5WdHS0AgMD1bFjR/3888/XbPPZZ5+pUaNG8vf3V/Xq1TV27FhduXLF8fzUqVNVr149lSlTRlWrVtWzzz6r7OzsQh8HAAAAAIob5dIFtmzZor59+2rQoEFKSUlRy5YtNWHCBKdtNm3apB49emjw4MHat2+f/va3vyk5OVkTJ050bOPl5aU333xT3377rd577z199dVXeuGFFwp1nKLKyclRVlaW0wMAAAAACspmGIZhdYiSLi4uTg0bNrzhDXGefPJJZWZm6vPPP3es69q1q7788kudOXNGktSqVSvFx8dr5MiRjm0++OADvfDCCzp+/Ph197t48WINGDBAp06dKvBxbsRutysxMVGJiYnXfT4pKUljx469Zn2ApJJ5dSkAAACA4mBIuiApMzNTISEhN9yOmUsX+O6779SkSROndc2aNXNa3r17t8aNG+e4BjIoKMhxk6Dz589LktasWaP4+HhVrlxZwcHBeuqpp/Tzzz87ni/IcYpq5MiRyszMdDzS09Ndsl8AAAAAtwZu6FNMsrOzNXbsWHXq1Oma5/z9/ZWWlqZHHnlEzzzzjCZOnKjw8HBt3rxZffv21aVLlxQYGOjWfH5+fvLz83PrMQAAAAB4LsqlC9SuXVtbtmxxWvfNN984LTdq1Ej79+9XzZo1r7uPHTt2KC8vT1OmTJGX168Tyh9//HGhjwMAAAAAVqBcusBzzz2nFi1a6I033tCjjz6qlStX6ssvv3TaZvTo0XrkkUcUHR2txx9/XF5eXtq9e7f27t2rCRMmqGbNmrp8+bJmzJih9u3b61//+pfefvvtQh8HAAAAAKzANZcu0LRpU82dO1fTp09XgwYNtGrVKr388stO27Rp00bLly/XqlWr9Ic//EFNmzbVX//6V8XExEiSGjRooKlTp2ry5MmqW7euFixYoEmTJhX6OAAAAABgBe4WWwD53S22NMjvbrG/l5WVpdDQUO4WCwAAANziuFusi82aNUtBQUFKTU21OkqhvPLKKwoKCtLRo0etjgIAAADAgzFzWQDHjh3ThQsXJEnR0dHy9fW1OFHBnT59WqdPn5YkVahQQaGhoQV6HTOXAAAAAKSCz1xyQ58CqFy5stURiiw8PFzh4eFWxwAAAADg4TgtFgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGCaj9UBUDIZhvHrfy3OAQAAAMBaVzvB1Y5wI5RLXNfZs2clSRctzgEAAACgZDh79qxCQ0Nv+LzNyK9+4paUl5en48ePKzg4WDabza3HysrKUtWqVZWenq6QkBC3HssKnjw+Tx6b5NnjY2yllyePj7GVXp48PsZWenny+Ip7bIZh6OzZs4qKipKX142vrGTmEtfl5eWlKlWqFOsxQ0JCPO4b/7c8eXyePDbJs8fH2EovTx4fYyu9PHl8jK308uTxFefYbjZjeRU39AEAAAAAmEa5BAAAAACYRrmE5fz8/DRmzBj5+flZHcUtPHl8njw2ybPHx9hKL08eH2MrvTx5fIyt9PLk8ZXUsXFDHwAAAACAacxcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1zCcm+99Zbsdrv8/f3VpEkTbd261epILrFx40a1b99eUVFRstlsWrZsmdWRXGbSpEn6wx/+oODgYFWsWFEJCQnav3+/1bFcYvbs2apfv77jQ4mbNWumFStWWB3LLV599VXZbDYlJiZaHcUlkpKSZLPZnB533nmn1bFc5tixY/rTn/6kcuXKKSAgQPXq1dP27dutjuUSdrv9mq+dzWbTwIEDrY5mWm5urkaNGqVq1aopICBANWrU0Pjx4+Up91M8e/asEhMTFRMTo4CAADVv3lzbtm2zOlaR5Pdz2zAMjR49WpGRkQoICFCrVq108OBBa8IWUn5jW7JkiVq3bq1y5crJZrMpJSXFkpxFcbOxXb58WcOHD1e9evVUpkwZRUVFqUePHjp+/Lh1gQspv69dUlKS7rzzTpUpU0Zly5ZVq1attGXLFmvCinIJi3300UcaOnSoxowZo507d6pBgwZq06aNTp48aXU0086dO6cGDRrorbfesjqKy23YsEEDBw7UN998o9WrV+vy5ctq3bq1zp07Z3U006pUqaJXX31VO3bs0Pbt2/XAAw/o0Ucf1bfffmt1NJfatm2b/va3v6l+/fpWR3GpOnXqKCMjw/HYvHmz1ZFc4pdfflGLFi102223acWKFdq3b5+mTJmismXLWh3NJbZt2+b0dVu9erUkqXPnzhYnM2/y5MmaPXu2Zs6cqe+++06TJ0/Wa6+9phkzZlgdzSX69eun1atXa/78+UpNTVXr1q3VqlUrHTt2zOpohZbfz+3XXntNb775pt5++21t2bJFZcqUUZs2bXTx4sViTlp4+Y3t3LlzuvfeezV58uRiTmbezcZ2/vx57dy5U6NGjdLOnTu1ZMkS7d+/Xx06dLAgadHk97W74447NHPmTKWmpmrz5s2y2+1q3bq1fvrpp2JO+v8ZgIUaN25sDBw40LGcm5trREVFGZMmTbIwletJMpYuXWp1DLc5efKkIcnYsGGD1VHcomzZssY777xjdQyXOXv2rHH77bcbq1evNu6//35j8ODBVkdyiTFjxhgNGjSwOoZbDB8+3Lj33nutjlFsBg8ebNSoUcPIy8uzOopp7dq1M/r06eO0rlOnTkb37t0tSuQ658+fN7y9vY3ly5c7rW/UqJHx0ksvWZTKNX7/czsvL8+IiIgwXn/9dce6M2fOGH5+fsaHH35oQcKiu9l7ksOHDxuSjF27dhVrJlcpyPutrVu3GpKMI0eOFE8oFyrI+DIzMw1Jxpo1a4on1O8wcwnLXLp0STt27FCrVq0c67y8vNSqVSv9+9//tjAZCiszM1OSFB4ebnES18rNzdWiRYt07tw5NWvWzOo4LjNw4EC1a9fO6XvPUxw8eFBRUVGqXr26unfvrqNHj1odySX+8Y9/KDY2Vp07d1bFihV19913a+7cuVbHcotLly7pgw8+UJ8+fWSz2ayOY1rz5s21du1aHThwQJK0e/dubd68WW3btrU4mXlXrlxRbm6u/P39ndYHBAR4zFkDVx0+fFgnTpxw+v9maGiomjRpwnuWUiYzM1M2m01hYWFWR3G5S5cuac6cOQoNDVWDBg0syeBjyVEBSadOnVJubq4qVarktL5SpUr6/vvvLUqFwsrLy1NiYqJatGihunXrWh3HJVJTU9WsWTNdvHhRQUFBWrp0qe666y6rY7nEokWLtHPnzlJ7TdTNNGnSRMnJyapVq5YyMjI0duxY/fGPf9TevXsVHBxsdTxTfvzxR82ePVtDhw7Viy++qG3btum5556Tr6+vevbsaXU8l1q2bJnOnDmjXr16WR3FJUaMGKGsrCzdeeed8vb2Vm5uriZOnKju3btbHc204OBgNWvWTOPHj1ft2rVVqVIlffjhh/r3v/+tmjVrWh3PpU6cOCFJ133PcvU5lHwXL17U8OHD1a1bN4WEhFgdx2WWL1+url276vz584qMjNTq1atVvnx5S7JQLgGYMnDgQO3du9ejfktdq1YtpaSkKDMzU4sXL1bPnj21YcOGUl8w09PTNXjwYK1evfqamQZP8NuZoPr166tJkyaKiYnRxx9/rL59+1qYzLy8vDzFxsbqlVdekSTdfffd2rt3r95++22PK5fvvvuu2rZtq6ioKKujuMTHH3+sBQsWaOHChapTp45SUlKUmJioqKgoj/jazZ8/X3369FHlypXl7e2tRo0aqVu3btqxY4fV0QAnly9f1hNPPCHDMDR79myr47hUy5YtlZKSolOnTmnu3Ll64okntGXLFlWsWLHYs3BaLCxTvnx5eXt767///a/T+v/+97+KiIiwKBUKY9CgQVq+fLnWrVunKlWqWB3HZXx9fVWzZk3dc889mjRpkho0aKDp06dbHcu0HTt26OTJk2rUqJF8fHzk4+OjDRs26M0335SPj49yc3OtjuhSYWFhuuOOO/TDDz9YHcW0yMjIa365Ubt2bY857feqI0eOaM2aNerXr5/VUVzm+eef14gRI9S1a1fVq1dPTz31lIYMGaJJkyZZHc0latSooQ0bNig7O1vp6enaunWrLl++rOrVq1sdzaWuvi/hPUvpdLVYHjlyRKtXr/aoWUtJKlOmjGrWrKmmTZvq3XfflY+Pj959911LslAuYRlfX1/dc889Wrt2rWNdXl6e1q5d61HXt3kiwzA0aNAgLV26VF999ZWqVatmdSS3ysvLU05OjtUxTIuPj1dqaqpSUlIcj9jYWHXv3l0pKSny9va2OqJLZWdn69ChQ4qMjLQ6imktWrS45uN+Dhw4oJiYGIsSuce8efNUsWJFtWvXzuooLnP+/Hl5eTm/3fL29lZeXp5FidyjTJkyioyM1C+//KKVK1fq0UcftTqSS1WrVk0RERFO71mysrK0ZcsW3rOUcFeL5cGDB7VmzRqVK1fO6khuZ+X7Fk6LhaWGDh2qnj17KjY2Vo0bN9a0adN07tw59e7d2+popmVnZzvNmBw+fFgpKSkKDw9XdHS0hcnMGzhwoBYuXKjPPvtMwcHBjutNQkNDFRAQYHE6c0aOHKm2bdsqOjpaZ8+e1cKFC7V+/XqtXLnS6mimBQcHX3NdbJkyZVSuXDmPuF522LBhat++vWJiYnT8+HGNGTNG3t7e6tatm9XRTBsyZIiaN2+uV155RU888YS2bt2qOXPmaM6cOVZHc5m8vDzNmzdPPXv2lI+P57w9ad++vSZOnKjo6GjVqVNHu3bt0tSpU9WnTx+ro7nEypUrZRiGatWqpR9++EHPP/+87rzzzlL5czy/n9uJiYmaMGGCbr/9dlWrVk2jRo1SVFSUEhISrAtdQPmN7fTp0zp69Kjj8x+v/jIrIiKixM/M3mxskZGRevzxx7Vz504tX75cubm5jvcs4eHh8vX1tSp2gd1sfOXKldPEiRPVoUMHRUZG6tSpU3rrrbd07Ngx6z7KyZJ71AK/MWPGDCM6Otrw9fU1GjdubHzzzTdWR3KJdevWGZKuefTs2dPqaKZdb1ySjHnz5lkdzbQ+ffoYMTExhq+vr1GhQgUjPj7eWLVqldWx3MaTPoqkS5cuRmRkpOHr62tUrlzZ6NKli/HDDz9YHctl/vnPfxp169Y1/Pz8jDvvvNOYM2eO1ZFcauXKlYYkY//+/VZHcamsrCxj8ODBRnR0tOHv729Ur17deOmll4ycnByro7nERx99ZFSvXt3w9fU1IiIijIEDBxpnzpyxOlaR5PdzOy8vzxg1apRRqVIlw8/Pz4iPjy81/17zG9u8efOu+/yYMWMszV0QNxvb1Y9Wud5j3bp1VkcvkJuN78KFC0bHjh2NqKgow9fX14iMjDQ6dOhgbN261bK8NsMwDDf1VgAAAADALYJrLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BALjF9OrVSwkJCVbHAAB4GMolAAAAAMA0yiUAAB5q8eLFqlevngICAlSuXDm1atVKzz//vN577z199tlnstlsstlsWr9+vSQpPT1dTzzxhMLCwhQeHq5HH31UaWlpjv1dnfEcO3asKlSooJCQEA0YMECXLl266THPnTtXzCMHAFjBx+oAAADA9TIyMtStWze99tpr6tixo86ePatNmzapR48eOnr0qLKysjRv3jxJUnh4uC5fvqw2bdqoWbNm2rRpk3x8fDRhwgQ99NBD2rNnj3x9fSVJa9eulb+/v9avX6+0tDT17t1b5cqV08SJE294TMMwrPyrAAAUE8olAAAeKCMjQ1euXFGnTp0UExMjSapXr54kKSAgQDk5OYqIiHBs/8EHHygvL0/vvPOObDabJGnevHkKCwvT+vXr1bp1a0mSr6+v/v73vyswMFB16tTRuHHj9Pzzz2v8+PE3PSYAwPNxWiwAAB6oQYMGio+PV7169dS5c2fNnTtXv/zyyw233717t3744QcFBwcrKChIQUFBCg8P18WLF3Xo0CGn/QYGBjqWmzVrpuzsbKWnpxf6mAAAz0K5BADAA3l7e2v16tVasWKF7rrrLs2YMUO1atXS4cOHr7t9dna27rnnHqWkpDg9Dhw4oCeffNItxwQAeBbKJQAAHspms6lFixYaO3asdu3aJV9fXy1dulS+vr7Kzc112rZRo0Y6ePCgKlasqJo1azo9QkNDHdvt3r1bFy5ccCx/8803CgoKUtWqVW96TACA56NcAgDggbZs2aJXXnlF27dv19GjR7VkyRL99NNPql27tux2u/bs2aP9+/fr1KlTunz5srp3767y5cvr0Ucf1aZNm3T48GGtX79ezz33nP7zn/849nvp0iX17dtX+/bt0xdffKExY8Zo0KBB8vLyuukxAQCejxv6AADggUJCQrRx40ZNmzZNWVlZiomJ0ZQpU9S2bVvFxsZq/fr1io2NVXZ2ttatW6e4uDht3LhRw4cPV6dOnXT27FlVrlxZ8fHxCgkJcew3Pj5et99+u+677z7l5OSoW7duSkpKyveYAADPZzO4PzgAACiAXr166cyZM1q2bJnVUQAAJRCnxQIAAAAATKNcAgAAAABM47RYAAAAAIBpzFwCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABM+38/J0kUHdhYqwAAAABJRU5ErkJggg==", "text/plain": [ "
" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "target = lion.get_states_with_label(\"full\")[0]\n", "res = naive_value_iteration(lion, 0.003, target)\n", "labels = lion.get_ordered_labels()\n", "extensions.display_value_iteration_result(res, 10, labels)" ] }, { "cell_type": "markdown", "id": "ee683515", "metadata": {}, "source": [ "Note that naive_value_iteration is also available under `stormvogel.extensions`, 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": 4, "id": "92e482ac", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:36.479059Z", "iopub.status.busy": "2026-03-26T10:47:36.478777Z", "iopub.status.idle": "2026-03-26T10:47:36.483560Z", "shell.execute_reply": "2026-03-26T10:47:36.482992Z" }, "lines_to_next_cell": 2 }, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "res2 = extensions.naive_value_iteration(\n", " lion, 0.003, lion.get_states_with_label(\"full\")[0]\n", ")\n", "res == res2" ] }, { "cell_type": "markdown", "id": "261eb9ab", "metadata": { "lines_to_next_cell": 2 }, "source": [ "## DTMC evolution\n", "An algorithm that is similar to naive value iteration. This time, there is no target state. The algorithm simply applies every probabilistic transition (hence it only works for DTMCs)\n", "\n", "This example simulates a die using coin flips." ] }, { "cell_type": "code", "execution_count": 5, "id": "06e22841", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:36.485254Z", "iopub.status.busy": "2026-03-26T10:47:36.485089Z", "iopub.status.idle": "2026-03-26T10:47:36.491020Z", "shell.execute_reply": "2026-03-26T10:47:36.490519Z" } }, "outputs": [], "source": [ "def dtmc_evolution(model: stormvogel.model.Model, steps: int) -> list[list[float]]:\n", " \"\"\"Run DTMC evolution. 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", "\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][model.get_initial_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.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" ] }, { "cell_type": "code", "execution_count": 6, "id": "f17fe323", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:36.492566Z", "iopub.status.busy": "2026-03-26T10:47:36.492398Z", "iopub.status.idle": "2026-03-26T10:47:36.522812Z", "shell.execute_reply": "2026-03-26T10:47:36.522296Z" } }, "outputs": [ { "data": { "text/html": [ "\n", "\n", "\n", " \n", " Network\n", " \n", " \n", " \n", " \n", " \n", "
\n", " \n", " \n", " \n", "\n" ], "text/plain": [ "" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "stormvogel_dtmc = mapping.stormpy_to_stormvogel(examples.example_building_dtmcs_01())\n", "vis = show(stormvogel_dtmc)" ] }, { "cell_type": "code", "execution_count": 7, "id": "ca5fe355", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:36.529691Z", "iopub.status.busy": "2026-03-26T10:47:36.529512Z", "iopub.status.idle": "2026-03-26T10:47:36.713352Z", "shell.execute_reply": "2026-03-26T10:47:36.712884Z" } }, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/tmp/ipykernel_873/642448037.py:24: DeprecationWarning: Call to deprecated method get_branch. (use get_branches instead) -- Deprecated since version 0.10.0.\n", " branch = model.get_branch(s)\n" ] }, { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAA6IAAALeCAYAAACwb6yJAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjcsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvTLEjVAAAAAlwSFlzAAAPYQAAD2EBqD+naQAAV3pJREFUeJzt3XucV3WBP/7XB3BGYGAIbwMIjokXBBXJUqRyvKy31vWyhRqZqLG12Sp5SV1TwRvZqmHr4pa6Ui59q6+39mte8yto7HpvEJP1lgjaFBkxI4ijwvz+6OfnuxNemGE8Hxiez8fjPJZzPu9zzut8xo158T6f8ym1tbW1BQAAAArSo9IBAAAA2LgoogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACtWr0gHY8K1evTq//e1v069fv5RKpUrHAQAAKqStrS2vvfZaBg8enB493nveUxFlnf32t7/N0KFDKx0DAABYTyxevDhbb731e76uiLLO+vXrl+TP/7H179+/wmm6Rl1tbaUjAADABqctyRv5fx3hvSiirLN3bsft379/tymibjAGAIDO+6CP7HlYEQAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIroeaGhoSKlUSqlUSmNj4xqvz5w5MwMGDOjwMSdPntyhfWbOnFnO0dF9AQAA1pYiup6YNGlSmpqaMmrUqCxcuDClUqn82tFHH51nn322Q8e75ZZbctFFF5XX6+vrM3369HZjZs+enfr6+nbnaWpqytixYzt1DQAAAGujV6UD8Gd9+vRJXV3du77Wu3fv9O7du0PHGzhwYIczvHOeqqqqDu8LAACwtsyIbgD+8tbcKVOmZPTo0bnxxhtTX1+f2traHHPMMXnttdfKY/7nrbkNDQ156aWX8vWvf7186y0AAEClKKIbqBdeeCG33XZbbr/99tx+++2ZM2dOvvWtb73r2FtuuSVbb711LrzwwjQ1NaWpqWmdzt3a2pqWlpZ2CwAAwNpSRNdD9fX1aWtre98xq1evzsyZMzNq1Kh86lOfynHHHZf77rvvXccOHDgwPXv2TL9+/VJXV1e+BbihoSELFy7scL5p06altra2vAwdOrTDxwAAADZeiugGqr6+Pv369SuvDxo0KEuWLCnk3Oecc06am5vLy+LFiws5LwAA0D14WNEGapNNNmm3XiqVsnr16kLOXV1dnerq6kLOBQAAdD9mRDcSVVVVWbVqVaVjAAAAKKIbi/r6+jzwwAN55ZVX8uqrr1Y6DgAAsBFTRDcSF154YRYuXJjtttsuW2yxRaXjAAAAG7FS2wc9npUPXUNDQ0aPHp3p06dXOkqSjudpaWlJbW1tmpub079//w83XEH6+q5VAADosLYkK5MP7AZmRNcTM2bMSE1NTebPn1+xDLNmzUpNTU0efPDBimUAAAC6PzOi64FXXnklK1euTJIMGzYsVVVVFcnx2muv5fe//32SZMCAAdl8883Xaj8zogAAQLL2M6K+vmU9MGTIkEpHSJL069ev3XeTAgAAfBjcmgsAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAAChUr0oHoPuoq61NqdIhusiKCZVO0HX6zqp0gq712UoH6GI3VTpAF9qi0gG62B8qHaCLbVLpAF3orUoHAGCdmREFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEU0Y1UQ0NDSqVSSqVSGhsbs3DhwvL66NGjKx0PAADoxhTRjdikSZPS1NSUUaNGZejQoWlqasrpp59e6VgAAEA316vSAaicPn36pK6urrxeV1eXmpqaCiYCAAA2BmZEAQAAKJQZUTqstbU1ra2t5fWWlpYKpgEAADY0ZkTpsGnTpqW2tra8DB06tNKRAACADYgiSoedc845aW5uLi+LFy+udCQAAGAD4tZcOqy6ujrV1dWVjgEAAGygzIgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCK6EZsxowZqampyfz587No0aLU1NTk0ksvrXQsAACgm/PU3I3UrFmzsnLlyiTJsGHD0qNHjzQ2NiaJJ+ICAAAfKkV0IzVkyJA1tg0fPrwCSQAAgI2NW3MBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpohuphoaGlEqllEqlNDY2ZuHCheX10aNHVzoeAADQjSmiG7FJkyalqakpo0aNytChQ9PU1JTTTz+90rEAAIBurlelA1A5ffr0SV1dXXm9rq4uNTU1FUwEAABsDBRROqy1tTWtra3l9ZaWlgqmAQAANjRuzaXDpk2bltra2vIydOjQSkcCAAA2IIooHXbOOeekubm5vCxevLjSkQAAgA2IW3PpsOrq6lRXV1c6BgAAsIEyIwoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoR3YjNmDEjNTU1mT9/fhYtWpSamppceumllY4FAAB0c76+ZSM1a9asrFy5MkkybNiw9OjRI42NjUniq1kAAIAPlSK6kRoyZMga24YPH16BJAAAwMbGrbkAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFCoXpUOAOujvrMqnaDr/LjSAbrYMZUO0MV2rnSALvR0pQN0sb6VDtDFVlQ6QBfqWekAXWxVpQMAVIAZUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShHdSDU0NKRUKqVUKqWxsTELFy4sr48ePbrS8QAAgG5MEd2ITZo0KU1NTRk1alSGDh2apqamnH766ZWOBQAAdHO9Kh2AyunTp0/q6urK63V1dampqalgIgAAYGNgRhQAAIBCmRGlw1pbW9Pa2lpeb2lpqWAaAABgQ2NGlA6bNm1aamtry8vQoUMrHQkAANiAKKJ02DnnnJPm5ubysnjx4kpHAgAANiBuzaXDqqurU11dXekYAADABsqMKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYhuxGbMmJGamprMnz8/ixYtSk1NTS699NJKxwIAALo5T83dSM2aNSsrV65MkgwbNiw9evRIY2NjkngiLgAA8KFSRDdSQ4YMWWPb8OHDK5AEAADY2Lg1FwAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCK6kWpoaEipVEqpVEpjY2MWLlxYXh89enSl4wEAAN2YIroRmzRpUpqamjJq1KgMHTo0TU1NOf300ysdCwAA6OZ6VToAldOnT5/U1dWV1+vq6lJTU1PBRAAAwMbAjCgAAACFMiNKh7W2tqa1tbW83tLSUsE0AADAhsaMKB02bdq01NbWlpehQ4dWOhIAALABUUTpsHPOOSfNzc3lZfHixZWOBAAAbEDcmkuHVVdXp7q6utIxAACADZQZUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShHdiM2YMSM1NTWZP39+Fi1alJqamlx66aWVjgUAAHRznpq7kZo1a1ZWrlyZJBk2bFh69OiRxsbGJPFEXAAA4EOliG6khgwZssa24cOHVyAJAACwsXFrLgAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEV0I9XQ0JBSqZRSqZTGxsYsXLiwvD569OhKxwMAALoxRXQjNmnSpDQ1NWXUqFEZOnRompqacvrpp1c6FgAA0M31qnQAKqdPnz6pq6srr9fV1aWmpqaCiQAAgI2BIkqHtba2prW1tbze0tJSwTQAAMCGxq25dNi0adNSW1tbXoYOHVrpSAAAwAZEEaXDzjnnnDQ3N5eXxYsXVzoSAACwAXFrLh1WXV2d6urqSscAAAA2UGZEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIbsRkzZqSmpibz58/PokWLUlNTk0svvbTSsQAAgG7O17dspGbNmpWVK1cmSYYNG5YePXqksbExSXw1CwAA8KFSRDdSQ4YMWWPb8OHDK5AEAADY2Lg1FwAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACtWpIvrEE09k/vz55fWf/exnOeKII/KP//iPefPNN7ssHAAAAN1Pp4rol7/85Tz77LNJkt/85jc55phj0qdPn/zv//2/841vfKNLAwIAANC9dKqIPvvssxk9enSS5H//7/+dT3/60/nRj36UmTNn5uabb+7KfAAAAHQznSqibW1tWb16dZLkF7/4RQ499NAkydChQ/Pqq692XToAAAC6nU4V0T322CMXX3xxbrzxxsyZMyef+cxnkiQvvvhittpqqy4NCAAAQPfSqSI6ffr0PPHEE/na176Wc889N8OHD0+S3HTTTdl77727NCAAAADdS6mtra2tqw72xhtvpGfPntlkk0266pBsAFpaWlJbW5veSUqVDsMaflzpAF3smEoH6GI7VzpAF3q60gG6WN9KB+hiKyodoAv1rHSALraq0gEAulBbkpVJmpub079///cc1+nvEV22bFmuu+66nHPOOVm6dGmS5Omnn86SJUs6e0gAAAA2Ar06s9OTTz6Z/fffPwMGDMjChQszadKkDBw4MLfccksWLVqUH/7wh12dEwAAgG6iUzOip512Wk444YQ899xz2XTTTcvbDz300DzwwANdFg4AAIDup1NF9NFHH82Xv/zlNbYPGTIkv/vd79Y5FAAAAN1Xp4podXV1Wlpa1tj+7LPPZosttljnUAAAAHRfnSqif/M3f5MLL7wwb731VpKkVCpl0aJFOeuss/K3f/u3XRoQAACA7qVTRfSKK67I8uXLs+WWW2blypXZZ599Mnz48PTr1y+XXHJJV2fkQ9DQ0JBSqZRSqZTGxsYsXLiwvD569OhKxwMAALqxTj01t7a2Nvfee2/mzp2befPmZfny5RkzZkwOOOCArs7Hh2jSpEm58MILs/nmm6dUKqWpqSmXX355fvGLX1Q6GgAA0I11qoj+8Ic/zNFHH51x48Zl3Lhx5e1vvvlmfvzjH+eLX/xilwXkw9OnT5/U1dWV1+vq6lJTU1PBRAAAwMagU7fmnnDCCWlubl5j+2uvvZYTTjhhnUMBAADQfXVqRrStrS2lUmmN7S+//HJqa2vXORTrt9bW1rS2tpbX3+0JygAAAO+lQ0V09913Lz/QZv/990+vXv9v91WrVuXFF1/MwQcf3OUhWb9MmzYtU6dOrXQMAABgA9WhInrEEUckSRobG3PQQQe1+zxhVVVV6uvrfX3LRuCcc87JaaedVl5vaWnJ0KFDK5gIAADYkHSoiF5wwQVJkvr6+hx99NHZdNNNP5RQrN+qq6tTXV1d6RgAAMAGqlOfET3++OO7OgcAAAAbiU4V0VWrVuU73/lOfvrTn2bRokV58803272+dOnSLgkHAABA99Opr2+ZOnVqrrzyyhx99NFpbm7OaaedlqOOOio9evTIlClTujgiAAAA3UmniuisWbNy7bXX5vTTT0+vXr1y7LHH5rrrrsv555+fhx56qKszAgAA0I10qoj+7ne/yy677JIkqampSXNzc5Lkr//6r/Pzn/+869LxoZoxY0Zqamoyf/78LFq0KDU1Nbn00ksrHQsAAOjmOvUZ0a233jpNTU0ZNmxYtttuu9xzzz0ZM2ZMHn30UU9T3UDMmjUrK1euTJIMGzYsPXr0SGNjY5L4GQIAAB+qThXRI488Mvfdd1/23HPP/MM//EO+8IUv5Prrr8+iRYvy9a9/vasz8iEYMmTIGtuGDx9egSQAAMDGptTW1ta2rgd56KGH8p//+Z/Zfvvtc9hhh3VFLjYgLS0tqa2tTe8kpUqHYQ0/rnSALnZMpQN0sZ0rHaALPV3pAF2sb6UDdLEVlQ7QhXpWOkAXW1XpAABdqC3JyiTNzc3p37//e47r1IzoAw88kL333ju9ev1597322it77bVX3n777TzwwAP59Kc/3ZnDAgAAsBHo1MOK9t1333f9rtDm5ubsu+++6xwKAACA7qtTRbStrS2l0po3Yf7xj39M377d7WYmAAAAulKHbs096qijkiSlUikTJ05s93TVVatW5cknn8zee+/dtQkBAADoVjpURGtra5P8eUa0X79+6d27d/m1qqqq7LXXXpk0aVLXJgQAAKBb6VARveGGG5IkW2yxRaZMmZI+ffokSRYuXJjbbrstI0aMyOabb971KQEAAOg2OvUZ0V/96lf54Q9/mCRZtmxZ9tprr1xxxRU54ogjcs0113RpQAAAALqXThfRT33qU0mSm266KVtttVVeeuml/PCHP8x3v/vdLg0IAABA99KpIvr666+nX79+SZJ77rknRx11VHr06JG99torL730UpcGBAAAoHvpVBEdPnx4brvttixevDh33313DjzwwCTJkiVL0r9//y4NCAAAQPfSqSJ6/vnn54wzzkh9fX323HPPjB07NsmfZ0d33333Lg0IAABA99Khp+a+47Of/Ww++clPpqmpKbvttlt5+/77758jjzyyy8IBAADQ/XSqiCZJXV1d6urq2m37xCc+sc6BAAAA6N46dWsuAAAAdJYiCgAAQKE6fWsusGE4ptIButhnKx2A97RPpQPwvjapdAAANgqtSb6zFuPMiAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUBtMEW1oaEipVEqpVEpjY+Na7zdz5swMGDDgQ8vV3UyZMqX8Pk+fPr3ScQAAgG5ogymiSTJp0qQ0NTVl1KhRSZKFCxemVCpVONW7mzhxYqZMmdKhfUqlUhYuXPih5HkvM2fOTENDQ3n9jDPOSFNTU7beeutCcwAAABuPXpUO0BF9+vRJXV1dpWN0azU1NampqUnPnj0rHQUAAOimNqgZ0bUxc+bMDBs2LH369MmRRx6ZP/7xj2uMueaaa7LddtulqqoqO+64Y2688cZ2r5dKpVx33XU58sgj06dPn2y//fb5j//4j3ZjnnrqqRxyyCGpqanJVlttleOOOy6vvvpql17LnDlz8olPfCLV1dUZNGhQzj777Lz99tvl1xsaGnLKKafkG9/4RgYOHJi6uro1ZmGXLVuWL33pS9liiy3Sv3//7Lfffpk3b16X5gQAAOiIblVEH3744Zx00kn52te+lsbGxuy77765+OKL24259dZbc+qpp+b000/PU089lS9/+cs54YQTcv/997cbN3Xq1IwfPz5PPvlkDj300EyYMCFLly5N8udyt99++2X33XfPY489lrvuuiu///3vM378+C67lldeeSWHHnpoPv7xj2fevHm55pprcv31169xPT/4wQ/St2/fPPzww/n2t7+dCy+8MPfee2/59c997nNZsmRJ7rzzzjz++OMZM2ZM9t9///K1dEZra2taWlraLQAAAGur1NbW1lbpEGujoaEho0ePft8H6Hz+859Pc3Nzfv7zn5e3HXPMMbnrrruybNmyJMm4ceMycuTIfP/73y+PGT9+fFasWFHer1Qq5Zvf/GYuuuiiJMmKFStSU1OTO++8MwcffHAuvvjiPPjgg7n77rvLx3j55ZczdOjQPPPMM9lhhx3W+XrPPffc3HzzzVmwYEH5c7AzZszIWWedlebm5vTo0SMNDQ1ZtWpVHnzwwfJ+n/jEJ7LffvvlW9/6Vn75y1/mM5/5TJYsWZLq6urymOHDh+cb3/hG/u7v/u49z19fX5/Jkydn8uTJa7w2ZcqUTJ06dY3tvZOsn5/YpTv5bKUD8J62qHQA3tcmlQ4AwEahNcl3kjQ3N6d///7vOa5bzYguWLAge+65Z7ttY8eOXWPMuHHj2m0bN25cFixY0G7brrvuWv5z3759079//yxZsiRJMm/evNx///3lz1PW1NRkp512SpK88MILXXYtY8eObfcwpnHjxmX58uV5+eWX3zVnkgwaNKhdzuXLl2ezzTZrl/XFF19cp5znnHNOmpuby8vixYs7fSwAAGDjs0E9rKhIm2zS/t+OS6VSVq9enSRZvnx5DjvssFx22WVr7Ddo0KBC8r3jg3IOGjQos2fPXmO/dflKm+rq6nYzrAAAAB3RrYroiBEj8vDDD7fb9tBDD60xZu7cuTn++OPL2+bOnZudd955rc8zZsyY3Hzzzamvr0+vXh/OWzhixIjcfPPNaWtrK8+Kzp07N/369Vvrr1YZM2ZMfve736VXr16pr6//UHICAAB0VLe6NfeUU07JXXfdlcsvvzzPPfdcrr766tx1113txpx55pmZOXNmrrnmmjz33HO58sorc8stt+SMM85Y6/OcfPLJWbp0aY499tg8+uijeeGFF3L33XfnhBNOyKpVq7rkWr761a9m8eLF+Yd/+If893//d372s5/lggsuyGmnnZYePdbux3bAAQdk7NixOeKII3LPPfdk4cKF+c///M+ce+65eeyxx7okJwAAQEd1qyK611575dprr81VV12V3XbbLffcc0+++c1vthtzxBFH5Kqrrsrll1+ekSNH5nvf+15uuOGGNDQ0rPV5Bg8enLlz52bVqlU58MADs8suu2Ty5MkZMGDAe5bEKVOmdGhWcsiQIbnjjjvyyCOPZLfddstXvvKVnHTSSWtcz/splUq544478ulPfzonnHBCdthhhxxzzDF56aWXstVWW631cQAAALpSt3pq7vrs+OOPT6lUysyZMysdZa2831Nz/1JLS0tqa2s9NZdCeGru+stTc9dvnpoLQBG65VNzZ8yYkZqamsyfP7/SUTqkra0ts2fPLn8dzPrs0ksvTU1NTRYtWlTpKAAAQDe1wcyIvvLKK1m5cmWSZNiwYamqqqpwou5p6dKlWbp0aZJkiy22SG1t7QfuY0aUIpkRXX+ZEV2/mREFoAhrOyO6wTw1d8iQIZWOsFEYOHBgBg4cWOkYAABAN7ZB3ZoLAADAhk8RBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChNpgi2tDQkFKplFKplMbGxrXeb+bMmRkwYMCHlqu7qa+vL7/Py5Ytq3QcAACgG9pgimiSTJo0KU1NTRk1alSSZOHChSmVShVO9e4mTpyYKVOmdGifUqmUhQsXJklmz55dSBlsaGjIzJkzy+uPPvpobr755g/1nAAAwMatV6UDdESfPn1SV1dX6Rjd2hZbbJGBAwdWOgYAANCNbVAzomtj5syZGTZsWPr06ZMjjzwyf/zjH9cYc80112S77bZLVVVVdtxxx9x4443tXi+VSrnuuuty5JFHpk+fPtl+++3zH//xH+3GPPXUUznkkENSU1OTrbbaKscdd1xeffXVLrmGhQsXZt99902SfOQjH0mpVMrEiRNz++23Z8CAAVm1alWSpLGxMaVSKWeffXZ53y996Uv5whe+UF6/+eabM3LkyFRXV6e+vj5XXHHFOudrbW1NS0tLuwUAAGBtdasi+vDDD+ekk07K1772tTQ2NmbffffNxRdf3G7MrbfemlNPPTWnn356nnrqqXz5y1/OCSeckPvvv7/duKlTp2b8+PF58sknc+ihh2bChAlZunRpkmTZsmXZb7/9svvuu+exxx7LXXfdld///vcZP358l1zH0KFDy7fHPvPMM2lqaspVV12VT33qU3nttdfyq1/9KkkyZ86cbL755pk9e3Z53zlz5qShoSFJ8vjjj2f8+PE55phjMn/+/EyZMiXnnXdeu1txO2PatGmpra0tL0OHDl2n4wEAABuXUltbW1ulQ6yNhoaGjB49OtOnT3/PMZ///OfT3Nycn//85+VtxxxzTO66667yZy3HjRuXkSNH5vvf/355zPjx47NixYryfqVSKd/85jdz0UUXJUlWrFiRmpqa3HnnnTn44INz8cUX58EHH8zdd99dPsbLL7+coUOH5plnnskOO+ywztc7e/bs7LvvvvnTn/7U7mFLH/vYx3LsscfmjDPOyJFHHpmPf/zjmTp1av74xz+mubk5W2+9dZ599tlsv/32mTBhQv7whz/knnvuKe//jW98Iz//+c/z61//usPnfkdra2taW1vL6y0tLRk6dGh6J1k/P7FLd/LZSgfgPW1R6QC8r00qHQCAjUJrku8kaW5uTv/+/d9zXLeaEV2wYEH23HPPdtvGjh27xphx48a12zZu3LgsWLCg3bZdd921/Oe+ffumf//+WbJkSZJk3rx5uf/++1NTU1NedtpppyTJCy+80GXX82722WefzJ49O21tbXnwwQdz1FFHZcSIEfnlL3+ZOXPmZPDgwdl+++2TvPe1Pvfcc+Xbezujuro6/fv3b7cAAACsrQ3qYUVF2mST9v92XCqVsnr16iTJ8uXLc9hhh+Wyyy5bY79BgwZ9qLkaGhryb//2b5k3b1422WST7LTTTmloaMjs2bPzpz/9Kfvss8+Hen4AAIB11a1mREeMGJGHH3643baHHnpojTFz585tt23u3LnZeeed1/o8Y8aMya9//evU19dn+PDh7Za+fft2/gL+h6qqqiRZY+bync+Jfuc73ymXzneK6OzZs8ufD03e+1p32GGH9OzZs0tyAgAAdFS3KqKnnHJK7rrrrlx++eV57rnncvXVV+euu+5qN+bMM8/MzJkzc8011+S5557LlVdemVtuuSVnnHHGWp/n5JNPztKlS3Psscfm0UcfzQsvvJC77747J5xwwjrd8vo/bbPNNimVSrn99tvzhz/8IcuXL0/y56fo7rrrrpk1a1a5dH7605/OE088kWeffbbdjOjpp5+e++67LxdddFGeffbZ/OAHP8jVV1/doWsFAADoat2qiO6111659tprc9VVV2W33XbLPffck29+85vtxhxxxBG56qqrcvnll2fkyJH53ve+lxtuuKHdTOIHGTx4cObOnZtVq1blwAMPzC677JLJkydnwIAB6dHj3d/SKVOmpL6+fq3PMWTIkEydOjVnn312ttpqq3zta18rv7bPPvtk1apV5cwDBw7MzjvvnLq6uuy4447lcWPGjMlPf/rT/PjHP86oUaNy/vnn58ILL8zEiRPXOgcAAEBX61ZPzV2fHX/88SmVSuv81SlF+KCn5v6llpaW1NbWemouhfDU3PWXp+au3zw1F4AidMun5s6YMSM1NTWZP39+paN0SFtbW2bPnl3+Opj12ciRI3PIIYdUOgYAANCNbTBPzZ01a1ZWrlyZJBk2bFiF03RMqVTKSy+9VOkYa+WOO+7IW2+9lSS+lgUAAPhQbDBFdMiQIZWOsFHYZpttKh0BAADo5jaoW3MBAADY8CmiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIWqaBFtaGhIqVRKqVRKY2Njh/atr6/P9OnTP5RclbBw4cJOvQ9dbcqUKeWfSXd6fwEAgPVHxWdEJ02alKampowaNSrJ/ytk75g5c2YGDBhQoXTvbsqUKZk4cWKH9qmvr8/s2bM/lDzrYubMmWloaCivn3HGGWlqasrWW29duVAAAEC31qvSAfr06ZO6urpCzvXWW29lk002KeRcG6qamprU1NSkZ8+elY4CAAB0UxWfEX0/s2fPzgknnJDm5uby7aJTpkwpv/7666/nxBNPTL9+/TJs2LB8//vfL7/2zszqT37yk+yzzz7ZdNNNM2vWrCTJddddlxEjRmTTTTfNTjvtlBkzZrQ77+LFizN+/PgMGDAgAwcOzOGHH56FCxd26bU98sgj2X333bPppptmjz32yK9+9as1xsyZMyef+MQnUl1dnUGDBuXss8/O22+/XX69oaEhp5xySr7xjW9k4MCBqaura/f+JMmyZcvypS99KVtssUX69++f/fbbL/PmzevSawEAAOiI9bqI7r333pk+fXr69++fpqamNDU15Ywzzii/fsUVV5RL3Fe/+tX8/d//fZ555pl2xzj77LNz6qmnZsGCBTnooIMya9asnH/++bnkkkuyYMGCXHrppTnvvPPygx/8IMmfZ00POuig9OvXLw8++GDmzp2bmpqaHHzwwXnzzTe75LqWL1+ev/7rv87OO++cxx9/PFOmTGl3XUnyyiuv5NBDD83HP/7xzJs3L9dcc02uv/76XHzxxe3G/eAHP0jfvn3z8MMP59vf/nYuvPDC3HvvveXXP/e5z2XJkiW588478/jjj2fMmDHZf//9s3Tp0k7nb21tTUtLS7sFAABgbVX81ty/VF9fn7a2tiRJVVVVamtrUyqV3vX23UMPPTRf/epXkyRnnXVWvvOd7+T+++/PjjvuWB4zefLkHHXUUeX1Cy64IFdccUV527bbbpunn3463/ve93L88cfnJz/5SVavXp3rrruu/FnVG264IQMGDMjs2bNz4IEHrjHruDb+54zqj370o6xevTrXX399Nt1004wcOTIvv/xy/v7v/748ZsaMGRk6dGiuvvrqlEql7LTTTvntb3+bs846K+eff3569PjzvyHsuuuuueCCC5Ik22+/fa6++urcd999+au/+qv88pe/zCOPPJIlS5akuro6SXL55Zfntttuy0033ZS/+7u/y8SJEzv8eddp06Zl6tSpHX4PAAAAkvWwiHbErrvuWv7zO2V1yZIl7cbsscce5T+vWLEiL7zwQk466aRMmjSpvP3tt99ObW1tkmTevHl5/vnn069fv3bHeeONN/LCCy90Se4FCxZk1113zaabblreNnbs2DXGjB07tt2Dm8aNG5fly5fn5ZdfzrBhw5K0fw+SZNCgQeX3YN68eVm+fHk222yzdmNWrly5Ttdyzjnn5LTTTiuvt7S0ZOjQoZ0+HgAAsHHZoIvoXz54qFQqZfXq1e229e3bt/zn5cuXJ0muvfba7Lnnnu3GvfNwnuXLl+djH/tY+fOk/9MWW2zRJbm70vu9B8uXL8+gQYPe9Wm96/Ik4urq6vIMKwAAQEet90W0qqoqq1at6pJjbbXVVhk8eHB+85vfZMKECe86ZsyYMfnJT36SLbfcMv379++S8/6lESNG5MYbb8wbb7xRnhV96KGH1hhz8803p62trTwrOnfu3PTr12+tv1plzJgx+d3vfpdevXqlvr6+S68BAACgs9brhxUlf/7M6PLly3Pffffl1Vdfzeuvv75Ox5s6dWqmTZuW7373u3n22Wczf/783HDDDbnyyiuTJBMmTMjmm2+eww8/PA8++GBefPHFzJ49O6ecckpefvnlrrikfP7zn0+pVMqkSZPy9NNP54477sjll1/ebsxXv/rVLF68OP/wD/+Q//7v/87PfvazXHDBBTnttNPKnw/9IAcccEDGjh2bI444Ivfcc08WLlyY//zP/8y5556bxx57rEuuBQAAoKPW+yK699575ytf+UqOPvrobLHFFvn2t7+9Tsf70pe+lOuuuy433HBDdtlll+yzzz6ZOXNmtt122yR//l7TBx54IMOGDctRRx2VESNG5KSTTsobb7zxnjOkM2fObPdZzg9SU1OT//N//k/mz5+f3XffPeeee24uu+yydmOGDBmSO+64I4888kh22223fOUrX8lJJ52Ub37zm2t9nlKplDvuuCOf/vSnc8IJJ2SHHXbIMccck5deeilbbbXVWh8HAACgK5Xa3nlEbQU0NDRk9OjRmT59eqUidIkLLrggc+bMedfPYm6o6uvrM3ny5EyePPkDx7a0tKS2tja9k6x9HYfO+WylA/Ce1r9P0fM/bfLBQwBgnbUm+U6S5ubm9/2oY8VnRGfMmJGamprMnz+/0lE67c4771znmdr1xaWXXpqamposWrSo0lEAAIBuqqIzoq+88kpWrlyZJBk2bFiqqqoqFYX/39KlS7N06dIkf35K8Dtfa/N+zIhSJDOi6y8zous3M6IAFGFtZ0Qr+tTcIUOGVPL0vIuBAwdm4MCBlY4BAAB0YxW/NRcAAICNiyIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEKt10W0oaEhpVIppVIpjY2N7znutttuy/Dhw9OzZ89Mnjy5sHxdqb6+PtOnT69ohtmzZ5ff7yOOOKKiWQAAgO5rvS6iSTJp0qQ0NTVl1KhRSZKFCxemVCq1G/PlL385n/3sZ7N48eJcdNFFH2qe2bNnp76+vkP7TJw4MVOmTPlQ8qyLv3wv99577zQ1NWX8+PEVTAUAAHR3vSod4IP06dMndXV17/n68uXLs2TJkhx00EEZPHjwh5rlrbfe+lCPX2lVVVWpq6tL796909raWuk4AABAN7Xez4i+n9mzZ6dfv35Jkv322y+lUimzZ89Oktx8880ZOXJkqqurU19fnyuuuKLdvqVSKbfddlu7bQMGDMjMmTOT/L/Zwp/85CfZZ599summm2bWrFldknvJkiU57LDD0rt372y77bbvetxFixbl8MMPT01NTfr375/x48fn97//ffn1KVOmZPTo0bnxxhtTX1+f2traHHPMMXnttdfKY1avXp1p06Zl2223Te/evbPbbrvlpptu6pJrAAAA6KwNuojuvffeeeaZZ5L8uXg2NTVl7733zuOPP57x48fnmGOOyfz58zNlypScd9555ZLZEWeffXZOPfXULFiwIAcddFCX5J44cWIWL16c+++/PzfddFNmzJiRJUuWlF9fvXp1Dj/88CxdujRz5szJvffem9/85jc5+uij2x3nhRdeyG233Zbbb789t99+e+bMmZNvfetb5denTZuWH/7wh/nXf/3X/PrXv87Xv/71fOELX8icOXPWKX9ra2taWlraLQAAAGtrvb819y/V19enra0tyZ9vJd1yyy2TJAMHDizfwnvllVdm//33z3nnnZck2WGHHfL000/nn/7pnzJx4sQOnW/y5Mk56qijyuuDBg3KwoULO3SM/1mAn3322dx555155JFH8vGPfzxJcv3112fEiBHlMffdd1/mz5+fF198MUOHDk2S/PCHP8zIkSPz6KOPlvdbvXp1Zs6cWZ4VPu6443LfffflkksuSWtray699NL84he/yNixY5MkH/3oR/PLX/4y3/ve97LPPvu0ey87Ytq0aZk6dWqH9wMAAEg28BnR97JgwYKMGzeu3bZx48blueeey6pVqzp0rD322KMro2XBggXp1atXPvaxj5W37bTTThkwYEC7MUOHDi2X0CTZeeedM2DAgCxYsKC8rb6+vlxCkz+X5HdmVp9//vm8/vrr+au/+qvU1NSUlx/+8Id54YUX1ukazjnnnDQ3N5eXxYsXr9PxAACAjcsGNyPaVUql0hqzge/2MKK+ffsWFanDNtlkk3brpVIpq1evTvLnhzglyc9//vMMGTKk3bjq6up1Om91dfU6HwMAANh4dcsiOmLEiMydO7fdtrlz52aHHXZIz549kyRbbLFFmpqayq8/99xzef311z/0bDvttFPefvvtPP744+VbbJ955pksW7asXf7Fixdn8eLF5VnRp59+OsuWLcvOO++8VufZeeedU11dnUWLFmWfffbp8usAAADorG5ZRE8//fR8/OMfz0UXXZSjjz46//Vf/5Wrr746M2bMKI/Zb7/9cvXVV2fs2LFZtWpVzjrrrDVmGD8MO+64Yw4++OB8+ctfzjXXXJNevXpl8uTJ6d27d3nMAQcckF122SUTJkzI9OnT8/bbb+erX/1q9tlnn7W+Vbhfv34544wz8vWvfz2rV6/OJz/5yTQ3N2fu3Lnp379/jj/++A/rEgEAAN5Xt/yM6JgxY/LTn/40P/7xjzNq1Kicf/75ufDCC9s9qOiKK67I0KFD86lPfSqf//znc8YZZ6RPnz4dPtc7X/PyztfGrI0bbrghgwcPzj777JOjjjoqf/d3f1d+6FLy51tsf/azn+UjH/lIPv3pT+eAAw7IRz/60fzkJz/pULaLLroo5513XqZNm5YRI0bk4IMPzs9//vNsu+22HToOAABAVyq1deaxqQVpaGjI6NGjM3369EpHeU/3339/jjrqqPzmN7/JRz7ykUrH6RITJ07MsmXL1vie1ffS0tKS2tra9E5S+lCTQfLZSgfgPW1R6QC8rw//nh8ASFqTfCdJc3Nz+vfv/57j1vsZ0RkzZqSmpibz58+vdJR3dccdd+Qf//Efu0UJffDBB1NTU5NZs2ZVOgoAANCNrdczoq+88kpWrlyZJBk2bFiqqqoqnKh7W7lyZV555ZUkSU1NTfl7WT+IGVGKZEZ0/WVGdP1mRhSAIqztjOh6/bCiv/zaET5cvXv3zvDhwysdAwAA6ObW+1tzAQAA6F4UUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUaoMpog0NDSmVSimVSmlsbFzr/WbOnJkBAwZ8aLk+THPnzs0uu+ySTTbZJEcccURmz56dUqmUZcuWfWjnnDhxYvl9vu222z608wAAABuvDaaIJsmkSZPS1NSUUaNGJUkWLlyYUqlU4VTvbuLEiZkyZUqH9imVSlm4cGF5/bTTTsvo0aPz4osvZubMmdl7773T1NSU2traLss5ZcqUTJw4sbx+1VVXpampqcuODwAA8Jc2qCLap0+f1NXVpVevXpWOUogXXngh++23X7beeusMGDAgVVVVqaur+1DLd21tberq6j604wMAAGxQRXRtzJw5M8OGDUufPn1y5JFH5o9//OMaY6655ppst912qaqqyo477pgbb7yx3eulUinXXXddjjzyyPTp0yfbb799/uM//qPdmKeeeiqHHHJIampqstVWW+W4447Lq6++2iXX8M5M7x//+MeceOKJKZVKmTlzZrtbc1taWtK7d+/ceeed7fa99dZb069fv7z++utJksWLF2f8+PEZMGBABg4cmMMPP7zdrGtntLa2pqWlpd0CAACwtrpVEX344Ydz0kkn5Wtf+1oaGxuz77775uKLL2435tZbb82pp56a008/PU899VS+/OUv54QTTsj999/fbtzUqVMzfvz4PPnkkzn00EMzYcKELF26NEmybNmy7Lffftl9993z2GOP5a677srvf//7jB8/vkuuY+jQoWlqakr//v0zffr0NDU15eijj243pn///vnrv/7r/OhHP2q3fdasWTniiCPSp0+fvPXWWznooIPSr1+/PPjgg5k7d25qampy8MEH58033+x0vmnTpqW2tra8DB06tNPHAgAANj6ltra2tkqHWBsNDQ0ZPXp0pk+f/p5jPv/5z6e5uTk///nPy9uOOeaY3HXXXeUH/IwbNy4jR47M97///fKY8ePHZ8WKFeX9SqVSvvnNb+aiiy5KkqxYsSI1NTW58847c/DBB+fiiy/Ogw8+mLvvvrt8jJdffjlDhw7NM888kx122KFLrnnAgAGZPn16+TOcs2fPzr777ps//elPGTBgQG677bYcd9xx+f3vf58+ffqkpaUlW221VW699dYcfPDB+fd///dcfPHFWbBgQfl23jfffLO874EHHvie5y6VSrn11ltzxBFHrPFaa2trWltby+stLS0ZOnRoeidZPz+xS3fy2UoH4D1tUekAvK9NKh0AgI1Ca5LvJGlubk7//v3fc1y3mhFdsGBB9txzz3bbxo4du8aYcePGtds2bty4LFiwoN22XXfdtfznvn37pn///lmyZEmSZN68ebn//vtTU1NTXnbaaackf/5cZ1EOPfTQbLLJJuXbhm+++eb0798/BxxwQDnn888/n379+pVzDhw4MG+88cY65ayurk7//v3bLQAAAGtr43jqTydsskn7fzsulUpZvXp1kmT58uU57LDDctlll62x36BBgwrJlyRVVVX57Gc/mx/96Ec55phj8qMf/ShHH310+WFOy5cvz8c+9rHMmjVrjX232MLcBQAAUBndqoiOGDEiDz/8cLttDz300Bpj5s6dm+OPP768be7cudl5553X+jxjxozJzTffnPr6+oo/wXfChAn5q7/6q/z617/O//2//7fdZ2LHjBmTn/zkJ9lyyy3NWgIAAOuNbnVr7imnnJK77rorl19+eZ577rlcffXVueuuu9qNOfPMMzNz5sxcc801ee6553LllVfmlltuyRlnnLHW5zn55JOzdOnSHHvssXn00Ufzwgsv5O67784JJ5yQVatWdfVlva9Pf/rTqaury4QJE7Ltttu2uzV5woQJ2XzzzXP44YfnwQcfzIsvvpjZs2fnlFNOycsvv1xoTgAAgHd0qyK611575dprr81VV12V3XbbLffcc0+++c1vthtzxBFH5Kqrrsrll1+ekSNH5nvf+15uuOGGNDQ0rPV5Bg8enLlz52bVqlU58MADs8suu2Ty5MkZMGBAevR497d0ypQpqa+vX4ere3elUinHHnts5s2blwkTJrR7rU+fPnnggQcybNiwHHXUURkxYkROOumkvPHGG2ZIAQCAiulWT81dnx1//PHl7wPdELzfU3P/UktLS2praz01l0J4au76yyfP12+emgtAEbrlU3NnzJiRmpqazJ8/v9JROqStrS2zZ88ufx3M+uwrX/lKampqKh0DAADoxjaYGdFXXnklK1euTJIMGzYsVVVVFU7UPS1ZsiQtLS1J/vwE4L59+37gPmZEKZIZ0fWXGdH1mxlRAIqwtjOiG8xTc4cMGVLpCBuFLbfcMltuuWWlYwAAAN3YBnVrLgAAABs+RRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUBt8EW1oaEipVEqpVEpjY2OH9589e3ZKpVKWLVvW5dk6YuLEiTniiCMqmiFJ+b0cMGBApaMAAADd1AZfRJNk0qRJaWpqyqhRo5IkCxcuTKlUWqt999577zQ1NaW2tnatz1cqlbJw4cK1Hj9z5sw0NDSs9fgi1dfXZ/bs2eX1pqamTJ8+vWJ5AACA7q9XpQN0hT59+qSurq5T+1ZVVXV63+6orq6uQ6UcAACgo7rFjOgHeemll3LYYYflIx/5SPr27ZuRI0fmjjvuSLLmrbknnnhidt1117S2tiZJ3nzzzey+++754he/2GV5Vq1aldNOOy0DBgzIZpttlm984xtpa2trN6a1tTWnnHJKttxyy2y66ab55Cc/mUcffbT8+ju577vvvuyxxx7p06dP9t577zzzzDPtjvOzn/0sY8aMyaabbpqPfvSjmTp1at5+++0uuxYAAICO2iiK6Mknn5zW1tY88MADmT9/fi677LLU1NS869jvfve7WbFiRc4+++wkybnnnptly5bl6quv7rI8V1xxRWbOnJl/+7d/yy9/+cssXbo0t956a7sx3/jGN3LzzTfnBz/4QZ544okMHz48Bx10UJYuXdpu3Lnnnpsrrrgijz32WHr16pUTTzyx/NqDDz6YL37xizn11FPz9NNP53vf+15mzpyZSy65ZJ3yt7a2pqWlpd0CAACwtrrFrbl/qb6+vt0M46JFi/K3f/u32WWXXZIkH/3oR99z35qamvz7v/979tlnn/Tr1y/Tp0/P/fffn/79+5fH/OXs5QeZOHFiJk6cWF6fPn16zjnnnBx11FFJkn/913/N3XffXX59xYoVueaaazJz5swccsghSZJrr7029957b66//vqceeaZ5bGXXHJJ9tlnnyTJ2Wefnc985jN54403summm2bq1Kk5++yzc/zxx5ev+6KLLso3vvGNXHDBBUnSoc+6vmPatGmZOnVqh/cDAABINpIZ0VNOOSUXX3xxxo0blwsuuCBPPvnk+44fO3ZszjjjjFx00UU5/fTT88lPfrLLsjQ3N6epqSl77rlneVuvXr2yxx57lNdfeOGFvPXWWxk3blx52yabbJJPfOITWbBgQbvj7brrruU/Dxo0KEmyZMmSJMm8efNy4YUXpqampry882Cn119/vdPXcM4556S5ubm8LF68uNPHAgAANj4bRRH90pe+lN/85jc57rjjMn/+/Oyxxx7553/+5/ccv3r16sydOzc9e/bM888/X2DSjttkk03Kf37nScGrV69OkixfvjxTp05NY2NjeZk/f36ee+65bLrppp0+Z3V1dfr3799uAQAAWFsbRRFNkqFDh+YrX/lKbrnllpx++um59tpr33PsP/3TP+W///u/M2fOnNx111254YYbuixHbW1tBg0alIcffri87e23387jjz9eXt9uu+1SVVWVuXPnlre99dZbefTRR7Pzzjuv9bnGjBmTZ555JsOHD19j6dFjo/nRAwAA65lu+RnRvzR58uQccsgh2WGHHfKnP/0p999/f0aMGPGuY3/1q1/l/PPPz0033ZRx48blyiuvzKmnnpp99tnnfT9b2hGnnnpqvvWtb2X77bfPTjvtlCuvvLL81N4k6du3b/7+7/8+Z555ZgYOHJhhw4bl29/+dl5//fWcdNJJa32e888/P3/913+dYcOG5bOf/Wx69OiRefPm5amnnsrFF1/cJdcCAADQURvFtNiqVaty8sknZ8SIETn44IOzww47ZMaMGWuMe+ONN/KFL3whEydOzGGHHZYk+bu/+7vsu+++Oe6447Jq1ap3PX59fX2mTJmy1nlOP/30HHfccTn++OMzduzY9OvXL0ceeWS7Md/61rfyt3/7tznuuOMyZsyYPP/887n77rvzkY98ZK3Pc9BBB+X222/PPffck49//OPZa6+98p3vfCfbbLPNWh8DAACgq5XaOvoI2PVMQ0NDRo8enenTp1fk/K+//no222yz3HnnnWloaKhIhq42c+bMTJ48ud0s7ftpaWlJbW1teicpfajJIPlspQPwnraodADe1yYfPAQA1llrku/kzw9pfb9nyXSLGdEZM2akpqYm8+fPL/zc999/f/bbb79uU0Jramryla98pdIxAACAbmyDnxF95ZVXsnLlyiTJsGHDUlVVVeFEG7Z3nhLcs2fPbLvttmu1jxlRimRGdP1lRnT9ZkYUgCKs7YzoBv+woiFDhlQ6QrcyfPjwSkcAAAC6uW5xay4AAAAbDkUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChelU6ABu+tra2P//fCudg4/BmpQPwnlorHYD3tbrSAQDYKLzz+8A7HeG9KKKss9deey1J8kaFc7Bx+HGlAwAA8IFee+211NbWvufrpbYPqqrwAVavXp3f/va36devX0ql0od2npaWlgwdOjSLFy9O//79P7TzFKE7XUvietZn3elaEtezPutO15K4nvVZd7qWxPWsz7rTtSTFXU9bW1tee+21DB48OD16vPcnQc2Iss569OiRrbfeurDz9e/fv1v8j0HSva4lcT3rs+50LYnrWZ91p2tJXM/6rDtdS+J61mfd6VqSYq7n/WZC3+FhRQAAABRKEQUAAKBQiigbjOrq6lxwwQWprq6udJR11p2uJXE967PudC2J61mfdadrSVzP+qw7XUvietZn3elakvXvejysCAAAgEKZEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRNgj/8i//kvr6+my66abZc88988gjj1Q6Uqc98MADOeywwzJ48OCUSqXcdtttlY7UadOmTcvHP/7x9OvXL1tuuWWOOOKIPPPMM5WO1SnXXHNNdt111/KXPI8dOzZ33nlnpWN1mW9961splUqZPHlypaN0ypQpU1IqldotO+20U6Vjddorr7ySL3zhC9lss83Su3fv7LLLLnnssccqHatT6uvr1/jZlEqlnHzyyZWO1imrVq3Keeedl2233Ta9e/fOdtttl4suuigb6rMdX3vttUyePDnbbLNNevfunb333juPPvpopWOtlQ/6+7KtrS3nn39+Bg0alN69e+eAAw7Ic889V5mwa+GDrueWW27JgQcemM022yylUimNjY0Vybk23u9a3nrrrZx11lnZZZdd0rdv3wwePDhf/OIX89vf/rZygT/AB/1spkyZkp122il9+/bNRz7ykRxwwAF5+OGHKxN2LXTkd82vfOUrKZVKmT59emH53qGIst77yU9+ktNOOy0XXHBBnnjiiey222456KCDsmTJkkpH65QVK1Zkt912y7/8y79UOso6mzNnTk4++eQ89NBDuffee/PWW2/lwAMPzIoVKyodrcO23nrrfOtb38rjjz+exx57LPvtt18OP/zw/PrXv650tHX26KOP5nvf+1523XXXSkdZJyNHjkxTU1N5+eUvf1npSJ3ypz/9KePGjcsmm2ySO++8M08//XSuuOKKfOQjH6l0tE559NFH2/1c7r333iTJ5z73uQon65zLLrss11xzTa6++uosWLAgl112Wb797W/nn//5nysdrVO+9KUv5d57782NN96Y+fPn58ADD8wBBxyQV155pdLRPtAH/X357W9/O9/97nfzr//6r3n44YfTt2/fHHTQQXnjjTcKTrp2Puh6VqxYkU9+8pO57LLLCk7Wce93La+//nqeeOKJnHfeeXniiSdyyy235Jlnnsnf/M3fVCDp2vmgn80OO+yQq6++OvPnz88vf/nL1NfX58ADD8wf/vCHgpOunbX9XfPWW2/NQw89lMGDBxeU7C+0wXruE5/4RNvJJ59cXl+1alXb4MGD26ZNm1bBVF0jSdutt95a6RhdZsmSJW1J2ubMmVPpKF3iIx/5SNt1111X6Rjr5LXXXmvbfvvt2+699962ffbZp+3UU0+tdKROueCCC9p22223SsfoEmeddVbbJz/5yUrH+NCceuqpbdttt13b6tWrKx2lUz7zmc+0nXjiie22HXXUUW0TJkyoUKLOe/3119t69uzZdvvtt7fbPmbMmLZzzz23Qqk65y//vly9enVbXV1d2z/90z+Vty1btqyturq67X/9r/9VgYQd835//7/44ottSdp+9atfFZqps9bmd5lHHnmkLUnbSy+9VEyodbA219Pc3NyWpO0Xv/hFMaHWwXtdz8svv9w2ZMiQtqeeeqptm222afvOd75TeDYzoqzX3nzzzTz++OM54IADytt69OiRAw44IP/1X/9VwWS8m+bm5iTJwIEDK5xk3axatSo//vGPs2LFiowdO7bScdbJySefnM985jPt/n9oQ/Xcc89l8ODB+ehHP5oJEyZk0aJFlY7UKf/xH/+RPfbYI5/73Oey5ZZbZvfdd8+1115b6Vhd4s0338y///u/58QTT0ypVKp0nE7Ze++9c9999+XZZ59NksybNy+//OUvc8ghh1Q4Wce9/fbbWbVqVTbddNN223v37r3B3lHwjhdffDG/+93v2v1vW21tbfbcc0+/H6yHmpubUyqVMmDAgEpHWWdvvvlmvv/976e2tja77bZbpeN0yurVq3PcccflzDPPzMiRIyuWo1fFzgxr4dVXX82qVauy1VZbtdu+1VZb5b//+78rlIp3s3r16kyePDnjxo3LqFGjKh2nU+bPn5+xY8fmjTfeSE1NTW699dbsvPPOlY7VaT/+8Y/zxBNPbDCfB3s/e+65Z2bOnJkdd9wxTU1NmTp1aj71qU/lqaeeSr9+/Sodr0N+85vf5Jprrslpp52Wf/zHf8yjjz6aU045JVVVVTn++OMrHW+d3HbbbVm2bFkmTpxY6SiddvbZZ6elpSU77bRTevbsmVWrVuWSSy7JhAkTKh2tw/r165exY8fmoosuyogRI7LVVlvlf/2v/5X/+q//yvDhwysdb5387ne/S5J3/f3gnddYP7zxxhs566yzcuyxx6Z///6VjtNpt99+e4455pi8/vrrGTRoUO69995svvnmlY7VKZdddll69eqVU045paI5FFGgS5x88sl56qmnNuh/Zd9xxx3T2NiY5ubm3HTTTTn++OMzZ86cDbKMLl68OKeeemruvffeNWZDNkT/czZq1113zZ577pltttkmP/3pT3PSSSdVMFnHrV69OnvssUcuvfTSJMnuu++ep556Kv/6r/+6wRfR66+/PoccckjlPm/UBX76059m1qxZ+dGPfpSRI0emsbExkydPzuDBgzfIn8+NN96YE088MUOGDEnPnj0zZsyYHHvssXn88ccrHY2NwFtvvZXx48enra0t11xzTaXjrJN99903jY2NefXVV3Pttddm/Pjxefjhh7PllltWOlqHPP7447nqqqvyxBNPVPzOFbfmsl7bfPPN07Nnz/z+979vt/33v/996urqKpSKv/S1r30tt99+e+6///5svfXWlY7TaVVVVRk+fHg+9rGPZdq0adltt91y1VVXVTpWpzz++ONZsmRJxowZk169eqVXr16ZM2dOvvvd76ZXr15ZtWpVpSOukwEDBmSHHXbI888/X+koHTZo0KA1/nFjxIgRG+ytxu946aWX8otf/CJf+tKXKh1lnZx55pk5++yzc8wxx2SXXXbJcccdl69//euZNm1apaN1ynbbbZc5c+Zk+fLlWbx4cR555JG89dZb+ehHP1rpaOvknd8B/H6w/nqnhL700ku59957N+jZ0CTp27dvhg8fnr322ivXX399evXqleuvv77SsTrswQcfzJIlSzJs2LDy7wcvvfRSTj/99NTX1xeaRRFlvVZVVZWPfexjue+++8rbVq9enfvuu2+D/+xed9DW1pavfe1rufXWW/N//+//zbbbblvpSF1q9erVaW1trXSMTtl///0zf/78NDY2lpc99tgjEyZMSGNjY3r27FnpiOtk+fLleeGFFzJo0KBKR+mwcePGrfE1R88++2y22WabCiXqGjfccEO23HLLfOYzn6l0lHXy+uuvp0eP9r8e9ezZM6tXr65Qoq7Rt2/fDBo0KH/6059y99135/DDD690pHWy7bbbpq6urt3vBy0tLXn44Yf9frAeeKeEPvfcc/nFL36RzTbbrNKRutyG+jvCcccdlyeffLLd7weDBw/OmWeembvvvrvQLG7NZb132mmn5fjjj88ee+yRT3ziE5k+fXpWrFiRE044odLROmX58uXtZnFefPHFNDY2ZuDAgRk2bFgFk3XcySefnB/96Ef52c9+ln79+pU/l1NbW5vevXtXOF3HnHPOOTnkkEMybNiwvPbaa/nRj36U2bNnF/4/yl2lX79+a3xWt2/fvtlss802yM/wnnHGGTnssMOyzTbb5Le//W0uuOCC9OzZM8cee2ylo3XY17/+9ey999659NJLM378+DzyyCP5/ve/n+9///uVjtZpq1evzg033JDjjz8+vXpt2L9aHHbYYbnkkksybNiwjBw5Mr/61a9y5ZVX5sQTT6x0tE65++6709bWlh133DHPP/98zjzzzOy0004bxN+hH/T35eTJk3PxxRdn++23z7bbbpvzzjsvgwcPzhFHHFG50O/jg65n6dKlWbRoUfn7Nt/5B6u6urr1bpb3/a5l0KBB+exnP5snnngit99+e1atWlX+/WDgwIGpqqqqVOz39H7Xs9lmm+WSSy7J3/zN32TQoEF59dVX8y//8i955ZVX1tuvqfqg/9b+8h8GNtlkk9TV1WXHHXcsNmjhz+mFTvjnf/7ntmHDhrVVVVW1feITn2h76KGHKh2p0+6///62JGssxx9/fKWjddi7XUeSthtuuKHS0TrsxBNPbNtmm23aqqqq2rbYYou2/fffv+2ee+6pdKwutSF/fcvRRx/dNmjQoLaqqqq2IUOGtB199NFtzz//fKVjddr/+T//p23UqFFt1dXVbTvttFPb97///UpHWid33313W5K2Z555ptJR1llLS0vbqaee2jZs2LC2TTfdtO2jH/1o27nnntvW2tpa6Wid8pOf/KTtox/9aFtVVVVbXV1d28knn9y2bNmySsdaKx/09+Xq1avbzjvvvLatttqqrbq6um3//fdfr/8b/KDrueGGG9719QsuuKCiud/N+13LO18/827L/fffX+no7+r9rmflypVtRx55ZNvgwYPbqqqq2gYNGtT2N3/zN22PPPJIpWO/p47+rlmpr28ptbW1tXV9vQUAAIB35zOiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQDe18SJE3PEEUdUOgYA3YgiCgAAQKEUUQAgSXLTTTdll112Se/evbPZZpvlgAMOyJlnnpkf/OAH+dnPfpZSqZRSqZTZs2cnSRYvXpzx48dnwIABGThwYA4//PAsXLiwfLx3ZlKnTp2aLbbYIv37989XvvKVvPnmm+97zhUrVhR85QAUrVelAwAAldfU1JRjjz023/72t3PkkUfmtddey4MPPpgvfvGLWbRoUVpaWnLDDTckSQYOHJi33norBx10UMaOHZsHH3wwvXr1ysUXX5yDDz44Tz75ZKqqqpIk9913XzbddNPMnj07CxcuzAknnJDNNtssl1xyyXues62trZJvBQAFUEQBgDQ1NeXtt9/OUUcdlW222SZJsssuuyRJevfundbW1tTV1ZXH//u//3tWr16d6667LqVSKUlyww03ZMCAAZk9e3YOPPDAJElVVVX+7d/+LX369MnIkSNz4YUX5swzz8xFF130vucEoHtzay4AkN122y37779/dtlll3zuc5/Ltddemz/96U/vOX7evHl5/vnn069fv9TU1KSmpiYDBw7MG2+8kRdeeKHdcfv06VNeHzt2bJYvX57Fixd3+JwAdB+KKACQnj175t57782dd96ZnXfeOf/8z/+cHXfcMS+++OK7jl++fHk+9rGPpbGxsd3y7LPP5vOf//yHck4Aug9FFABIkpRKpYwbNy5Tp07Nr371q1RVVeXWW29NVVVVVq1a1W7smDFj8txzz2XLLbfM8OHD2y21tbXlcfPmzcvKlSvL6w899FBqamoydOjQ9z0nAN2bIgoA5OGHH86ll16axx57LIsWLcott9ySP/zhDxkxYkTq6+vz5JNP5plnnsmrr76at956KxMmTMjmm2+eww8/PA8++GBefPHFzJ49O6ecckpefvnl8nHffPPNnHTSSXn66adzxx135IILLsjXvva19OjR433PCUD35mFFAED69++fBx54INOnT09LS0u22WabXHHFFTnkkEOyxx57ZPbs2dljjz2yfPny3H///WloaMgDDzyQs846K0cddVRee+21DBkyJPvvv3/69+9fPu7++++f7bffPp/+9KfT2tqaY489NlOmTPnAcwLQvZXaPCMdAPgQTJw4McuWLcttt91W6SgArGfcmgsAAEChFFEAAAAK5dZcAAAACmVGFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUKj/D/zTxrYXx4uBAAAAAElFTkSuQmCC", "text/plain": [ "
" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "res3 = dtmc_evolution(stormvogel_dtmc, steps=15)\n", "labels = stormvogel_dtmc.get_ordered_labels()\n", "extensions.display_value_iteration_result(res3, 10, labels)" ] }, { "cell_type": "markdown", "id": "cb7c96f9", "metadata": {}, "source": [ "Naive DTMC evolution is also available under stormvogel.extensions.visual_algos." ] }, { "cell_type": "code", "execution_count": 8, "id": "031990dc", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:47:36.715080Z", "iopub.status.busy": "2026-03-26T10:47:36.714911Z", "iopub.status.idle": "2026-03-26T10:47:36.718929Z", "shell.execute_reply": "2026-03-26T10:47:36.718482Z" } }, "outputs": [ { "data": { "text/plain": [ "True" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "res4 = extensions.dtmc_evolution(stormvogel_dtmc, 15)\n", "res3 == res4" ] } ], "metadata": { "kernelspec": { "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.12.13" }, "widgets": { "application/vnd.jupyter.widget-state+json": { "state": { "04a3f1c9ecd746519b9459b3fb7fc4bd": { "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_703223b119224bf78340e7fed843b74b", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "0a41f2231c684c3389561c42540bac49": { "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_ab5150aedb044793aaca6abd695eb3f8", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "299fa1b7da9c4491864fa450519a39f4": { "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_fa2355f0b01943b0b11b3bb43256b0c3", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "703223b119224bf78340e7fed843b74b": { "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 } }, "79d354d147e6414082a770af52edcbdb": { "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 } }, "ab5150aedb044793aaca6abd695eb3f8": { "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 } }, "dec54b3597e943b0948869838676921f": { "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_79d354d147e6414082a770af52edcbdb", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "fa2355f0b01943b0b11b3bb43256b0c3": { "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 }