{ "cells": [ { "cell_type": "markdown", "id": "efd3108f", "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": "e74b5666", "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": "3d577da8", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:00.831996Z", "iopub.status.busy": "2026-03-26T10:42:00.831752Z", "iopub.status.idle": "2026-03-26T10:42:01.061922Z", "shell.execute_reply": "2026-03-26T10:42:01.061404Z" } }, "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", " raise RuntimeError(\"The algorithm will not terminate if epsilon is zero.\")\n", "\n", " # Map state objects to their integer index to avoid slow lookup\n", " state_to_index = {state: i for i, state in enumerate(model.states)}\n", " target_idx = state_to_index[target_state]\n", " values_matrix = [[0 for _ in model.states]]\n", " values_matrix[0][target_idx] = 1\n", "\n", " terminate = False\n", " while not terminate:\n", " old_values = values_matrix[-1]\n", " new_values = [0 for _ in model.states]\n", " for sid, state in enumerate(model.states):\n", " choices = state.choices\n", " # Now we have to take a decision for an action.\n", " action_values = {}\n", " for action, branch in choices:\n", " branch_value = sum(\n", " [prob * old_values[state_to_index[s]] for (prob, s) in branch]\n", " )\n", " action_values[action] = branch_value\n", " # We take the action with the highest value.\n", " highest_value = max(action_values.values()) if action_values else 0\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": "827e8f2b", "metadata": {}, "source": [ "To demonstrate the workings of this algorithm, we use the lion model again." ] }, { "cell_type": "code", "execution_count": 2, "id": "2f310df7", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:01.064033Z", "iopub.status.busy": "2026-03-26T10:42:01.063775Z", "iopub.status.idle": "2026-03-26T10:42:01.284563Z", "shell.execute_reply": "2026-03-26T10:42:01.283969Z" } }, "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" }, { "data": { "text/plain": [ "" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "lion = examples.create_lion_mdp()\n", "show(lion)" ] }, { "cell_type": "markdown", "id": "13b2db60", "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": "729477c1", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:01.291586Z", "iopub.status.busy": "2026-03-26T10:42:01.291247Z", "iopub.status.idle": "2026-03-26T10:42:01.744682Z", "shell.execute_reply": "2026-03-26T10:42:01.744158Z" } }, "outputs": [ { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAA0EAAAFUCAYAAADieTfYAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjgsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvwVt1zgAAAAlwSFlzAAAPYQAAD2EBqD+naQAAJLVJREFUeJzt3Xt0FOXh//HPJmkuhGQhYEgigXATFCEKKRBQFJOCSLlWQUprBPXYNiiYoyJ6EFAxqEdrVQ4qItYLilrAlpZioAa0lWuMolYuihDlJirZJEiCu/P7oz/ybQoSspnlMfu8X+fM0Z2d7HweN3H3szPzrMdxHEcAAAAAYIkI0wEAAAAA4EyiBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqUaYDNEYgENDevXuVkJAgj8djOg4AAAAAQxzHUUVFhdLS0hQRcepjPU26BO3du1fp6emmYwAAAAD4kSgrK1Pbtm1PuU2TLkEJCQmSpFhJ4XgcaI3pACHWvb/pBCE00HSAEOpiOkCIpZoOEEJe0wFCqJnpACH2E9MBQijSdIAQ48ID4IzxVUrpvf+vI5xKky5Bx0+B8yg8S1Bz0wFCLLFJ//bVI9Z0gBAK9zeb8aYDhFA4/08lnJ83iRLUlFGCgDPudC6T4U8TAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqlCAAAAAAVqEEAQAAALAKJQgAAACAVShBAAAAAKxCCQIAAABgFUoQAAAAAKtQggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq/woStC8efOUkZGh2NhY9e3bVxs3bjQdCQAAAECYMl6ClixZooKCAs2cOVMlJSXKzMzUkCFDdPDgQdPRAAAAAIQh4yXokUce0Q033KCJEyfqvPPO05NPPqlmzZrp2WefNR0NAAAAQBgyWoJqamq0ZcsW5ebm1q6LiIhQbm6u3n33XYPJAAAAAISrKJM7P3TokPx+v9q0aVNnfZs2bfTJJ5+csH11dbWqq6trb/t8vpBnBAAAABBejJ8O1xCFhYXyer21S3p6uulIAAAAAJoYoyWodevWioyM1IEDB+qsP3DggFJSUk7Yfvr06SovL69dysrKzlRUAAAAAGHCaAmKjo5W7969tWbNmtp1gUBAa9asUXZ29gnbx8TEKDExsc4CAAAAAA1h9JogSSooKFBeXp6ysrLUp08fPfroo6qqqtLEiRNNRwMAAAAQhoyXoHHjxumrr77S3Xffrf379+uCCy7Q3//+9xMmSwAAAAAAN3gcx3FMhwiWz+eT1+tVnCSP6TAhsN50gBDrMdB0ghC6zHSAEOpqOkCIpZkOEEItTAcIoXjTAULsJ6YDhFCk6QAh1qSmoAKaNl+F5O0qlZeX13vZDH+aAAAAAKxCCQIAAABgFUoQAAAAAKtQggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq1CCAAAAAFiFEgQAAADAKpQgAAAAAFahBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqUaYDuGF/ebkSExNNxwiBhaYDhNg/TQcIoW2mA4TQftMBQuyQ6QAhdNR0gNBxakwnCC2/6QAhFDAdIMTC+bkL57GFu3D9u2vA7yRHggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq1CCAAAAAFiFEgQAAADAKpQgAAAAAFahBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqlCAAAAAAVqEEAQAAALAKJQgAAACAVShBAAAAAKxCCQIAAABgFaMlaN26dRo+fLjS0tLk8Xi0fPlyk3EAAAAAWMBoCaqqqlJmZqbmzZtnMgYAAAAAi0SZ3PnQoUM1dOhQkxEAAAAAWMZoCWqo6upqVVdX1972+XwG0wAAAABoiprUxAiFhYXyer21S3p6uulIAAAAAJqYJlWCpk+frvLy8tqlrKzMdCQAAAAATUyTOh0uJiZGMTExpmMAAAAAaMKa1JEgAAAAAGgso0eCKisrtXPnztrbu3btUmlpqZKSktSuXTuDyQAAAACEK6MlaPPmzRo0aFDt7YKCAklSXl6ennvuOUOpAAAAAIQzoyXo0ksvleM4JiMAAAAAsAzXBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqlCAAAAAAVqEEAQAAALAKJQgAAACAVShBAAAAAKxCCQIAAABgFUoQAAAAAKtQggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq0SZDuCGFK9XHtMhQuB+0wFCbEo4V/DRpgOEUC/TAUIsw3SAEEoyHSCEEkwHCLFY0wFCKNJ0gBAL59e6cH/u0PRUnv6m4fynCQAAAAAnoAQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq1CCAAAAAFiFEgQAAADAKkGVoJKSEm3durX29htvvKFRo0bpzjvvVE1NjWvhAAAAAMBtQZWgG2+8Udu3b5ckffbZZ7r66qvVrFkzvfbaa7r99ttdDQgAAAAAbgqqBG3fvl0XXHCBJOm1117TwIEDtXjxYj333HP605/+5GY+AAAAAHBVUCXIcRwFAgFJ0urVq3XFFVdIktLT03Xo0CH30gEAAACAy4IqQVlZWbrvvvv0wgsvaO3atRo2bJgkadeuXWrTpo2rAQEAAADATUGVoEcffVQlJSWaPHmy7rrrLnXu3FmS9Prrr6t///6uBgQAAAAAN0UF80M9e/asMzvccQ899JAiIyMbHQoAAAAAQiXo7wk6fPiwnnnmGU2fPl3ffPONJOnjjz/WwYMHXQsHAAAAAG4L6kjQBx98oJycHLVo0UKff/65brjhBiUlJWnp0qXas2ePnn/+ebdzAgAAAIArgjoSVFBQoIkTJ2rHjh2KjY2tXX/FFVdo3bp1roUDAAAAALcFVYI2bdqkG2+88YT1Z599tvbv39/oUAAAAAAQKkGVoJiYGPl8vhPWb9++XWeddVajQwEAAABAqARVgkaMGKF77rlHx44dkyR5PB7t2bNH06ZN0y9+8QtXAwIAAACAm4IqQQ8//LAqKyuVnJys7777Tpdccok6d+6shIQEzZkzx+2MAAAAAOCaoGaH83q9Kioq0j//+U+9//77qqysVK9evZSbm9ugxyksLNTSpUv1ySefKC4uTv3799cDDzygrl27BhMLAAAAAOoV1JGg559/XtXV1RowYIB+97vf6fbbb1dubq5qamoaND322rVrlZ+fr/Xr16uoqEjHjh3T4MGDVVVVFUwsAAAAAKiXx3Ecp6E/FBkZqX379ik5ObnO+q+//lrJycny+/1Bhfnqq6+UnJystWvXauDAgfVu7/P55PV6FSfJE9Qef9zuNx0gxKYE/VW9TcBo0wFCqJfpACGWYTpACCWZDhBCCaYDhFhs/Zs0WZGmA4RYOL/WhftzhybHVyl5+0nl5eVKTEw85bZBnQ7nOI48nhNrxxdffCGv1xvMQ0r6T2BJSko6+St1dXW1qqura2+fbIY6AAAAADiVBpWgCy+8UB6PRx6PRzk5OYqK+r8f9/v92rVrly6//PKgggQCAU2dOlUDBgzQ+eeff9JtCgsLNXv27KAeHwAAAACkBpagUaNGSZJKS0s1ZMgQNW/evPa+6OhoZWRkBD1Fdn5+vj788EO98847P7jN9OnTVVBQUHvb5/MpPT09qP0BAAAAsFODStDMmTMlSRkZGRo3bpxiY905SXny5MlasWKF1q1bp7Zt2/7gdjExMYqJiXFlnwAAAADsFNQ1QXl5ea7s3HEc3XTTTVq2bJmKi4vVoUMHVx4XAAAAAH5IUCXI7/fr97//vV599VXt2bNHNTU1de7/5ptvTutx8vPztXjxYr3xxhtKSEjQ/v37Jf3ne4ji4uKCiQYAAAAApxTUxI2zZ8/WI488onHjxqm8vFwFBQUaM2aMIiIiNGvWrNN+nPnz56u8vFyXXnqpUlNTa5clS5YEEwsAAAAA6hXUkaCXXnpJCxYs0LBhwzRr1iyNHz9enTp1Us+ePbV+/XrdfPPNp/U4QXxFEQAAAAA0SlBHgvbv368ePXpIkpo3b177/T4///nP9de//tW9dAAAAADgsqBKUNu2bbVv3z5JUqdOnfTmm29KkjZt2sTsbQAAAAB+1IIqQaNHj9aaNWskSTfddJNmzJihLl266JprrtGkSZNcDQgAAAAAbgrqmqC5c+fW/vu4cePUvn17/etf/1KXLl00fPhw18IBAAAAgNuCKkHr1q1T//79FRX1nx/v16+f+vXrp++//17r1q3TwIEDXQ0JAAAAAG4J6nS4QYMGnfS7gMrLyzVo0KBGhwIAAACAUAmqBDmOI4/Hc8L6r7/+WvHx8Y0OBQAAAACh0qDT4caMGSNJ8ng8uvbaa+vMBOf3+/XBBx+of//+7iYEAAAAABc1qAR5vV5J/zkSlJCQoLi4uNr7oqOj1a9fP91www3uJgQAAAAAFzWoBC1atEiSdNZZZ2nWrFlq1qyZJOnzzz/X8uXLde6556p169bupwQAAAAAlwR1TdB7772n559/XpJ0+PBh9evXTw8//LBGjRql+fPnuxoQAAAAANwUdAm6+OKLJUmvv/662rRpo927d+v555/XY4895mpAAAAAAHBTUCXoyJEjSkhIkCS9+eabGjNmjCIiItSvXz/t3r3b1YAAAAAA4KagSlDnzp21fPlylZWVadWqVRo8eLAk6eDBg0pMTHQ1IAAAAAC4KagSdPfdd+vWW29VRkaG+vbtq+zsbEn/OSp04YUXuhoQAAAAANzUoNnhjrvyyit10UUXad++fcrMzKxdn5OTo9GjR7sWDgAAAADcFlQJkqSUlBSlpKTUWdenT59GBwIAAACAUArqdDgAAAAAaKooQQAAAACsQgkCAAAAYBVKEAAAAACrBD0xAkJvtekAIZYVMJ0gdAaE85N3wHSAEEs3HSCEkkwHCKFmpgOEWKzpACEUaTpAiIXz+PgoHT82R09/U359AQAAAFiFEgQAAADAKpQgAAAAAFahBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqlCAAAAAAVqEEAQAAALAKJQgAAACAVShBAAAAAKxCCQIAAABgFUoQAAAAAKtQggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArGK0BM2fP189e/ZUYmKiEhMTlZ2drZUrV5qMBAAAACDMGS1Bbdu21dy5c7VlyxZt3rxZl112mUaOHKmPPvrIZCwAAAAAYSzK5M6HDx9e5/acOXM0f/58rV+/Xt27dzeUCgAAAEA4M1qC/pvf79drr72mqqoqZWdnm44DAAAAIEwZL0Fbt25Vdna2jh49qubNm2vZsmU677zzTrptdXW1qqura2/7fL4zFRMAAABAmDA+O1zXrl1VWlqqDRs26Le//a3y8vL08ccfn3TbwsJCeb3e2iU9Pf0MpwUAAADQ1Hkcx3FMh/hvubm56tSpk5566qkT7jvZkaD09HTFSfKcwYxnymWmA4TYHaYDhNAAr+kEIdTDdIAQC+fPVpJMBwihZqYDhFis6QAhFGk6QIiF8/iMf5QO1OU7KnnvlcrLy5WYmHjKbY2fDve/AoFAnaLz32JiYhQTE3OGEwEAAAAIJ0ZL0PTp0zV06FC1a9dOFRUVWrx4sYqLi7Vq1SqTsQAAAACEMaMl6ODBg7rmmmu0b98+eb1e9ezZU6tWrdLPfvYzk7EAAAAAhDGjJWjhwoUmdw8AAADAQlzSBgAAAMAqlCAAAAAAVqEEAQAAALAKJQgAAACAVShBAAAAAKxCCQIAAABgFUoQAAAAAKtQggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq1CCAAAAAFiFEgQAAADAKpQgAAAAAFahBAEAAACwCiUIAAAAgFUoQQAAAACs4nEcxzEdIlg+n09er1dxkjymwwAAAAAwxpH0naTy8nIlJiaecluOBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqlCAAAAAAVqEEAQAAALAKJQgAAACAVShBAAAAAKxCCQIAAABgFUoQAAAAAKtQggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq1CCAAAAAFiFEgQAAADAKj+aEjR37lx5PB5NnTrVdBQAAAAAYexHUYI2bdqkp556Sj179jQdBQAAAECYM16CKisrNWHCBC1YsEAtW7Y0HQcAAABAmDNegvLz8zVs2DDl5ubWu211dbV8Pl+dBQAAAAAaIsrkzl955RWVlJRo06ZNp7V9YWGhZs+eHeJUAAAAAMKZsSNBZWVlmjJlil566SXFxsae1s9Mnz5d5eXltUtZWVmIUwIAAAAINx7HcRwTO16+fLlGjx6tyMjI2nV+v18ej0cRERGqrq6uc9/J+Hw+eb1exUnyhDgvAAAAgB8vR9J3ksrLy5WYmHjKbY2dDpeTk6OtW7fWWTdx4kR169ZN06ZNq7cAAQAAAEAwjJWghIQEnX/++XXWxcfHq1WrViesBwAAAAC3GJ8dDgAAAADOJKOzw/2v4uJi0xEAAAAAhDmOBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqlCAAAAAAVqEEAQAAALAKJQgAAACAVShBAAAAAKxCCQIAAABgFUoQAAAAAKtQggAAAABYhRIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGCVKNMBGsNxnP/803AOAAAAAGYd7wTHO8KpNOkSVFFRIUk6ajgHAAAAgB+HiooKeb3eU27jcU6nKv1IBQIB7d27VwkJCfJ4PCHfn8/nU3p6usrKypSYmBjy/Z1J4Tw2KbzHx9iarnAeH2NrusJ5fIyt6Qrn8TE29ziOo4qKCqWlpSki4tRX/TTpI0ERERFq27btGd9vYmJi2P2SHhfOY5PCe3yMrekK5/ExtqYrnMfH2JqucB4fY3NHfUeAjmNiBAAAAABWoQQBAAAAsAolqAFiYmI0c+ZMxcTEmI7iunAemxTe42NsTVc4j4+xNV3hPD7G1nSF8/gYmxlNemIEAAAAAGgojgQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVStBpmjdvnjIyMhQbG6u+fftq48aNpiO5Yt26dRo+fLjS0tLk8Xi0fPly05FcU1hYqJ/+9KdKSEhQcnKyRo0apW3btpmO5Zr58+erZ8+etV9Alp2drZUrV5qOFRJz586Vx+PR1KlTTUdptFmzZsnj8dRZunXrZjqWq7788kv96le/UqtWrRQXF6cePXpo8+bNpmM1WkZGxgnPncfjUX5+vulojeb3+zVjxgx16NBBcXFx6tSpk+69916Fy9xJFRUVmjp1qtq3b6+4uDj1799fmzZtMh0rKPW9bjuOo7vvvlupqamKi4tTbm6uduzYYSZsA9U3tqVLl2rw4MFq1aqVPB6PSktLjeQM1qnGd+zYMU2bNk09evRQfHy80tLSdM0112jv3r3mAjdAfc/drFmz1K1bN8XHx6tly5bKzc3Vhg0bzIT9/yhBp2HJkiUqKCjQzJkzVVJSoszMTA0ZMkQHDx40Ha3RqqqqlJmZqXnz5pmO4rq1a9cqPz9f69evV1FRkY4dO6bBgwerqqrKdDRXtG3bVnPnztWWLVu0efNmXXbZZRo5cqQ++ugj09FctWnTJj311FPq2bOn6Siu6d69u/bt21e7vPPOO6Yjuebbb7/VgAED9JOf/EQrV67Uxx9/rIcfflgtW7Y0Ha3RNm3aVOd5KyoqkiRdddVVhpM13gMPPKD58+friSee0L///W898MADevDBB/X444+bjuaK66+/XkVFRXrhhRe0detWDR48WLm5ufryyy9NR2uw+l63H3zwQT322GN68skntWHDBsXHx2vIkCE6evToGU7acPWNraqqShdddJEeeOCBM5zMHaca35EjR1RSUqIZM2aopKRES5cu1bZt2zRixAgDSRuuvufunHPO0RNPPKGtW7fqnXfeUUZGhgYPHqyvvvrqDCf9Lw7q1adPHyc/P7/2tt/vd9LS0pzCwkKDqdwnyVm2bJnpGCFz8OBBR5Kzdu1a01FCpmXLls4zzzxjOoZrKioqnC5dujhFRUXOJZdc4kyZMsV0pEabOXOmk5mZaTpGyEybNs256KKLTMc4I6ZMmeJ06tTJCQQCpqM02rBhw5xJkybVWTdmzBhnwoQJhhK558iRI05kZKSzYsWKOut79erl3HXXXYZSueN/X7cDgYCTkpLiPPTQQ7XrDh8+7MTExDgvv/yygYTBO9V7kl27djmSnPfee++MZnLT6bzn2rhxoyPJ2b1795kJ5ZLTGVt5ebkjyVm9evWZCXUSHAmqR01NjbZs2aLc3NzadREREcrNzdW7775rMBkaqry8XJKUlJRkOIn7/H6/XnnlFVVVVSk7O9t0HNfk5+dr2LBhdf7+wsGOHTuUlpamjh07asKECdqzZ4/pSK7585//rKysLF111VVKTk7WhRdeqAULFpiO5bqamhq9+OKLmjRpkjwej+k4jda/f3+tWbNG27dvlyS9//77eueddzR06FDDyRrv+++/l9/vV2xsbJ31cXFxYXUUVpJ27dql/fv31/l/ptfrVd++fXnP0gSVl5fL4/GoRYsWpqO4qqamRk8//bS8Xq8yMzON5Ygytucm4tChQ/L7/WrTpk2d9W3atNEnn3xiKBUaKhAIaOrUqRowYIDOP/9803Fcs3XrVmVnZ+vo0aNq3ry5li1bpvPOO890LFe88sorKikpabLn7f+Qvn376rnnnlPXrl21b98+zZ49WxdffLE+/PBDJSQkmI7XaJ999pnmz5+vgoIC3Xnnndq0aZNuvvlmRUdHKy8vz3Q81yxfvlyHDx/WtddeazqKK+644w75fD5169ZNkZGR8vv9mjNnjiZMmGA6WqMlJCQoOztb9957r84991y1adNGL7/8st5991117tzZdDxX7d+/X5JO+p7l+H1oGo4ePapp06Zp/PjxSkxMNB3HFStWrNDVV1+tI0eOKDU1VUVFRWrdurWxPJQgWCE/P18ffvhh2H3q17VrV5WWlqq8vFyvv/668vLytHbt2iZfhMrKyjRlyhQVFRWd8OltU/ffn6z37NlTffv2Vfv27fXqq6/quuuuM5jMHYFAQFlZWbr//vslSRdeeKE+/PBDPfnkk2FVghYuXKihQ4cqLS3NdBRXvPrqq3rppZe0ePFide/eXaWlpZo6darS0tLC4nl74YUXNGnSJJ199tmKjIxUr169NH78eG3ZssV0NOAEx44d09ixY+U4jubPn286jmsGDRqk0tJSHTp0SAsWLNDYsWO1YcMGJScnG8nD6XD1aN26tSIjI3XgwIE66w8cOKCUlBRDqdAQkydP1ooVK/TWW2+pbdu2puO4Kjo6Wp07d1bv3r1VWFiozMxM/eEPfzAdq9G2bNmigwcPqlevXoqKilJUVJTWrl2rxx57TFFRUfL7/aYjuqZFixY655xztHPnTtNRXJGamnpCCT/33HPD6pS/3bt3a/Xq1br++utNR3HNbbfdpjvuuENXX321evTooV//+te65ZZbVFhYaDqaKzp16qS1a9eqsrJSZWVl2rhxo44dO6aOHTuajuaq4+9LeM/SdB0vQLt371ZRUVHYHAWSpPj4eHXu3Fn9+vXTwoULFRUVpYULFxrLQwmqR3R0tHr37q01a9bUrgsEAlqzZk1YXXsRjhzH0eTJk7Vs2TL94x//UIcOHUxHCrlAIKDq6mrTMRotJydHW7duVWlpae2SlZWlCRMmqLS0VJGRkaYjuqayslKffvqpUlNTTUdxxYABA06Yin779u1q3769oUTuW7RokZKTkzVs2DDTUVxz5MgRRUTUfUsQGRmpQCBgKFFoxMfHKzU1Vd9++61WrVqlkSNHmo7kqg4dOiglJaXOexafz6cNGzbwnqUJOF6AduzYodWrV6tVq1amI4WU6fcsnA53GgoKCpSXl6esrCz16dNHjz76qKqqqjRx4kTT0RqtsrKyzifQu3btUmlpqZKSktSuXTuDyRovPz9fixcv1htvvKGEhITa86G9Xq/i4uIMp2u86dOna+jQoWrXrp0qKiq0ePFiFRcXa9WqVaajNVpCQsIJ127Fx8erVatWTf6arltvvVXDhw9X+/bttXfvXs2cOVORkZEaP3686WiuuOWWW9S/f3/df//9Gjt2rDZu3Kinn35aTz/9tOlorggEAlq0aJHy8vIUFRU+L6HDhw/XnDlz1K5dO3Xv3l3vvfeeHnnkEU2aNMl0NFesWrVKjuOoa9eu2rlzp2677TZ169atSb6O1/e6PXXqVN13333q0qWLOnTooBkzZigtLU2jRo0yF/o01Te2b775Rnv27Kn97pzjH7ikpKQ0iSNdpxpfamqqrrzySpWUlGjFihXy+/2171uSkpIUHR1tKvZpOdXYWrVqpTlz5mjEiBFKTU3VoUOHNG/ePH355Zdmv2LA2Lx0Tczjjz/utGvXzomOjnb69OnjrF+/3nQkV7z11luOpBOWvLw809Ea7WTjkuQsWrTIdDRXTJo0yWnfvr0THR3tnHXWWU5OTo7z5ptvmo4VMuEyRfa4ceOc1NRUJzo62jn77LOdcePGOTt37jQdy1V/+ctfnPPPP9+JiYlxunXr5jz99NOmI7lm1apVjiRn27ZtpqO4yufzOVOmTHHatWvnxMbGOh07dnTuuusup7q62nQ0VyxZssTp2LGjEx0d7aSkpDj5+fnO4cOHTccKSn2v24FAwJkxY4bTpk0bJyYmxsnJyWkyv6/1jW3RokUnvX/mzJlGc5+uU43v+LTfJ1veeust09Hrdaqxfffdd87o0aOdtLQ0Jzo62klNTXVGjBjhbNy40Whmj+OEyddBAwAAAMBp4JogAAAAAFahBAEAAACwCiUIAAAAgFUoQQAAAACsQgkCAAAAYBVKEAAAAACrUIIAAAAAWIUSBAAAAMAqlCAAwI/Wtddeq1GjRpmOAQAIM5QgAAAAAFahBAEAjHv99dfVo0cPxcXFqVWrVsrNzdVtt92mP/7xj3rjjTfk8Xjk8XhUXFwsSSorK9PYsWPVokULJSUlaeTIkfr8889rH+/4EaTZs2frrLPOUmJion7zm9+opqbmlPusqqo6wyMHAJgQZToAAMBu+/bt0/jx4/Xggw9q9OjRqqio0Ntvv61rrrlGe/bskc/n06JFiyRJSUlJOnbsmIYMGaLs7Gy9/fbbioqK0n333afLL79cH3zwgaKjoyVJa9asUWxsrIqLi/X5559r4sSJatWqlebMmfOD+3Qcx+R/CgDAGUIJAgAYtW/fPn3//fcaM2aM2rdvL0nq0aOHJCkuLk7V1dVKSUmp3f7FF19UIBDQM888I4/HI0latGiRWrRooeLiYg0ePFiSFB0drWeffVbNmjVT9+7ddc899+i2227Tvffee8p9AgDCH6fDAQCMyszMVE5Ojnr06KGrrrpKCxYs0LfffvuD27///vvauXOnEhIS1Lx5czVv3lxJSUk6evSoPv300zqP26xZs9rb2dnZqqysVFlZWYP3CQAIL5QgAIBRkZGRKioq0sqVK3Xeeefp8ccfV9euXbVr166Tbl9ZWanevXurtLS0zrJ9+3b98pe/DMk+AQDhhRIEADDO4/FowIABmj17tt577z1FR0dr2bJlio6Olt/vr7Ntr169tGPHDiUnJ6tz5851Fq/XW7vd+++/r++++6729vr169W8eXOlp6efcp8AgPBHCQIAGLVhwwbdf//92rx5s/bs2aOlS5fqq6++0rnnnquMjAx98MEH2rZtmw4dOqRjx45pwoQJat26tUaOHKm3335bu3btUnFxsW6++WZ98cUXtY9bU1Oj6667Th9//LH+9re/aebMmZo8ebIiIiJOuU8AQPhjYgQAgFGJiYlat26dHn30Ufl8PrVv314PP/ywhg4dqqysLBUXFysrK0uVlZV66623dOmll2rdunWaNm2axowZo4qKCp199tnKyclRYmJi7ePm5OSoS5cuGjhwoKqrqzV+/HjNmjWr3n0CAMKfx2E+UABAmLn22mt1+PBhLV++3HQUAMCPEKfDAQAAALAKJQgAAACAVTgdDgAAAIBVOBIEAAAAwCqUIAAAAABWoQQBAAAAsAolCAAAAIBVKEEAAAAArEIJAgAAAGAVShAAAAAAq1CCAAAAAFiFEgQAAADAKv8P+XyojyDOaJQAAAAASUVORK5CYII=", "text/plain": [ "
" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "target = next(iter(lion.get_states_with_label(\"full\")))\n", "res = naive_value_iteration(lion, 0.003, target)\n", "labels = [str(i) for i in range(len(lion.states))]\n", "extensions.display_value_iteration_result(res, 10, labels)" ] }, { "cell_type": "markdown", "id": "ee19ea16", "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": "93b9cfe4", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:01.746699Z", "iopub.status.busy": "2026-03-26T10:42:01.746393Z", "iopub.status.idle": "2026-03-26T10:42:01.750443Z", "shell.execute_reply": "2026-03-26T10:42:01.749973Z" }, "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, next(iter(lion.get_states_with_label(\"full\")))\n", ")\n", "res == res2" ] }, { "cell_type": "markdown", "id": "f6e0cb72", "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": "5fbe3206", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:01.752084Z", "iopub.status.busy": "2026-03-26T10:42:01.751903Z", "iopub.status.idle": "2026-03-26T10:42:01.756540Z", "shell.execute_reply": "2026-03-26T10:42:01.756033Z" } }, "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", " raise RuntimeError(\"Need at least two steps\")\n", " if model.model_type != stormvogel.model.ModelType.DTMC:\n", " raise 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_state_index(model.initial_state)] = 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 enumerate(model.states):\n", " branches = s.get_branches()\n", " for transition_prob, target in branches:\n", " current_prob = matrix_steps_states[current_step][s_id]\n", " matrix_steps_states[next_step][model.get_state_index(target)] += (\n", " current_prob * float(transition_prob)\n", " )\n", "\n", " return matrix_steps_states" ] }, { "cell_type": "code", "execution_count": 6, "id": "2f675e33", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:01.758084Z", "iopub.status.busy": "2026-03-26T10:42:01.757904Z", "iopub.status.idle": "2026-03-26T10:42:01.788948Z", "shell.execute_reply": "2026-03-26T10:42:01.788335Z" } }, "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" }, { "data": { "text/plain": [ "" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "stormvogel_dtmc = mapping.stormpy_to_stormvogel(examples.example_building_dtmcs_01())\n", "show(stormvogel_dtmc)" ] }, { "cell_type": "code", "execution_count": 7, "id": "01183924", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:01.796142Z", "iopub.status.busy": "2026-03-26T10:42:01.795895Z", "iopub.status.idle": "2026-03-26T10:42:01.938094Z", "shell.execute_reply": "2026-03-26T10:42:01.937455Z" } }, "outputs": [ { "data": { "image/png": "iVBORw0KGgoAAAANSUhEUgAAA0oAAALeCAYAAACUWuEMAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjgsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvwVt1zgAAAAlwSFlzAAAPYQAAD2EBqD+naQAAOh5JREFUeJzt3Xuc1PV97/HPAO6y4u4oyG11uXiJKEGKEhW0iRaKpRy81RuHE1GTnORRrBIaS0iKl6pZtY9Ea+IDo0mxmhhjrGLqOYYgFdDGC4J4qa1CgkAUJCayC6suZHfOH3m4J3zlIsuwv9nh+Xw85tHO7Ozu+xdN2Be/38zmCoVCIQAAAGjTJesBAAAApUYoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQKJb1gP2ttbW1njrrbeiuro6crlc1nMAAICMFAqF2LRpU9TW1kaXLjs/Z1T2ofTWW29FXV1d1jMAAIASsXbt2jj00EN3+pyyD6Xq6uqI+MN/GDU1NRmvKY5++XzWEwAAoNMpRMQH8f8bYWfKPpQ+vNyupqambELJBYQAANB+H+clOd7MAQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAINEpQun222+PQYMGRffu3ePEE0+M5557LutJAABAGSv5UPrxj38c06dPj6uvvjqWLVsWw4cPj9NPPz02bNiQ9TQAAKBMlXwofetb34ovfOELcckll8QxxxwTd9xxR+y///7xz//8z1lPAwAAylRJh9KWLVti6dKlMXbs2LbHunTpEmPHjo2nn356u5/T3NwcjY2N29wAAAB2R0mH0jvvvBMtLS3Rt2/fbR7v27dvrF+/frufU19fH/l8vu1WV1fXEVMBAIAyUtKh1B4zZ86MhoaGttvatWuzngQAAHQy3bIesDMHH3xwdO3aNd5+++1tHn/77bejX79+2/2cysrKqKys7Ih5AABAmSrpM0oVFRVx/PHHx4IFC9oea21tjQULFsSoUaMyXAYAAJSzkj6jFBExffr0mDJlSowcOTJOOOGEuPXWW6OpqSkuueSSrKcBAABlquRD6YILLojf/OY3cdVVV8X69evjT/7kT+JnP/vZR97gAQAAoFhyhUKhkPWIvamxsTHy+Xw0NDRETU1N1nOKokcul/UEAADodAoR8X7Ex2qDkn6NEgAAQBaEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACS6ZT2go/TL5yOX9YgiaZqc9YLi6fHDrBcU17lZDyiyB7MeUES9sx5QZL/JekCR7Zf1gCLamvUAAIrCGSUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgETJh9LixYtj4sSJUVtbG7lcLubOnZv1JAAAoMyVfCg1NTXF8OHD4/bbb896CgAAsI/olvWAXRk/fnyMHz8+6xkAAMA+pORDaXc1NzdHc3Nz2/3GxsYM1wAAAJ1RyV96t7vq6+sjn8+33erq6rKeBAAAdDJlF0ozZ86MhoaGttvatWuzngQAAHQyZXfpXWVlZVRWVmY9AwAA6MTK7owSAADAnir5M0qbN2+OlStXtt1ftWpVLF++PHr27BkDBgzIcBkAAFCuSj6Unn/++TjttNPa7k+fPj0iIqZMmRJ33313RqsAAIByVvKhdOqpp0ahUMh6BgAAsA/xGiUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACARMmHUn19fXzqU5+K6urq6NOnT5x11lnx2muvZT0LAAAoYyUfSosWLYqpU6fGM888E/Pnz4+tW7fGuHHjoqmpKetpAABAmeqW9YBd+dnPfrbN/bvvvjv69OkTS5cujU9/+tMfeX5zc3M0Nze33W9sbNzrGwEAgPJS8meUUg0NDRER0bNnz+1+vL6+PvL5fNutrq6uI+cBAABlIFcoFApZj/i4Wltb44wzzoiNGzfGU089td3nbO+MUl1dXVRFRK6Ddu5tTZOzXlA8PX6Y9YLiOjfrAUX2YNYDiqh31gOK7DdZDyiy/bIeUERbsx4AwA4VIuL9+MPJl5qamp0+t+QvvftjU6dOjVdeeWWHkRQRUVlZGZWVlR24CgAAKDedJpQuu+yyePTRR2Px4sVx6KGHZj0HAAAoYyUfSoVCIf7mb/4mHn744Vi4cGEMHjw460kAAECZK/lQmjp1atx3333xyCOPRHV1daxfvz4iIvL5fFRVVWW8DgAAKEcl/653s2fPjoaGhjj11FOjf//+bbcf//jHWU8DAADKVMmfUepEb8oHAACUiZI/owQAANDRhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAolvWA9h9PX6Y9YLiuT/rAUV2YdYDiuyYrAcU0atZDyiyHlkPKLKmrAcUUdesBxRZS9YDADLijBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQKLkQ2n27Nlx7LHHRk1NTdTU1MSoUaPisccey3oWAABQxko+lA499NC48cYbY+nSpfH888/Hn/3Zn8WZZ54Z//mf/5n1NAAAoEzlCoVCIesRu6tnz57xj//4j/G5z31ul89tbGyMfD4fVRGR2/vT2E33Zz2gyC7MekCRHZP1gCJ6NesBRdYj6wFF1pT1gCLqmvWAImvJegBAERUi4v2IaGhoiJqamp0+t1uHLCqSlpaW+MlPfhJNTU0xatSo7T6nubk5mpub2+43NjZ21DwAAKBMlPyldxERL7/8chxwwAFRWVkZX/rSl+Lhhx+OY47Z/t9119fXRz6fb7vV1dV18FoAAKCz6xSX3m3ZsiXWrFkTDQ0N8eCDD8b3vve9WLRo0XZjaXtnlOrq6lx6V6JcelfaXHpXulx6V7pcegdQunbn0rtOEUqpsWPHxuGHHx7f/e53d/lcr1EqbUKptAml0iWUSpdQAihduxNKneLSu1Rra+s2Z40AAACKqeTfzGHmzJkxfvz4GDBgQGzatCnuu+++WLhwYcybNy/raQAAQJkq+VDasGFDXHTRRbFu3brI5/Nx7LHHxrx58+LP//zPs54GAACUqZIPpe9///tZTwAAAPYxnfI1SgAAAHuTUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACARKcKpRtvvDFyuVxMmzYt6ykAAEAZ6zShtGTJkvjud78bxx57bNZTAACAMtcpQmnz5s0xefLkuOuuu+Kggw7Keg4AAFDmOkUoTZ06NSZMmBBjx47d5XObm5ujsbFxmxsAAMDu6Jb1gF25//77Y9myZbFkyZKP9fz6+vq49tpr9/IqAACgnJX0GaW1a9fGFVdcET/84Q+je/fuH+tzZs6cGQ0NDW23tWvX7uWVAABAuSnpM0pLly6NDRs2xHHHHdf2WEtLSyxevDi+853vRHNzc3Tt2nWbz6msrIzKysqOngoAAJSRkg6lMWPGxMsvv7zNY5dcckkMGTIkZsyY8ZFIAgAAKIaSDqXq6ur45Cc/uc1jPXr0iF69en3kcQAAgGIp6dcoAQAAZKGkzyhtz8KFC7OeAAAAlDlnlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASJR9K11xzTeRyuW1uQ4YMyXoWAABQxrplPeDjGDp0aDz++ONt97t16xSzAQCATqpTFEe3bt2iX79+H+u5zc3N0dzc3Ha/sbFxb80CAADKVMlfehcRsWLFiqitrY3DDjssJk+eHGvWrNnhc+vr6yOfz7fd6urqOnApAABQDnKFQqGQ9Yideeyxx2Lz5s1x1FFHxbp16+Laa6+NN998M1555ZWorq7+yPO3d0aprq4uqiIi14G7+Xjuz3pAkV2Y9YAiOybrAUX0atYDiqxH1gOKrCnrAUXUNesBRdaS9QCAIipExPsR0dDQEDU1NTt9bslfejd+/Pi2///YY4+NE088MQYOHBgPPPBAfO5zn/vI8ysrK6OysrIjJwIAAGWmU1x698cOPPDA+MQnPhErV67MegoAAFCmOl0obd68OX75y19G//79s54CAACUqZIPpa985SuxaNGieOONN+IXv/hFnH322dG1a9eYNGlS1tMAAIAyVfKvUfr1r38dkyZNit/+9rfRu3fvOOWUU+KZZ56J3r17Zz0NAAAoUyUfSvffX27viwYAAJS6kr/0DgAAoKMJJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgES7QmnZsmXx8ssvt91/5JFH4qyzzoqvfe1rsWXLlqKNAwAAyEK7QumLX/xivP766xER8atf/SouvPDC2H///eMnP/lJ/N3f/V1RBwIAAHS0doXS66+/Hn/yJ38SERE/+clP4tOf/nTcd999cffdd8e//uu/FnMfAABAh2tXKBUKhWhtbY2IiMcffzz+8i//MiIi6urq4p133ineOgAAgAy0K5RGjhwZ119/fdx7772xaNGimDBhQkRErFq1Kvr27VvUgQAAAB2tXaF06623xrJly+Kyyy6Lr3/963HEEUdERMSDDz4Yo0ePLupAAACAjpYrFAqFYn2xDz74ILp27Rr77bdfsb7kHmtsbIx8Ph9VEZHLegwfcX/WA4rswqwHFNkxWQ8oolezHlBkPbIeUGRNWQ8ooq5ZDyiylqwHABRRISLej4iGhoaoqanZ6XPb/XuUNm7cGN/73vdi5syZ8bvf/S4iIl599dXYsGFDe78kAABASejWnk966aWXYsyYMXHggQfGG2+8EV/4wheiZ8+e8dBDD8WaNWvinnvuKfZOAACADtOuM0rTp0+PSy65JFasWBHdu3dve/wv//IvY/HixUUbBwAAkIV2hdKSJUvii1/84kceP+SQQ2L9+vV7PAoAACBL7QqlysrKaGxs/Mjjr7/+evTu3XuPRwEAAGSpXaF0xhlnxD/8wz/E1q1bIyIil8vFmjVrYsaMGfFXf/VXRR0IAADQ0doVSt/85jdj8+bN0adPn3j//ffjM5/5TBxxxBFRXV0dN9xwQ7E3AgAAdKh2vetdPp+P+fPnx3/8x3/Eiy++GJs3b47jjjsuxo4dW+x98eabb8aMGTPisccei/feey+OOOKImDNnTowcObLo3wsAACCinaF0zz33xAUXXBAnn3xynHzyyW2Pb9myJe6///646KKLijLu3XffjZNPPjlOO+20eOyxx6J3796xYsWKOOigg4ry9QEAALYnVygUCrv7SV27do1169ZFnz59tnn8t7/9bfTp0ydaWorze7y/+tWvxn/8x3/Ek08+2e6v0djYGPl8PqoiIleUVRTT/VkPKLILsx5QZMdkPaCIXs16QJH1yHpAkTVlPaCIumY9oMiK8yc6QGkoRMT7EdHQ0BA1NTU7fW67XqNUKBQil/todvz617+OfD7fni+5XT/96U9j5MiRcd5550WfPn1ixIgRcdddd+30c5qbm6OxsXGbGwAAwO7YrUvvRowYEblcLnK5XIwZMya6dfv/n97S0hKrVq2Kv/iLvyjauF/96lcxe/bsmD59enzta1+LJUuWxOWXXx4VFRUxZcqU7X5OfX19XHvttUXbAAAA7Ht269K7DwPk2muvjb/927+NAw44oO1jFRUVMWjQoPirv/qrqKioKMq4ioqKGDlyZPziF79oe+zyyy+PJUuWxNNPP73dz2lubo7m5ua2+42NjVFXV+fSuxLl0rvS5tK70uXSu9Ll0juA0rU7l97t1hmlq6++OiIiBg0aFBdccEF07969vRs/lv79+8cxx2z7o9rRRx8d//qv/7rDz6msrIzKysq9ugsAAChv7XrXux1d9lZsJ598crz22mvbPPb666/HwIEDO+T7AwAA+6Z2hVJLS0vccsst8cADD8SaNWtiy5Yt23z8d7/7XVHGffnLX47Ro0fHN77xjTj//PPjueeeizvvvDPuvPPOonx9AACA7WnXu95de+218a1vfSsuuOCCaGhoiOnTp8c555wTXbp0iWuuuaZo4z71qU/Fww8/HD/60Y/ik5/8ZFx33XVx6623xuTJk4v2PQAAAFLt+j1Khx9+eNx2220xYcKEqK6ujuXLl7c99swzz8R99923N7a2i9+jVNq8mUNp82YOpcubOZQub+YAULr2+u9RWr9+fQwbNiwiIg444IBoaGiIiIj/8T/+R/yf//N/2vMlAQAASka7QunQQw+NdevWRcQfzi79/Oc/j4iIJUuWeMc5AACg02tXKJ199tmxYMGCiIj4m7/5m5g1a1YceeSRcdFFF8Wll15a1IEAAAAdrV2vUUo988wz8Ytf/CKOPPLImDhxYjF2FY3XKJU2r1EqbV6jVLq8Rql0eY0SQOnaa79w9kOLFy+O0aNHR7duf/j0k046KU466aT4/e9/H4sXL45Pf/rT7fmyAAAAJaFdl96ddtpp2/1dSQ0NDXHaaaft8SgAAIAstSuUCoVC5HIfvZDtt7/9bfToUW4XhAAAAPua3br07pxzzomIiFwuFxdffPE273DX0tISL730UowePbq4CwEAADrYboVSPp+PiD+cUaquro6qqqq2j1VUVMRJJ50UX/jCF4q7EAAAoIPtVijNmTMnIiJ69+4d11xzTey///4REfHGG2/E3Llz4+ijj46DDz64+CsBAAA6ULteo/TCCy/EPffcExERGzdujJNOOim++c1vxllnnRWzZ88u6kAAAICO1u5Q+tM//dOIiHjwwQejb9++sXr16rjnnnvitttuK+pAAACAjtauUHrvvfeiuro6IiJ+/vOfxznnnBNdunSJk046KVavXl3UgQAAAB2tXaF0xBFHxNy5c2Pt2rUxb968GDduXEREbNiwYZe/4RYAAKDUtSuUrrrqqvjKV74SgwYNihNPPDFGjRoVEX84uzRixIiiDgQAAOhou/Wudx8699xz45RTTol169bF8OHD2x4fM2ZMnH322UUbBwAAkIV2hVJERL9+/aJfv37bPHbCCSfs8SAAAICstevSOwAAgHImlAAAABLtvvQOiuHCrAcU2blZD2CHPpP1AHZqv6wHALBPaI6IWz7mc51RAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABIlHwoDRo0KHK53EduU6dOzXoaAABQprplPWBXlixZEi0tLW33X3nllfjzP//zOO+88zJcBQAAlLOSD6XevXtvc//GG2+Mww8/PD7zmc9ktAgAACh3JR9Kf2zLli3xgx/8IKZPnx65XG67z2lubo7m5ua2+42NjR01DwAAKBMl/xqlPzZ37tzYuHFjXHzxxTt8Tn19feTz+bZbXV1dxw0EAADKQq5QKBSyHvFxnX766VFRURH/9m//tsPnbO+MUl1dXVRFxPbPQUHxnJv1AHao966fQob2y3oAAPuE5oi4JSIaGhqipqZmp8/tNJferV69Oh5//PF46KGHdvq8ysrKqKys7KBVAABAOeo0l97NmTMn+vTpExMmTMh6CgAAUOY6RSi1trbGnDlzYsqUKdGtW6c5CQYAAHRSnSKUHn/88VizZk1ceumlWU8BAAD2AZ3i9My4ceOiE73nBAAA0Ml1ijNKAAAAHUkoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAECipEOppaUlZs2aFYMHD46qqqo4/PDD47rrrotCoZD1NAAAoIx1y3rAztx0000xe/bs+Jd/+ZcYOnRoPP/883HJJZdEPp+Pyy+/POt5AABAmSrpUPrFL34RZ555ZkyYMCEiIgYNGhQ/+tGP4rnnntvh5zQ3N0dzc3Pb/cbGxr2+EwAAKC8lfend6NGjY8GCBfH6669HRMSLL74YTz31VIwfP36Hn1NfXx/5fL7tVldX11FzAQCAMpErlPALflpbW+NrX/ta3HzzzdG1a9doaWmJG264IWbOnLnDz9neGaW6urqoiohcB2xm33Zu1gPYod5ZD2Cn9st6AAD7hOaIuCUiGhoaoqamZqfPLelL7x544IH44Q9/GPfdd18MHTo0li9fHtOmTYva2tqYMmXKdj+nsrIyKisrO3gpAABQTko6lK688sr46le/GhdeeGFERAwbNixWr14d9fX1OwwlAACAPVXSr1F67733okuXbSd27do1WltbM1oEAADsC0r6jNLEiRPjhhtuiAEDBsTQoUPjhRdeiG9961tx6aWXZj0NAAAoYyUdSt/+9rdj1qxZ8dd//dexYcOGqK2tjS9+8Ytx1VVXZT0NAAAoYyX9rnfF0NjYGPl83rve0SG8613p8q53pc273gHQEXbnXe9K+jVKAAAAWRBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAACJkg+lTZs2xbRp02LgwIFRVVUVo0ePjiVLlmQ9CwAAKGMlH0qf//znY/78+XHvvffGyy+/HOPGjYuxY8fGm2++mfU0AACgTOUKhUIh6xE78v7770d1dXU88sgjMWHChLbHjz/++Bg/fnxcf/31u/wajY2Nkc/noyoicntxK0REnJv1AHaod9YD2Kn9sh4AwD6hOSJuiYiGhoaoqanZ6XO7dciidvr9738fLS0t0b17920er6qqiqeeemq7n9Pc3BzNzc1t9xsbG/fqRgAAoPyU9KV31dXVMWrUqLjuuuvirbfeipaWlvjBD34QTz/9dKxbt267n1NfXx/5fL7tVldX18GrAQCAzq6kQyki4t57741CoRCHHHJIVFZWxm233RaTJk2KLl22P33mzJnR0NDQdlu7dm0HLwYAADq7kr70LiLi8MMPj0WLFkVTU1M0NjZG//7944ILLojDDjtsu8+vrKyMysrKDl4JAACUk5I/o/ShHj16RP/+/ePdd9+NefPmxZlnnpn1JAAAoEyV/BmlefPmRaFQiKOOOipWrlwZV155ZQwZMiQuueSSrKcBAABlquTPKDU0NMTUqVNjyJAhcdFFF8Upp5wS8+bNi/3282ayAADA3lHSv0epGPweJTqS36NUuvwepdLmr74A6Ai783uUSv6MEgAAQEcTSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQyDSUFi9eHBMnToza2trI5XIxd+7cbT5eKBTiqquuiv79+0dVVVWMHTs2VqxYkc1YAABgn5FpKDU1NcXw4cPj9ttv3+7Hb7755rjtttvijjvuiGeffTZ69OgRp59+enzwwQcdvBQAANiXdMvym48fPz7Gjx+/3Y8VCoW49dZb4+///u/jzDPPjIiIe+65J/r27Rtz586NCy+8sCOnAgAA+5CSfY3SqlWrYv369TF27Ni2x/L5fJx44onx9NNP7/Dzmpubo7GxcZsbAADA7ijZUFq/fn1ERPTt23ebx/v27dv2se2pr6+PfD7fdqurq9urOwEAgPJTsqHUXjNnzoyGhoa229q1a7OeBAAAdDIlG0r9+vWLiIi33357m8fffvvtto9tT2VlZdTU1GxzAwAA2B0lG0qDBw+Ofv36xYIFC9oea2xsjGeffTZGjRqV4TIAAKDcZfqud5s3b46VK1e23V+1alUsX748evbsGQMGDIhp06bF9ddfH0ceeWQMHjw4Zs2aFbW1tXHWWWdlNxoAACh7mYbS888/H6eddlrb/enTp0dExJQpU+Luu++Ov/u7v4umpqb43//7f8fGjRvjlFNOiZ/97GfRvXv3rCYDAAD7gFyhUChkPWJvamxsjHw+H1URkct6DGXv3KwHsEO9sx7ATu2X9QAA9gnNEXFLRDQ0NOzyvQxK9jVKAAAAWRFKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJAQSgAAAAmhBAAAkBBKAAAACaEEAACQEEoAAAAJoQQAAJDINJQWL14cEydOjNra2sjlcjF37txtPv7QQw/FuHHjolevXpHL5WL58uWZ7AQAAPYtmYZSU1NTDB8+PG6//fYdfvyUU06Jm266qYOXAQAA+7JuWX7z8ePHx/jx43f48c9+9rMREfHGG2987K/Z3Nwczc3NbfcbGxvbvQ8AANg3ld1rlOrr6yOfz7fd6urqsp4EAAB0MmUXSjNnzoyGhoa229q1a7OeBAAAdDKZXnq3N1RWVkZlZWXWMwAAgE6s7M4oAQAA7CmhBAAAkMj00rvNmzfHypUr2+6vWrUqli9fHj179owBAwbE7373u1izZk289dZbERHx2muvRUREv379ol+/fplsBgAAyl+mZ5Sef/75GDFiRIwYMSIiIqZPnx4jRoyIq666KiIifvrTn8aIESNiwoQJERFx4YUXxogRI+KOO+7IbDMAAFD+coVCoZD1iL2psbEx8vl8VEVELusxlL1zsx7ADvXOegA7tV/WAwDYJzRHxC0R0dDQEDU1NTt9rtcoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEBCKAEAACSEEgAAQEIoAQAAJIQSAABAQigBAAAkhBIAAEAi01BavHhxTJw4MWprayOXy8XcuXPbPrZ169aYMWNGDBs2LHr06BG1tbVx0UUXxVtvvZXdYAAAYJ+QaSg1NTXF8OHD4/bbb//Ix957771YtmxZzJo1K5YtWxYPPfRQvPbaa3HGGWdksBQAANiXdMvym48fPz7Gjx+/3Y/l8/mYP3/+No995zvfiRNOOCHWrFkTAwYM6IiJAADAPijTUNpdDQ0Nkcvl4sADD9zhc5qbm6O5ubntfmNjYwcsAwAAykmneTOHDz74IGbMmBGTJk2KmpqaHT6vvr4+8vl8262urq4DVwIAAOWgU4TS1q1b4/zzz49CoRCzZ8/e6XNnzpwZDQ0Nbbe1a9d20EoAAKBclPyldx9G0urVq+Pf//3fd3o2KSKisrIyKisrO2gdAABQjko6lD6MpBUrVsQTTzwRvXr1ynoSAACwD8g0lDZv3hwrV65su79q1apYvnx59OzZM/r37x/nnntuLFu2LB599NFoaWmJ9evXR0REz549o6KiIqvZAABAmcsVCoVCVt984cKFcdppp33k8SlTpsQ111wTgwcP3u7nPfHEE3Hqqad+rO/R2NgY+Xw+qiIitwdb4eM4N+sB7FDvrAewU/tlPQCAfUJzRNwSf3g37V29pCfTM0qnnnpq7KzTMmw4AABgH9Yp3vUOAACgIwklAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgES3rAfsbYVC4Q//N+Md7Bu2ZD2AHWrOegA71Zr1AAD2CR/+PPBhI+xM2YfSpk2bIiLig4x3sG+4P+sBAADs0qZNmyKfz+/0ObnCx8mpTqy1tTXeeuutqK6ujlwut9e+T2NjY9TV1cXatWujpqZmr32fjlJOx1NOxxLheEpZOR1LhOMpZeV0LBGOp5SV07FEOJ5S1lHHUigUYtOmTVFbWxtduuz8VUhlf0apS5cuceihh3bY96upqen0/6L+sXI6nnI6lgjHU8rK6VgiHE8pK6djiXA8paycjiXC8ZSyjjiWXZ1J+pA3cwAAAEgIJQAAgIRQKpLKysq4+uqro7KyMuspRVFOx1NOxxLheEpZOR1LhOMpZeV0LBGOp5SV07FEOJ5SVorHUvZv5gAAALC7nFECAABICCUAAICEUAIAAEgIJQAAgIRQKoLbb789Bg0aFN27d48TTzwxnnvuuawntdvixYtj4sSJUVtbG7lcLubOnZv1pHarr6+PT33qU1FdXR19+vSJs846K1577bWsZ7Xb7Nmz49hjj237RWyjRo2Kxx57LOtZRXHjjTdGLpeLadOmZT2lXa655prI5XLb3IYMGZL1rHZ7880343/9r/8VvXr1iqqqqhg2bFg8//zzWc9ql0GDBn3kn00ul4upU6dmPa1dWlpaYtasWTF48OCoqqqKww8/PK677rrorO/LtGnTppg2bVoMHDgwqqqqYvTo0bFkyZKsZ30su/rzslAoxFVXXRX9+/ePqqqqGDt2bKxYsSKbsR/Dro7noYceinHjxkWvXr0il8vF8uXLM9n5ce3seLZu3RozZsyIYcOGRY8ePaK2tjYuuuiieOutt7IbvBO7+mdzzTXXxJAhQ6JHjx5x0EEHxdixY+PZZ5/NZuzHsDs/a37pS1+KXC4Xt956a4ft+2NCaQ/9+Mc/junTp8fVV18dy5Yti+HDh8fpp58eGzZsyHpauzQ1NcXw4cPj9ttvz3rKHlu0aFFMnTo1nnnmmZg/f35s3bo1xo0bF01NTVlPa5dDDz00brzxxli6dGk8//zz8Wd/9mdx5plnxn/+539mPW2PLFmyJL773e/Gsccem/WUPTJ06NBYt25d2+2pp57KelK7vPvuu3HyySfHfvvtF4899li8+uqr8c1vfjMOOuigrKe1y5IlS7b55zJ//vyIiDjvvPMyXtY+N910U8yePTu+853vxH/913/FTTfdFDfffHN8+9vfznpau3z+85+P+fPnx7333hsvv/xyjBs3LsaOHRtvvvlm1tN2aVd/Xt58881x2223xR133BHPPvts9OjRI04//fT44IMPOnjpx7Or42lqaopTTjklbrrppg5e1j47O5733nsvli1bFrNmzYply5bFQw89FK+99lqcccYZGSzdtV39s/nEJz4R3/nOd+Lll1+Op556KgYNGhTjxo2L3/zmNx289OP5uD9rPvzww/HMM89EbW1tBy3bjgJ75IQTTihMnTq17X5LS0uhtra2UF9fn+Gq4oiIwsMPP5z1jKLZsGFDISIKixYtynpK0Rx00EGF733ve1nPaLdNmzYVjjzyyML8+fMLn/nMZwpXXHFF1pPa5eqrry4MHz486xlFMWPGjMIpp5yS9Yy95oorrigcfvjhhdbW1qyntMuECRMKl1566TaPnXPOOYXJkydntKj93nvvvULXrl0Ljz766DaPH3fccYWvf/3rGa1qn/TPy9bW1kK/fv0K//iP/9j22MaNGwuVlZWFH/3oRxks3D07+/N/1apVhYgovPDCCx26aU98nJ9nnnvuuUJEFFavXt0xo9rp4xxLQ0NDISIKjz/+eMeM2gM7Op5f//rXhUMOOaTwyiuvFAYOHFi45ZZbOnxboVAoOKO0B7Zs2RJLly6NsWPHtj3WpUuXGDt2bDz99NMZLmN7GhoaIiKiZ8+eGS/Zcy0tLXH//fdHU1NTjBo1Kus57TZ16tSYMGHCNv8d6qxWrFgRtbW1cdhhh8XkyZNjzZo1WU9ql5/+9KcxcuTIOO+886JPnz4xYsSIuOuuu7KeVRRbtmyJH/zgB3HppZdGLpfLek67jB49OhYsWBCvv/56RES8+OKL8dRTT8X48eMzXrb7fv/730dLS0t07959m8erqqo67RnZD61atSrWr1+/zf+25fP5OPHEE/18UKIaGhoil8vFgQcemPWUPbJly5a48847I5/Px/Dhw7Oe0y6tra3x2c9+Nq688soYOnRoplu6ZfrdO7l33nknWlpaom/fvts83rdv3/jv//7vjFaxPa2trTFt2rQ4+eST45Of/GTWc9rt5ZdfjlGjRsUHH3wQBxxwQDz88MNxzDHHZD2rXe6///5YtmxZp3k9ws6ceOKJcffdd8dRRx0V69ati2uvvTb+9E//NF555ZWorq7Oet5u+dWvfhWzZ8+O6dOnx9e+9rVYsmRJXH755VFRURFTpkzJet4emTt3bmzcuDEuvvjirKe021e/+tVobGyMIUOGRNeuXaOlpSVuuOGGmDx5ctbTdlt1dXWMGjUqrrvuujj66KOjb9++8aMf/SiefvrpOOKII7Ket0fWr18fEbHdnw8+/Bil44MPPogZM2bEpEmToqamJus57fLoo4/GhRdeGO+99170798/5s+fHwcffHDWs9rlpptuim7dusXll1+e9RShxL5h6tSp8corr3T6v6U86qijYvny5dHQ0BAPPvhgTJkyJRYtWtTpYmnt2rVxxRVXxPz58z/yt8md0R//bf6xxx4bJ554YgwcODAeeOCB+NznPpfhst3X2toaI0eOjG984xsRETFixIh45ZVX4o477uj0ofT9738/xo8fn+317nvogQceiB/+8Idx3333xdChQ2P58uUxbdq0qK2t7ZT/fO6999649NJL45BDDomuXbvGcccdF5MmTYqlS5dmPY19xNatW+P888+PQqEQs2fPznpOu5122mmxfPnyeOedd+Kuu+6K888/P5599tno06dP1tN2y9KlS+Of/umfYtmyZSVx5t+ld3vg4IMPjq5du8bbb7+9zeNvv/129OvXL6NVpC677LJ49NFH44knnohDDz006zl7pKKiIo444og4/vjjo76+PoYPHx7/9E//lPWs3bZ06dLYsGFDHHfccdGtW7fo1q1bLFq0KG677bbo1q1btLS0ZD1xjxx44IHxiU98IlauXJn1lN3Wv3//j4T30Ucf3WkvJfzQ6tWr4/HHH4/Pf/7zWU/ZI1deeWV89atfjQsvvDCGDRsWn/3sZ+PLX/5y1NfXZz2tXQ4//PBYtGhRbN68OdauXRvPPfdcbN26NQ477LCsp+2RD38G8PNBafswklavXh3z58/vtGeTIiJ69OgRRxxxRJx00knx/e9/P7p16xbf//73s56125588snYsGFDDBgwoO3ng9WrV8ff/u3fxqBBgzp8j1DaAxUVFXH88cfHggUL2h5rbW2NBQsWdOrXjZSLQqEQl112WTz88MPx7//+7zF48OCsJxVda2trNDc3Zz1jt40ZMyZefvnlWL58edtt5MiRMXny5Fi+fHl07do164l7ZPPmzfHLX/4y+vfvn/WU3XbyySd/5G30X3/99Rg4cGBGi4pjzpw50adPn5gwYULWU/bIe++9F126bPtHd9euXaO1tTWjRcXRo0eP6N+/f7z77rsxb968OPPMM7OetEcGDx4c/fr12+bng8bGxnj22Wf9fFAiPoykFStWxOOPPx69evXKelJRddafDz772c/GSy+9tM3PB7W1tXHllVfGvHnzOnyPS+/20PTp02PKlCkxcuTIOOGEE+LWW2+NpqamuOSSS7Ke1i6bN2/e5m/BV61aFcuXL4+ePXvGgAEDMly2+6ZOnRr33XdfPPLII1FdXd12XXg+n4+qqqqM1+2+mTNnxvjx42PAgAGxadOmuO+++2LhwoWZ/A/Hnqqurv7Ia8V69OgRvXr16pSvIfvKV74SEydOjIEDB8Zbb70VV199dXTt2jUmTZqU9bTd9uUvfzlGjx4d3/jGN+L888+P5557Lu6888648847s57Wbq2trTFnzpyYMmVKdOvWuf/YmzhxYtxwww0xYMCAGDp0aLzwwgvxrW99Ky699NKsp7XLvHnzolAoxFFHHRUrV66MK6+8MoYMGdIp/gzd1Z+X06ZNi+uvvz6OPPLIGDx4cMyaNStqa2vjrLPOym70TuzqeH73u9/FmjVr2n7X0Id/odKvX7+SPEu2s+Pp379/nHvuubFs2bJ49NFHo6Wlpe1nhJ49e0ZFRUVWs7drZ8fSq1evuOGGG+KMM86I/v37xzvvvBO33357vPnmmyX7axB29e9aGq377bdf9OvXL4466qiOnurtwYvh29/+dmHAgAGFioqKwgknnFB45plnsp7Ubk888UQhIj5ymzJlStbTdtv2jiMiCnPmzMl6WrtceumlhYEDBxYqKioKvXv3LowZM6bw85//POtZRdOZ3x78ggsuKPTv379QUVFROOSQQwoXXHBBYeXKlVnPard/+7d/K3zyk58sVFZWFoYMGVK48847s560R+bNm1eIiMJrr72W9ZQ91tjYWLjiiisKAwYMKHTv3r1w2GGHFb7+9a8Xmpubs57WLj/+8Y8Lhx12WKGioqLQr1+/wtSpUwsbN27MetbHsqs/L1tbWwuzZs0q9O3bt1BZWVkYM2ZMSf87uKvjmTNnznY/fvXVV2e6e0d2djwfvsX59m5PPPFE1tM/YmfH8v777xfOPvvsQm1tbaGioqLQv3//whlnnFF47rnnsp69Q7v7s2aWbw+eKxQ66a/zBgAA2Eu8RgkAACAhlAAAABJCCQAAICGUAAAAEkIJAAAgIZQAAAASQgkAACAhlAAAABJCCQAAICGUAOjULr744jjrrLOyngFAmRFKAAAACaEEQKfw4IMPxrBhw6Kqqip69eoVY8eOjSuvvDL+5V/+JR555JHI5XKRy+Vi4cKFERGxdu3aOP/88+PAAw+Mnj17xplnnhlvvPFG29f78EzUtddeG717946ampr40pe+FFu2bNnp92xqaurgIwcgC92yHgAAu7Ju3bqYNGlS3HzzzXH22WfHpk2b4sknn4yLLroo1qxZE42NjTFnzpyIiOjZs2ds3bo1Tj/99Bg1alQ8+eST0a1bt7j++uvjL/7iL+Kll16KioqKiIhYsGBBdO/ePRYuXBhvvPFGXHLJJdGrV6+44YYbdvg9C4VClv9RANBBhBIAJW/dunXx+9//Ps4555wYOHBgREQMGzYsIiKqqqqiubk5+vXr1/b8H/zgB9Ha2hrf+973IpfLRUTEnDlz4sADD4yFCxfGuHHjIiKioqIi/vmf/zn233//GDp0aPzDP/xDXHnllXHdddft9HsCUP5cegdAyRs+fHiMGTMmhg0bFuedd17cdddd8e677+7w+S+++GKsXLkyqqur44ADDogDDjggevbsGR988EH88pe/3Obr7r///m33R40aFZs3b461a9fu9vcEoLwIJQBKXteuXWP+/Pnx2GOPxTHHHBPf/va346ijjopVq1Zt9/mbN2+O448/PpYvX77N7fXXX4//+T//5175ngCUF6EEQKeQy+Xi5JNPjmuvvTZeeOGFqKioiIcffjgqKiqipaVlm+ced9xxsWLFiujTp08cccQR29zy+Xzb81588cV4//332+4/88wzccABB0RdXd1OvycA5U8oAVDynn322fjGN74Rzz//fKxZsyYeeuih+M1vfhNHH310DBo0KF566aV47bXX4p133omtW7fG5MmT4+CDD44zzzwznnzyyVi1alUsXLgwLr/88vj1r3/d9nW3bNkSn/vc5+LVV1+N//t//29cffXVcdlll0WXLl12+j0BKH/ezAGAkldTUxOLFy+OW2+9NRobG2PgwIHxzW9+M8aPHx8jR46MhQsXxsiRI2Pz5s3xxBNPxKmnnhqLFy+OGTNmxDnnnBObNm2KQw45JMaMGRM1NTVtX3fMmDFx5JFHxqc//elobm6OSZMmxTXXXLPL7wlA+csVvM8pAPugiy++ODZu3Bhz587NegoAJcildwAAAAmhBAAAkHDpHQAAQMIZJQAAgIRQAgAASAglAACAhFACAABICCUAAICEUAIAAEgIJQAAgIRQAgAASPw/JRBQkQqhp2kAAAAASUVORK5CYII=", "text/plain": [ "
" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "res3 = dtmc_evolution(stormvogel_dtmc, steps=15)\n", "labels = [str(i) for i in range(len(stormvogel_dtmc.states))]\n", "extensions.display_value_iteration_result(res3, 10, labels)" ] }, { "cell_type": "markdown", "id": "572faa21", "metadata": {}, "source": [ "Naive DTMC evolution is also available under stormvogel.extensions.visual_algos." ] }, { "cell_type": "code", "execution_count": 8, "id": "12156879", "metadata": { "execution": { "iopub.execute_input": "2026-03-26T10:42:01.940040Z", "iopub.status.busy": "2026-03-26T10:42:01.939855Z", "iopub.status.idle": "2026-03-26T10:42:01.944072Z", "shell.execute_reply": "2026-03-26T10:42:01.943490Z" } }, "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": { "1b332cfdb4ac429a8cabbc250e9b6f66": { "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 } }, "2f38dd3814054f8b951ac512d2402df1": { "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 } }, "3d6dd306e0614f788d877aafd5e60e24": { "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_af4babf3a4974c04a304dd0289d93e5d", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "819f089e4ff24e44847275e374d0bfc1": { "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 } }, "9730778683ab4b88873c6723ce34802c": { "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_2f38dd3814054f8b951ac512d2402df1", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "af4babf3a4974c04a304dd0289d93e5d": { "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 } }, "e02d2066c1524e18a13cc5d3704879c9": { "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_819f089e4ff24e44847275e374d0bfc1", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } }, "f09ec390c28d4a98b18bf8755c0cda48": { "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_1b332cfdb4ac429a8cabbc250e9b6f66", "msg_id": "", "outputs": [], "tabbable": null, "tooltip": null } } }, "version_major": 2, "version_minor": 0 } } }, "nbformat": 4, "nbformat_minor": 5 }