{
"cells": [
{
"cell_type": "markdown",
"id": "497882d8",
"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": "38fd0210",
"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": "8cc82e95",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:39.389950Z",
"iopub.status.busy": "2025-08-27T16:22:39.389779Z",
"iopub.status.idle": "2025-08-27T16:22:40.647740Z",
"shell.execute_reply": "2025-08-27T16:22:40.647219Z"
}
},
"outputs": [],
"source": [
"from stormvogel import *\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",
" transitions = model.get_choice(state)\n",
" # Now we have to take a decision for an action.\n",
" actions = transitions.transition.keys()\n",
" action_values = {}\n",
" for action, branch in transitions.transition.items():\n",
" branch_value = sum([prob * old_values[state.id] for (prob, state) in branch.branch])\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 = sum([abs(x-y) for (x, y) in zip(new_values, old_values)]) < epsilon\n",
" return values_matrix\n",
"\n"
]
},
{
"cell_type": "markdown",
"id": "045c5187",
"metadata": {},
"source": [
"To demonstrate the workings of this algorithm, we use the lion model again."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "f478e6e9",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:40.649668Z",
"iopub.status.busy": "2025-08-27T16:22:40.649397Z",
"iopub.status.idle": "2025-08-27T16:22:42.694765Z",
"shell.execute_reply": "2025-08-27T16:22:42.694224Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "88e12ad362414530a59d918edc163ebf",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/html": [
""
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/javascript": [
"\n",
"function return_id_result(url, id, data) {\n",
" fetch(url, {\n",
" method: 'POST',\n",
" body: JSON.stringify({\n",
" 'id': id,\n",
" 'data': data\n",
" })\n",
" })\n",
" }\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/javascript": [
"return_id_result('http://127.0.0.1:8889', 'pvLIQBbSZaVMclpahKgm', 'test message')"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Test request failed. See 'Implementation details' in docs. Disable warning by use_server=False.\n"
]
},
{
"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": "1e3b5b00",
"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": "fa9f398b",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:42.702916Z",
"iopub.status.busy": "2025-08-27T16:22:42.702663Z",
"iopub.status.idle": "2025-08-27T16:22:42.806466Z",
"shell.execute_reply": "2025-08-27T16:22:42.805941Z"
}
},
"outputs": [
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAAA5cAAAFUCAYAAACwdsjWAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjUsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvWftoOwAAAAlwSFlzAAAPYQAAD2EBqD+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": "8e199685",
"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": "5d3adec7",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:42.808078Z",
"iopub.status.busy": "2025-08-27T16:22:42.807918Z",
"iopub.status.idle": "2025-08-27T16:22:42.811646Z",
"shell.execute_reply": "2025-08-27T16:22:42.811160Z"
}
},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"res2 = extensions.naive_value_iteration(lion, 0.003, lion.get_states_with_label(\"full\")[0])\n",
"res == res2"
]
},
{
"cell_type": "markdown",
"id": "2825e200",
"metadata": {},
"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": "16ec92dc",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:42.813217Z",
"iopub.status.busy": "2025-08-27T16:22:42.813065Z",
"iopub.status.idle": "2025-08-27T16:22:42.816958Z",
"shell.execute_reply": "2025-08-27T16:22:42.816525Z"
}
},
"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": "e8d7b929",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:42.818329Z",
"iopub.status.busy": "2025-08-27T16:22:42.818177Z",
"iopub.status.idle": "2025-08-27T16:22:42.853973Z",
"shell.execute_reply": "2025-08-27T16:22:42.853386Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "e5e2b537a5b24920b9ee18e0987a3fd2",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"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": "bb1337dd",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:42.862048Z",
"iopub.status.busy": "2025-08-27T16:22:42.861824Z",
"iopub.status.idle": "2025-08-27T16:22:43.005440Z",
"shell.execute_reply": "2025-08-27T16:22:43.004990Z"
}
},
"outputs": [
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAAA6IAAALeCAYAAACwb6yJAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjUsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvWftoOwAAAAlwSFlzAAAPYQAAD2EBqD+naQAAVvVJREFUeJzt3XuclmWBP/7PA8gIDAzhgQEER8UjqEimIqXjYT21JvotRMmEzHV39avkqdw0QU2yNcPWYD20ThqttXmonyZqrihSkocGUVklE0GbJCVmBAkV5vdHL+e7Ex44DPcDw/v9ej2v9bmf637uzzW4OR+u+7meUnNzc3MAAACgIB3KHQAAAIDNiyIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQncodgE3fqlWr8oc//CHdu3dPqVQqdxwAAKBMmpub8+abb6Zv377p0OGD1z0VUdbbH/7wh/Tv37/cMQAAgI3EwoULs912233g64oo66179+5J/vovW48ePcqcpm1UV1WVOwIAAGxympP8Jf+vI3wQRZT19t7tuD169Gg3RdQNxgAAsO4+6iN7NisCAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJENwK1tbUplUoplUqpr69f7fW6urr07Nlzrd9z3Lhxa3VOXV1dS461PRcAAGBNKaIbidNPPz0NDQ0ZPHhw5s+fn1Kp1PLaiSeemBdeeGGt3u+OO+7I5Zdf3vK8pqYmkyZNajVm+vTpqampaXWdhoaGDBs2bJ3mAAAAsCY6lTsAf9W1a9dUV1e/72tdunRJly5d1ur9evXqtdYZ3rtO586d1/pcAACANWVFdBPwt7fmjh8/PkOGDMmtt96ampqaVFVVZdSoUXnzzTdbxvzvW3Nra2vz8ssv58tf/nLLrbcAAADloohuol588cXcddddufvuu3P33Xfn4Ycfzje/+c33HXvHHXdku+22y2WXXZaGhoY0NDSs17VXrFiRpqamVg8AAIA1pYhuhGpqatLc3PyhY1atWpW6uroMHjw4n/rUp3LKKafkwQcffN+xvXr1SseOHdO9e/dUV1e33AJcW1ub+fPnr3W+iRMnpqqqquXRv3//tX4PAABg86WIbqJqamrSvXv3lud9+vTJokWLCrn2RRddlMbGxpbHwoULC7kuAADQPtisaBO1xRZbtHpeKpWyatWqQq5dUVGRioqKQq4FAAC0P1ZENxOdO3fOypUryx0DAABAEd1c1NTU5JFHHsmrr76a119/vdxxAACAzZgiupm47LLLMn/+/Oy0007ZZpttyh0HAADYjJWaP2p7Vja42traDBkyJJMmTSp3lCRrn6epqSlVVVVpbGxMjx49Nmy4gnTzXasAALDWmpMsTz6yG1gR3UhMnjw5lZWVmTNnTtkyTJ06NZWVlZkxY0bZMgAAAO2fFdGNwKuvvprly5cnSQYMGJDOnTuXJcebb76Z1157LUnSs2fPbL311mt0nhVRAAAgWfMVUV/fshHo169fuSMkSbp3797qu0kBAAA2BLfmAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACtWp3AFoP6qrqlIqd4g2smx0uRO0nW5Ty52gbX223AHa2E/LHaANbVPuAG3sT+UO0Ma2KHeANvROuQMAsN6siAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIroZqq2tjalUimlUin19fWZP39+y/MhQ4aUOx4AANCOKaKbsdNPPz0NDQ0ZPHhw+vfvn4aGhpx33nnljgUAALRzncodgPLp2rVrqqurW55XV1ensrKyjIkAAIDNgRVRAAAACmVFlLW2YsWKrFixouV5U1NTGdMAAACbGiuirLWJEyemqqqq5dG/f/9yRwIAADYhiihr7aKLLkpjY2PLY+HCheWOBAAAbELcmstaq6ioSEVFRbljAAAAmygrogAAABRKEQUAAKBQiigAAACFUkQBAAAolCK6GZs8eXIqKyszZ86cLFiwIJWVlbnyyivLHQsAAGjn7Jq7mZo6dWqWL1+eJBkwYEA6dOiQ+vr6JLEjLgAAsEEpopupfv36rXZs4MCBZUgCAABsbtyaCwAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShHdTNXW1qZUKqVUKqW+vj7z589veT5kyJByxwMAANoxRXQzdvrpp6ehoSGDBw9O//7909DQkPPOO6/csQAAgHauU7kDUD5du3ZNdXV1y/Pq6upUVlaWMREAALA5UERZaytWrMiKFStanjc1NZUxDQAAsKlxay5rbeLEiamqqmp59O/fv9yRAACATYgiylq76KKL0tjY2PJYuHBhuSMBAACbELfmstYqKipSUVFR7hgAAMAmyoooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRXQzNnny5FRWVmbOnDlZsGBBKisrc+WVV5Y7FgAA0M75+pbN1NSpU7N8+fIkyYABA9KhQ4fU19cnia9mAQAANihFdDPVr1+/1Y4NHDiwDEkAAIDNjVtzAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUJ3KHQA2Rt2mljtB27mt3AHa2KhyB2hje5Q7QBt6rtwB2li3cgdoY8vKHaANdSx3gDa2stwBAMrAiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIbqZqa2tTKpVSKpVSX1+f+fPntzwfMmRIueMBAADtmCK6GTv99NPT0NCQwYMHp3///mloaMh5551X7lgAAEA716ncASifrl27prq6uuV5dXV1Kisry5gIAADYHFgRBQAAoFBWRFlrK1asyIoVK1qeNzU1lTENAACwqbEiylqbOHFiqqqqWh79+/cvdyQAAGATooiy1i666KI0Nja2PBYuXFjuSAAAwCbErbmstYqKilRUVJQ7BgAAsImyIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimim7HJkyensrIyc+bMyYIFC1JZWZkrr7yy3LEAAIB2zq65m6mpU6dm+fLlSZIBAwakQ4cOqa+vTxI74gIAABuUIrqZ6tev32rHBg4cWIYkAADA5satuQAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRTRzVRtbW1KpVJKpVLq6+szf/78ludDhgwpdzwAAKAdU0Q3Y6effnoaGhoyePDg9O/fPw0NDTnvvPPKHQsAAGjnOpU7AOXTtWvXVFdXtzyvrq5OZWVlGRMBAACbAyuiAAAAFMqKKGttxYoVWbFiRcvzpqamMqYBAAA2NVZEWWsTJ05MVVVVy6N///7ljgQAAGxCFFHW2kUXXZTGxsaWx8KFC8sdCQAA2IS4NZe1VlFRkYqKinLHAAAANlFWRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEV0MzZ58uRUVlZmzpw5WbBgQSorK3PllVeWOxYAANDO2TV3MzV16tQsX748STJgwIB06NAh9fX1SWJHXAAAYINSRDdT/fr1W+3YwIEDy5AEAADY3Lg1FwAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCK6maqtrU2pVEqpVEp9fX3mz5/f8nzIkCHljgcAALRjiuhm7PTTT09DQ0MGDx6c/v37p6GhIeedd165YwEAAO1cp3IHoHy6du2a6urqlufV1dWprKwsYyIAAGBzoIiy1lasWJEVK1a0PG9qaipjGgAAYFPj1lzW2sSJE1NVVdXy6N+/f7kjAQAAmxBFlLV20UUXpbGxseWxcOHCckcCAAA2IW7NZa1VVFSkoqKi3DEAAIBNlBVRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiuhmbPLkyamsrMycOXOyYMGCVFZW5sorryx3LAAAoJ3z9S2bqalTp2b58uVJkgEDBqRDhw6pr69PEl/NAgAAbFCK6GaqX79+qx0bOHBgGZIAAACbG7fmAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAodapiD711FOZM2dOy/Of/exnGTFiRP7lX/4lb7/9dpuFAwAAoP1ZpyJ6xhln5IUXXkiS/P73v8+oUaPStWvX/Nd//VcuvPDCNg0IAABA+7JORfSFF17IkCFDkiT/9V//lYMOOig/+tGPUldXl9tvv70t8wEAANDOrFMRbW5uzqpVq5Ikv/zlL3PMMcckSfr375/XX3+97dIBAADQ7qxTEd13331zxRVX5NZbb83DDz+cT3/600mSl156Kb17927TgAAAALQv61REJ02alKeeeipnnXVWvva1r2XgwIFJkp/+9Kc58MAD2zQgAAAA7Uupubm5ua3e7C9/+Us6duyYLbbYoq3ekk1AU1NTqqqq0iVJqdxhWM1t5Q7QxkaVO0Ab26PcAdrQc+UO0Ma6lTtAG1tW7gBtqGO5A7SxleUOANCGmpMsT9LY2JgePXp84Lh1/h7RJUuW5KabbspFF12UxYsXJ0mee+65LFq0aF3fEgAAgM1Ap3U56emnn85hhx2Wnj17Zv78+Tn99NPTq1ev3HHHHVmwYEFuueWWts4JAABAO7FOK6Lnnntuxo4dm3nz5mXLLbdsOX7MMcfkkUceabNwAAAAtD/rVEQff/zxnHHGGasd79evX/74xz+udygAAADar3UqohUVFWlqalrt+AsvvJBtttlmvUMBAADQfq1TEf3MZz6Tyy67LO+8806SpFQqZcGCBfnKV76S//N//k+bBgQAAKB9Waci+u1vfztLly7Ntttum+XLl+fggw/OwIED071793zjG99o64xsALW1tSmVSimVSqmvr8/8+fNbng8ZMqTc8QAAgHZsnXbNraqqygMPPJCZM2dm9uzZWbp0aYYOHZrDDz+8rfOxAZ1++um57LLLsvXWW6dUKqWhoSFXX311fvnLX5Y7GgAA0I6tUxG95ZZbcuKJJ2b48OEZPnx4y/G33347t912W77whS+0WUA2nK5du6a6urrleXV1dSorK8uYCAAA2Bys0625Y8eOTWNj42rH33zzzYwdO3a9QwEAANB+rdOKaHNzc0ql0mrHX3nllVRVVa13KDZuK1asyIoVK1qev98OygAAAB9krYroPvvs07KhzWGHHZZOnf7f6StXrsxLL72Uo446qs1DsnGZOHFiJkyYUO4YAADAJmqtiuiIESOSJPX19TnyyCNbfZ6wc+fOqamp8fUtm4GLLroo5557bsvzpqam9O/fv4yJAACATclaFdFLL700SVJTU5MTTzwxW2655QYJxcatoqIiFRUV5Y4BAABsotbpM6KnnnpqW+cAAABgM7FORXTlypX5zne+k5/85CdZsGBB3n777VavL168uE3CAQAA0P6s09e3TJgwIddcc01OPPHENDY25txzz80JJ5yQDh06ZPz48W0cEQAAgPZknYro1KlTc+ONN+a8885Lp06dctJJJ+Wmm27K17/+9Tz22GNtnREAAIB2ZJ2K6B//+MfsueeeSZLKyso0NjYmSf7+7/8+99xzT9ulY4OaPHlyKisrM2fOnCxYsCCVlZW58soryx0LAABo59bpM6LbbbddGhoaMmDAgOy00065//77M3To0Dz++ON2U91ETJ06NcuXL0+SDBgwIB06dEh9fX2S+DMEAAA2qHUqoscff3wefPDB7L///vm///f/5vOf/3y+//3vZ8GCBfnyl7/c1hnZAPr167fasYEDB5YhCQAAsLkpNTc3N6/vmzz22GP51a9+lZ133jnHHntsW+RiE9LU1JSqqqp0SVIqdxhWc1u5A7SxUeUO0Mb2KHeANvRcuQO0sW7lDtDGlpU7QBvqWO4AbWxluQMAtKHmJMuTNDY2pkePHh84bp1WRB955JEceOCB6dTpr6cfcMABOeCAA/Luu+/mkUceyUEHHbQubwsAAMBmYJ02KzrkkEPe97tCGxsbc8ghh6x3KAAAANqvdSqizc3NKZVWvwnzjTfeSLdu7e1mJgAAANrSWt2ae8IJJyRJSqVSxowZ02p31ZUrV+bpp5/OgQce2LYJAQAAaFfWqohWVVUl+euKaPfu3dOlS5eW1zp37pwDDjggp59+etsmBAAAoF1ZqyJ68803J0m22WabjB8/Pl27dk2SzJ8/P3fddVd23333bL311m2fEgAAgHZjnT4j+tvf/ja33HJLkmTJkiU54IAD8u1vfzsjRozIlClT2jQgAAAA7cs6F9FPfepTSZKf/vSn6d27d15++eXccsst+e53v9umAQEAAGhf1qmIvvXWW+nevXuS5P77788JJ5yQDh065IADDsjLL7/cpgEBAABoX9apiA4cODB33XVXFi5cmPvuuy9HHHFEkmTRokXp0aNHmwYEAACgfVmnIvr1r389559/fmpqarL//vtn2LBhSf66OrrPPvu0aUAAAADal7XaNfc9n/3sZ/PJT34yDQ0N2XvvvVuOH3bYYTn++OPbLBwAAADtzzoV0SSprq5OdXV1q2P77bffegcCAACgfVunW3MBAABgXSmiAAAAFGqdb80FNg2jyh2gjX223AH4QAeXOwAfaotyBwBgs7AiyXfWYJwVUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUapMporW1tSmVSimVSqmvr1/j8+rq6tKzZ88Nlqu9GT9+fMvPedKkSeWOAwAAtEObTBFNktNPPz0NDQ0ZPHhwkmT+/PkplUplTvX+xowZk/Hjx6/VOaVSKfPnz98geT5IXV1damtrW56ff/75aWhoyHbbbVdoDgAAYPPRqdwB1kbXrl1TXV1d7hjtWmVlZSorK9OxY8dyRwEAANqpTWpFdE3U1dVlwIAB6dq1a44//vi88cYbq42ZMmVKdtppp3Tu3Dm77rprbr311lavl0ql3HTTTTn++OPTtWvX7Lzzzvn5z3/easwzzzyTo48+OpWVlendu3dOOeWUvP766206l4cffjj77bdfKioq0qdPn3z1q1/Nu+++2/J6bW1tzj777Fx44YXp1atXqqurV1uFXbJkSb70pS9lm222SY8ePXLooYdm9uzZbZoTAABgbbSrIjpr1qycdtppOeuss1JfX59DDjkkV1xxRasxd955Z84555ycd955eeaZZ3LGGWdk7Nixeeihh1qNmzBhQkaOHJmnn346xxxzTEaPHp3Fixcn+Wu5O/TQQ7PPPvvkiSeeyLRp0/Laa69l5MiRbTaXV199Ncccc0w+8YlPZPbs2ZkyZUq+//3vrzafH/zgB+nWrVtmzZqVb33rW7nsssvywAMPtLz+uc99LosWLcq9996bJ598MkOHDs1hhx3WMpd1sWLFijQ1NbV6AAAArKlSc3Nzc7lDrIna2toMGTLkQzfQOfnkk9PY2Jh77rmn5dioUaMybdq0LFmyJEkyfPjwDBo0KDfccEPLmJEjR2bZsmUt55VKpVx88cW5/PLLkyTLli1LZWVl7r333hx11FG54oorMmPGjNx3330t7/HKK6+kf//+ef7557PLLrus93y/9rWv5fbbb8/cuXNbPgc7efLkfOUrX0ljY2M6dOiQ2trarFy5MjNmzGg5b7/99suhhx6ab37zm3n00Ufz6U9/OosWLUpFRUXLmIEDB+bCCy/MP/zDP3zg9WtqajJu3LiMGzdutdfGjx+fCRMmrHa8S5KN8xO7tCefLXcAPtA25Q7Ah9qi3AEA2CysSPKdJI2NjenRo8cHjmtXK6Jz587N/vvv3+rYsGHDVhszfPjwVseGDx+euXPntjq21157tfxzt27d0qNHjyxatChJMnv27Dz00EMtn6esrKzMbrvtliR58cUX22wuw4YNa7UZ0/Dhw7N06dK88sor75szSfr06dMq59KlS7PVVlu1yvrSSy+tV86LLroojY2NLY+FCxeu83sBAACbn01qs6IibbFF6787LpVKWbVqVZJk6dKlOfbYY3PVVVetdl6fPn0Kyfeej8rZp0+fTJ8+fbXz1ucrbSoqKlqtsAIAAKyNdlVEd99998yaNavVsccee2y1MTNnzsypp57acmzmzJnZY4891vg6Q4cOze23356ampp06rRhfoS77757br/99jQ3N7esis6cOTPdu3df469WGTp0aP74xz+mU6dOqamp2SA5AQAA1la7ujX37LPPzrRp03L11Vdn3rx5ue666zJt2rRWYy644ILU1dVlypQpmTdvXq655prccccdOf/889f4OmeeeWYWL16ck046KY8//nhefPHF3HfffRk7dmxWrlzZJnP553/+5yxcuDD/9//+3/zP//xPfvazn+XSSy/Nueeemw4d1uyP7fDDD8+wYcMyYsSI3H///Zk/f35+9atf5Wtf+1qeeOKJNskJAACwttpVET3ggANy44035tprr83ee++d+++/PxdffHGrMSNGjMi1116bq6++OoMGDcr111+fm2++ObW1tWt8nb59+2bmzJlZuXJljjjiiOy5554ZN25cevbs+YElcfz48Wu1KtmvX7/84he/yG9+85vsvffe+cd//Mecdtppq83nw5RKpfziF7/IQQcdlLFjx2aXXXbJqFGj8vLLL6d3795r/D4AAABtqV3tmrsxO/XUU1MqlVJXV1fuKGvkw3bN/VtNTU2pqqqyay6FsGvuxsuuuRs3u+YCUIR2uWvu5MmTU1lZmTlz5pQ7ylppbm7O9OnTW74OZmN25ZVXprKyMgsWLCh3FAAAoJ3aZFZEX3311SxfvjxJMmDAgHTu3LnMidqnxYsXZ/HixUmSbbbZJlVVVR95jhVRimRFdONlRXTjZkUUgCKs6YroJrNrbr9+/codYbPQq1ev9OrVq9wxAACAdmyTujUXAACATZ8iCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCbTJFtLa2NqVSKaVSKfX19Wt8Xl1dXXr27LnBcrU3NTU1LT/nJUuWlDsOAADQDm0yRTRJTj/99DQ0NGTw4MFJkvnz56dUKpU51fsbM2ZMxo8fv1bnlEqlzJ8/P0kyffr0QspgbW1t6urqWp4//vjjuf322zfoNQEAgM1bp3IHWBtdu3ZNdXV1uWO0a9tss0169epV7hgAAEA7tkmtiK6Jurq6DBgwIF27ds3xxx+fN954Y7UxU6ZMyU477ZTOnTtn1113za233trq9VKplJtuuinHH398unbtmp133jk///nPW4155plncvTRR6eysjK9e/fOKaecktdff71N5jB//vwccsghSZKPfexjKZVKGTNmTO6+++707NkzK1euTJLU19enVCrlq1/9asu5X/rSl/L5z3++5fntt9+eQYMGpaKiIjU1Nfn2t7+93vlWrFiRpqamVg8AAIA11a6K6KxZs3LaaaflrLPOSn19fQ455JBcccUVrcbceeedOeecc3LeeeflmWeeyRlnnJGxY8fmoYceajVuwoQJGTlyZJ5++ukcc8wxGT16dBYvXpwkWbJkSQ499NDss88+eeKJJzJt2rS89tprGTlyZJvMo3///i23xz7//PNpaGjItddem0996lN5880389vf/jZJ8vDDD2frrbfO9OnTW859+OGHU1tbmyR58sknM3LkyIwaNSpz5szJ+PHjc8kll7S6FXddTJw4MVVVVS2P/v37r9f7AQAAm5dSc3Nzc7lDrIna2toMGTIkkyZN+sAxJ598chobG3PPPfe0HBs1alSmTZvW8lnL4cOHZ9CgQbnhhhtaxowcOTLLli1rOa9UKuXiiy/O5ZdfniRZtmxZKisrc++99+aoo47KFVdckRkzZuS+++5reY9XXnkl/fv3z/PPP59ddtllvec7ffr0HHLIIfnzn//carOlj3/84znppJNy/vnn5/jjj88nPvGJTJgwIW+88UYaGxuz3Xbb5YUXXsjOO++c0aNH509/+lPuv//+lvMvvPDC3HPPPXn22WfX+trvWbFiRVasWNHyvKmpKf3790+XJBvnJ3ZpTz5b7gB8oG3KHYAPtUW5AwCwWViR5DtJGhsb06NHjw8c165WROfOnZv999+/1bFhw4atNmb48OGtjg0fPjxz585tdWyvvfZq+edu3bqlR48eWbRoUZJk9uzZeeihh1JZWdny2G233ZIkL774YpvN5/0cfPDBmT59epqbmzNjxoyccMIJ2X333fPoo4/m4YcfTt++fbPzzjsn+eC5zps3r+X23nVRUVGRHj16tHoAAACsqU1qs6IibbFF6787LpVKWbVqVZJk6dKlOfbYY3PVVVetdl6fPn02aK7a2tr8x3/8R2bPnp0tttgiu+22W2prazN9+vT8+c9/zsEHH7xBrw8AALC+2tWK6O67755Zs2a1OvbYY4+tNmbmzJmtjs2cOTN77LHHGl9n6NChefbZZ1NTU5OBAwe2enTr1m3dJ/C/dO7cOUlWW7l873Oi3/nOd1pK53tFdPr06S2fD00+eK677LJLOnbs2CY5AQAA1la7KqJnn312pk2blquvvjrz5s3Lddddl2nTprUac8EFF6Suri5TpkzJvHnzcs011+SOO+7I+eefv8bXOfPMM7N48eKcdNJJefzxx/Piiy/mvvvuy9ixY9frltf/bfvtt0+pVMrdd9+dP/3pT1m6dGmSv+6iu9dee2Xq1KktpfOggw7KU089lRdeeKHViuh5552XBx98MJdffnleeOGF/OAHP8h11123VnMFAABoa+2qiB5wwAG58cYbc+2112bvvffO/fffn4svvrjVmBEjRuTaa6/N1VdfnUGDBuX666/PzTff3Gol8aP07ds3M2fOzMqVK3PEEUdkzz33zLhx49KzZ8906PD+P9Lx48enpqZmja/Rr1+/TJgwIV/96lfTu3fvnHXWWS2vHXzwwVm5cmVL5l69emWPPfZIdXV1dt1115ZxQ4cOzU9+8pPcdtttGTx4cL7+9a/nsssuy5gxY9Y4BwAAQFtrV7vmbsxOPfXUlEql9f7qlCJ81K65f6upqSlVVVV2zaUQds3deNk1d+Nm11wAitAud82dPHlyKisrM2fOnHJHWSvNzc2ZPn16y9fBbMwGDRqUo48+utwxAACAdmyT2TV36tSpWb58eZJkwIABZU6zdkqlUl5++eVyx1gjv/jFL/LOO+8kia9lAQAANohNpoj269ev3BE2C9tvv325IwAAAO3cJnVrLgAAAJs+RRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUGUtorW1tSmVSimVSqmvr1/j8+rq6tKzZ88NlqtotbW1GTduXLljJEnGjx/f8mcyadKkcscBAADaobKviJ5++ulpaGjI4MGDkyTz589PqVQqc6r3N2bMmIwfP36tzimVSpk/f36SZPr06SmVSlmyZEmbZ1tXdXV1qa2tbXl+/vnnp6GhIdttt135QgEAAO1ap3IH6Nq1a6qrq8sdY5PzzjvvZIsttmjz962srExlZWU6duzY5u8NAACQbAQromuirq4uAwYMSNeuXXP88cfnjTfeWG3MlClTstNOO6Vz587Zddddc+utt7Z6vVQq5aabbsrxxx+frl27Zuedd87Pf/7zVmOeeeaZHH300amsrEzv3r1zyimn5PXXX2+TOcyfPz+HHHJIkuRjH/tYSqVSxowZ0/L6qlWrcuGFF6ZXr16prq5ebeW1VCplypQp+cxnPpNu3brlG9/4RpLkZz/7WYYOHZott9wyO+64YyZMmJB333235bwlS5bkS1/6UrbZZpv06NEjhx56aGbPnt0mcwIAAFgXG30RnTVrVk477bScddZZqa+vzyGHHJIrrrii1Zg777wz55xzTs4777w888wzOeOMMzJ27Ng89NBDrcZNmDAhI0eOzNNPP51jjjkmo0ePzuLFi5P8tbAdeuih2WefffLEE09k2rRpee211zJy5Mg2mUf//v1z++23J0mef/75NDQ05Nprr215/Qc/+EG6deuWWbNm5Vvf+lYuu+yyPPDAA63eY/z48Tn++OMzZ86cfPGLX8yMGTPyhS98Ieecc06ee+65XH/99amrq2spqUnyuc99LosWLcq9996bJ598MkOHDs1hhx3WMu91sWLFijQ1NbV6AAAArKlSc3Nzc7kuXltbmyFDhnzopjgnn3xyGhsbc88997QcGzVqVKZNm9byWcvhw4dn0KBBueGGG1rGjBw5MsuWLWs5r1Qq5eKLL87ll1+eJFm2bFkqKytz77335qijjsoVV1yRGTNm5L777mt5j1deeSX9+/fP888/n1122WW95zt9+vQccsgh+fOf/9xqs6Xa2tqsXLkyM2bMaDm233775dBDD803v/nNlvzjxo3Ld77znZYxhx9+eA477LBcdNFFLcd++MMf5sILL8wf/vCHPProo/n0pz+dRYsWpaKiomXMwIEDc+GFF+Yf/uEfPjBrTU1Nxo0b976bKI0fPz4TJkxY7XiXJBvnp3tpTz5b7gB8oG3KHYAP1fYf5gCA1a1I8p0kjY2N6dGjxweO2+hXROfOnZv999+/1bFhw4atNmb48OGtjg0fPjxz585tdWyvvfZq+edu3bqlR48eWbRoUZJk9uzZeeihh1o+I1lZWZnddtstSfLiiy+22Xw+yP/OliR9+vRpyfaefffdt9Xz2bNn57LLLmuV+b3Nn956663Mnj07S5cuzVZbbdVqzEsvvbRec7rooovS2NjY8li4cOE6vxcAALD5KftmRUX62819SqVSVq1alSRZunRpjj322Fx11VWrndenT5+yZntPt27dWj1funRpJkyYkBNOOGG199tyyy2zdOnS9OnTJ9OnT1/t9fX5+puKiopWK6wAAABrY6MvorvvvntmzZrV6thjjz222piZM2fm1FNPbTk2c+bM7LHHHmt8naFDh+b2229PTU1NOnXaMD+Wzp07J0lWrlzZJu83dOjQPP/88xk4cOAHvv7HP/4xnTp1Sk1NTZtcEwAAYH1t9Lfmnn322Zk2bVquvvrqzJs3L9ddd12mTZvWaswFF1yQurq6TJkyJfPmzcs111yTO+64I+eff/4aX+fMM8/M4sWLc9JJJ+Xxxx/Piy++mPvuuy9jx45ts+K4/fbbp1Qq5e67786f/vSnLF26dL3e7+tf/3puueWWTJgwIc8++2zmzp2b2267LRdffHGSv36GdNiwYRkxYkTuv//+zJ8/P7/61a/yta99LU888URbTAkAAGCtbfRF9IADDsiNN96Ya6+9NnvvvXfuv//+lqL1nhEjRuTaa6/N1VdfnUGDBuX666/PzTffnNra2jW+Tt++fTNz5sysXLkyRxxxRPbcc8+MGzcuPXv2TIcO7/9jGj9+/FqtNPbr1y8TJkzIV7/61fTu3TtnnXXWGp/7fo488sjcfffduf/++/OJT3wiBxxwQL7zne9k++23T/LX23t/8Ytf5KCDDsrYsWOzyy67ZNSoUXn55ZfTu3fv9bo2AADAutrod83dmJ166qkplUqpq6srd5Q292G75v6tpqamVFVV2TWXQtg1d+Nl19yNm11zASjCJrNr7uTJk1NZWZk5c+aUO8paaW5uzvTp01u+Dqa9uPLKK1NZWZkFCxaUOwoAANBOlXVF9NVXX83y5cuTJAMGDGjZzIfyWbx4cRYvXpwk2WabbVJVVfWR51gRpUhWRDdeVkQ3blZEASjCmq6IlnXX3H79+pXz8ryPXr16pVevXuWOAQAAtGNlvzUXAACAzYsiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCbdRFtLa2NqVSKaVSKfX19R847q677srAgQPTsWPHjBs3rrB8bammpiaTJk0qa4bp06e3/LxHjBhR1iwAAED7tVEX0SQ5/fTT09DQkMGDBydJ5s+fn1Kp1GrMGWeckc9+9rNZuHBhLr/88g2aZ/r06ampqVmrc8aMGZPx48dvkDzr429/lgceeGAaGhoycuTIMqYCAADau07lDvBRunbtmurq6g98fenSpVm0aFGOPPLI9O3bd4Nmeeeddzbo+5db586dU11dnS5dumTFihXljgMAALRTG/2K6IeZPn16unfvniQ59NBDUyqVMn369CTJ7bffnkGDBqWioiI1NTX59re/3ercUqmUu+66q9Wxnj17pq6uLsn/Wy388Y9/nIMPPjhbbrllpk6d2ia5Fy1alGOPPTZdunTJDjvs8L7vu2DBghx33HGprKxMjx49MnLkyLz22mstr48fPz5DhgzJrbfempqamlRVVWXUqFF58803W8asWrUqEydOzA477JAuXbpk7733zk9/+tM2mQMAAMC62qSL6IEHHpjnn38+yV+LZ0NDQw488MA8+eSTGTlyZEaNGpU5c+Zk/PjxueSSS1pK5tr46le/mnPOOSdz587NkUce2Sa5x4wZk4ULF+ahhx7KT3/600yePDmLFi1qeX3VqlU57rjjsnjx4jz88MN54IEH8vvf/z4nnnhiq/d58cUXc9ddd+Xuu+/O3XffnYcffjjf/OY3W16fOHFibrnllvz7v/97nn322Xz5y1/O5z//+Tz88MPrlX/FihVpampq9QAAAFhTG/2tuX+rpqYmzc3NSf56K+m2226bJOnVq1fLLbzXXHNNDjvssFxyySVJkl122SXPPfdc/vVf/zVjxoxZq+uNGzcuJ5xwQsvzPn36ZP78+Wv1Hv+7AL/wwgu5995785vf/Caf+MQnkiTf//73s/vuu7eMefDBBzNnzpy89NJL6d+/f5LklltuyaBBg/L444+3nLdq1arU1dW1rAqfcsopefDBB/ONb3wjK1asyJVXXplf/vKXGTZsWJJkxx13zKOPPprrr78+Bx98cKuf5dqYOHFiJkyYsNbnAQAAJJv4iugHmTt3boYPH97q2PDhwzNv3rysXLlyrd5r3333bctomTt3bjp16pSPf/zjLcd222239OzZs9WY/v37t5TQJNljjz3Ss2fPzJ07t+VYTU1NSwlN/lqS31tZ/d3vfpe33norf/d3f5fKysqWxy233JIXX3xxveZw0UUXpbGxseWxcOHC9Xo/AABg87LJrYi2lVKptNpq4PttRtStW7eiIq21LbbYotXzUqmUVatWJfnrJk5Jcs8996Rfv36txlVUVKzXdSsqKtb7PQAAgM1Xuyyiu+++e2bOnNnq2MyZM7PLLrukY8eOSZJtttkmDQ0NLa/Pmzcvb7311gbPtttuu+Xdd9/Nk08+2XKL7fPPP58lS5a0yr9w4cIsXLiwZVX0ueeey5IlS7LHHnus0XX22GOPVFRUZMGCBTn44IPbfB4AAADrql0W0fPOOy+f+MQncvnll+fEE0/Mr3/961x33XWZPHlyy5hDDz001113XYYNG5aVK1fmK1/5ymorjBvCrrvumqOOOipnnHFGpkyZkk6dOmXcuHHp0qVLy5jDDz88e+65Z0aPHp1Jkybl3XffzT//8z/n4IMPXuNbhbt3757zzz8/X/7yl7Nq1ap88pOfTGNjY2bOnJkePXrk1FNP3VBTBAAA+FDt8jOiQ4cOzU9+8pPcdtttGTx4cL7+9a/nsssua7VR0be//e30798/n/rUp3LyySfn/PPPT9euXdf6Wu99zct7XxuzJm6++eb07ds3Bx98cE444YT8wz/8Q8umS8lfb7H92c9+lo997GM56KCDcvjhh2fHHXfMj3/847XKdvnll+eSSy7JxIkTs/vuu+eoo47KPffckx122GGt3gcAAKAtlZrXZdvUgtTW1mbIkCGZNGlSuaN8oIceeignnHBCfv/73+djH/tYueO0iTFjxmTJkiWrfc/qB2lqakpVVVW6JClt0GSQfLbcAfhA25Q7AB9qw9/zAwDJiiTfSdLY2JgePXp84LiNfkV08uTJqayszJw5c8od5X394he/yL/8y7+0ixI6Y8aMVFZWZurUqeWOAgAAtGMb9Yroq6++muXLlydJBgwYkM6dO5c5Ufu2fPnyvPrqq0mSysrKlu9l/ShWRCmSFdGNlxXRjZsVUQCKsKYrohv1ZkV/+7UjbFhdunTJwIEDyx0DAABo5zb6W3MBAABoXxRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRqkymitbW1KZVKKZVKqa+vX+Pz6urq0rNnzw2Wa0OaOXNm9txzz2yxxRYZMWJEpk+fnlKplCVLlmywa44ZM6bl53zXXXdtsOsAAACbr02miCbJ6aefnoaGhgwePDhJMn/+/JRKpTKnen9jxozJ+PHj1+qcUqmU+fPntzw/99xzM2TIkLz00kupq6vLgQcemIaGhlRVVbVZzvHjx2fMmDEtz6+99to0NDS02fsDAAD8rU2qiHbt2jXV1dXp1KlTuaMU4sUXX8yhhx6a7bbbLj179kznzp1TXV29Qct3VVVVqqurN9j7AwAAbFJFdE3U1dVlwIAB6dq1a44//vi88cYbq42ZMmVKdtppp3Tu3Dm77rprbr311lavl0ql3HTTTTn++OPTtWvX7Lzzzvn5z3/easwzzzyTo48+OpWVlendu3dOOeWUvP76620yh/dWet9444188YtfTKlUSl1dXatbc5uamtKlS5fce++9rc698847071797z11ltJkoULF2bkyJHp2bNnevXqleOOO67Vquu6WLFiRZqamlo9AAAA1lS7KqKzZs3KaaedlrPOOiv19fU55JBDcsUVV7Qac+edd+acc87Jeeedl2eeeSZnnHFGxo4dm4ceeqjVuAkTJmTkyJF5+umnc8wxx2T06NFZvHhxkmTJkiU59NBDs88+++SJJ57ItGnT8tprr2XkyJFtMo/+/funoaEhPXr0yKRJk9LQ0JATTzyx1ZgePXrk7//+7/OjH/2o1fGpU6dmxIgR6dq1a955550ceeSR6d69e2bMmJGZM2emsrIyRx11VN5+++11zjdx4sRUVVW1PPr377/O7wUAAGx+Ss3Nzc3lDrEmamtrM2TIkEyaNOkDx5x88slpbGzMPffc03Js1KhRmTZtWssGP8OHD8+gQYNyww03tIwZOXJkli1b1nJeqVTKxRdfnMsvvzxJsmzZslRWVubee+/NUUcdlSuuuCIzZszIfffd1/Ier7zySvr375/nn38+u+yyS5vMuWfPnpk0aVLLZzinT5+eQw45JH/+85/Ts2fP3HXXXTnllFPy2muvpWvXrmlqakrv3r1z55135qijjsoPf/jDXHHFFZk7d27L7bxvv/12y7lHHHHEB167VCrlzjvvzIgRI1Z7bcWKFVmxYkXL86ampvTv3z9dkmycn9ilPflsuQPwgbYpdwA+1BblDgDAZmFFku8kaWxsTI8ePT5wXLtaEZ07d27233//VseGDRu22pjhw4e3OjZ8+PDMnTu31bG99tqr5Z+7deuWHj16ZNGiRUmS2bNn56GHHkplZWXLY7fddkvy1891FuWYY47JFlts0XLb8O23354ePXrk8MMPb8n5u9/9Lt27d2/J2atXr/zlL39Zr5wVFRXp0aNHqwcAAMCa2jx2/VkHW2zR+u+OS6VSVq1alSRZunRpjj322Fx11VWrndenT59C8iVJ586d89nPfjY/+tGPMmrUqPzoRz/KiSee2LKZ09KlS/Pxj388U6dOXe3cbbaxdgEAAJRHuyqiu+++e2bNmtXq2GOPPbbamJkzZ+bUU09tOTZz5szssccea3ydoUOH5vbbb09NTU3Zd/AdPXp0/u7v/i7PPvts/vu//7vVZ2KHDh2aH//4x9l2222tWgIAABuNdnVr7tlnn51p06bl6quvzrx583Lddddl2rRprcZccMEFqaury5QpUzJv3rxcc801ueOOO3L++eev8XXOPPPMLF68OCeddFIef/zxvPjii7nvvvsyduzYrFy5sq2n9aEOOuigVFdXZ/To0dlhhx1a3Zo8evTobL311jnuuOMyY8aMvPTSS5k+fXrOPvvsvPLKK4XmBAAAeE+7KqIHHHBAbrzxxlx77bXZe++9c//99+fiiy9uNWbEiBG59tprc/XVV2fQoEG5/vrrc/PNN6e2tnaNr9O3b9/MnDkzK1euzBFHHJE999wz48aNS8+ePdOhw/v/SMePH5+ampr1mN37K5VKOemkkzJ79uyMHj261Wtdu3bNI488kgEDBuSEE07I7rvvntNOOy1/+ctfrJACAABl0652zd2YnXrqqS3fB7op+LBdc/9WU1NTqqqq7JpLIeyau/HyyfONm11zAShCu9w1d/LkyamsrMycOXPKHWWtNDc3Z/r06S1fB7Mx+8d//MdUVlaWOwYAANCObTIroq+++mqWL1+eJBkwYEA6d+5c5kTt06JFi9LU1JTkrzsAd+vW7SPPsSJKkayIbrysiG7crIgCUIQ1XRHdZHbN7devX7kjbBa23XbbbLvttuWOAQAAtGOb1K25AAAAbPoUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCbfJFtLa2NqVSKaVSKfX19Wt8Xl1dXXr27LnBcpXD/Pnz1/rn8Lfe+1m2t58NAACw8djki2iSnH766WloaMjgwYOT/L9CtjEaM2ZMxo8fv1bnlEqlzJ8//yPH9e/fv9XPYU3U1NRk+vTpLc8bGhoyadKktcoHAACwNjqVO0Bb6Nq1a6qrq8sdo+w6duy43j+H6urqVFVVtVEiAACA1bWLFdE1UVdXlwEDBqRr1645/vjj88Ybb6w2ZsqUKdlpp53SuXPn7Lrrrrn11ltbvV4qlXLTTTfl+OOPT9euXbPzzjvn5z//easxzzzzTI4++uhUVlamd+/eOeWUU/L666+32Tz+/Oc/Z/To0dlmm23SpUuX7Lzzzrn55puTrH5r7mWXXZa+ffu2muunP/3pHHLIIVm1alWbZQIAAFgbm0URnTVrVk477bScddZZqa+vzyGHHJIrrrii1Zg777wz55xzTs4777w888wzOeOMMzJ27Ng89NBDrcZNmDAhI0eOzNNPP51jjjkmo0ePzuLFi5MkS5YsyaGHHpp99tknTzzxRKZNm5bXXnstI0eObLO5XHLJJXnuuedy7733Zu7cuZkyZUq23nrr9x37ta99LTU1NfnSl76UJPne976XX/3qV/nBD36QDh3W/Y9+xYoVaWpqavUAAABYU6Xm5ubmcodYH7W1tRkyZMiHfq7x5JNPTmNjY+65556WY6NGjcq0adOyZMmSJMnw4cMzaNCg3HDDDS1jRo4cmWXLlrWcVyqVcvHFF+fyyy9PkixbtiyVlZW59957c9RRR+WKK67IjBkzct9997W8xyuvvJL+/fvn+eefzy677LLe8/3MZz6TrbfeOv/xH/+x2mvz58/PDjvskN/+9rcZMmRIkuT3v/99hgwZkn/+53/Od7/73dx00005+eSTP/QadXV1GTduXMvP5m+NHz8+EyZMWO14lyQb5ydzaU8+W+4AfKBtyh2AD7VFuQMAsFlYkeQ7SRobG9OjR48PHLdZrIjOnTs3+++/f6tjw4YNW23M8OHDWx0bPnx45s6d2+rYXnvt1fLP3bp1S48ePbJo0aIkyezZs/PQQw+lsrKy5bHbbrslSV588cU2mcs//dM/5bbbbsuQIUNy4YUX5le/+tWHjt9xxx1z9dVX56qrrspnPvOZjyyha+Kiiy5KY2Njy2PhwoXr/Z4AAMDmo11sVlSkLbZo/XfKpVKp5fOWS5cuzbHHHpurrrpqtfP69OnTJtc/+uij8/LLL+cXv/hFHnjggRx22GE588wzc/XVV3/gOY888kg6duyY+fPn5913302nTuv3x15RUZGKior1eg8AAGDztVmsiO6+++6ZNWtWq2OPPfbYamNmzpzZ6tjMmTOzxx57rPF1hg4dmmeffTY1NTUZOHBgq0e3bt3WfQJ/Y5tttsmpp56aH/7wh5k0aVKr24n/1o9//OPccccdmT59ehYsWNByWzEAAEC5bBZF9Oyzz860adNy9dVXZ968ebnuuusybdq0VmMuuOCC1NXVZcqUKZk3b16uueaa3HHHHTn//PPX+DpnnnlmFi9enJNOOimPP/54Xnzxxdx3330ZO3ZsVq5c2SZz+frXv56f/exn+d3vfpdnn302d999d3bffff3HfvKK6/kn/7pn3LVVVflk5/8ZG6++eZceeWVq5VwAACAIm0WRfSAAw7IjTfemGuvvTZ777137r///lx88cWtxowYMSLXXnttrr766gwaNCjXX399br755tTW1q7xdfr27ZuZM2dm5cqVOeKII7Lnnntm3Lhx6dmz5wfuUjt+/PjU1NSs8TU6d+6ciy66KHvttVcOOuigdOzYMbfddttq45qbmzNmzJjst99+Oeuss5IkRx55ZP7pn/4pn//857N06dI1viYAAEBb2ix2zd2YnXrqqSmVSqmrqyt3lBYftWvu32pqakpVVZVdcymEXXM3XnbN3bjZNReAIqzprrntYrOiyZMn56abbsqvf/3r7LnnnuWOs8aam5szffr0PProo+WO0qKysjLvvvtuttxyy3JHAQAA2qlNvohOnTo1y5cvT5IMGDCgzGnWTqlUyssvv1zuGK3U19cnSTp27FjeIAAAQLu1yRfRfv36lTtCuzJw4MByRwAAANq5zWKzIgAAADYeiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEJ1KncANn3Nzc1//b9lzsHm4e1yB+ADrSh3AD7UqnIHAGCz8N7vA+91hA+iiLLe3nzzzSTJX8qcg83DbeUOAADAR3rzzTdTVVX1ga+Xmj+qqsJHWLVqVf7whz+ke/fuKZVKG+w6TU1N6d+/fxYuXJgePXpssOsUoT3NJTGfjVl7mktiPhuz9jSXxHw2Zu1pLon5bMza01yS4ubT3NycN998M3379k2HDh/8SVAroqy3Dh06ZLvttivsej169GgX/2OQtK+5JOazMWtPc0nMZ2PWnuaSmM/GrD3NJTGfjVl7mktSzHw+bCX0PTYrAgAAoFCKKAAAAIVSRNlkVFRU5NJLL01FRUW5o6y39jSXxHw2Zu1pLon5bMza01wS89mYtae5JOazMWtPc0k2vvnYrAgAAIBCWREFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUTYJ3/ve91JTU5Mtt9wy+++/f37zm9+UO9I6e+SRR3Lsscemb9++KZVKueuuu8odaZ1NnDgxn/jEJ9K9e/dsu+22GTFiRJ5//vlyx1onU6ZMyV577dXyJc/Dhg3LvffeW+5Ybeab3/xmSqVSxo0bV+4o62T8+PEplUqtHrvttlu5Y62zV199NZ///Oez1VZbpUuXLtlzzz3zxBNPlDvWOqmpqVntz6ZUKuXMM88sd7R1snLlylxyySXZYYcd0qVLl+y00065/PLLs6nu7fjmm29m3Lhx2X777dOlS5cceOCBefzxx8sda4181H8vm5ub8/Wvfz19+vRJly5dcvjhh2fevHnlCbsGPmo+d9xxR4444ohstdVWKZVKqa+vL0vONfFhc3nnnXfyla98JXvuuWe6deuWvn375gtf+EL+8Ic/lC/wR/ioP5vx48dnt912S7du3fKxj30shx9+eGbNmlWesGtgbX7X/Md//MeUSqVMmjSpsHzvUUTZ6P34xz/Oueeem0svvTRPPfVU9t577xx55JFZtGhRuaOtk2XLlmXvvffO9773vXJHWW8PP/xwzjzzzDz22GN54IEH8s477+SII47IsmXLyh1trW233Xb55je/mSeffDJPPPFEDj300Bx33HF59tlnyx1tvT3++OO5/vrrs9dee5U7ynoZNGhQGhoaWh6PPvpouSOtkz//+c8ZPnx4tthii9x777157rnn8u1vfzsf+9jHyh1tnTz++OOt/lweeOCBJMnnPve5MidbN1dddVWmTJmS6667LnPnzs1VV12Vb33rW/m3f/u3ckdbJ1/60pfywAMP5NZbb82cOXNyxBFH5PDDD8+rr75a7mgf6aP+e/mtb30r3/3ud/Pv//7vmTVrVrp165Yjjzwyf/nLXwpOumY+aj7Lli3LJz/5yVx11VUFJ1t7HzaXt956K0899VQuueSSPPXUU7njjjvy/PPP5zOf+UwZkq6Zj/qz2WWXXXLddddlzpw5efTRR1NTU5Mjjjgif/rTnwpOumbW9HfNO++8M4899lj69u1bULK/0Qwbuf3226/5zDPPbHm+cuXK5r59+zZPnDixjKnaRpLmO++8s9wx2syiRYuakzQ//PDD5Y7SJj72sY8133TTTeWOsV7efPPN5p133rn5gQceaD744IObzznnnHJHWieXXnpp8957713uGG3iK1/5SvMnP/nJcsfYYM4555zmnXbaqXnVqlXljrJOPv3pTzd/8YtfbHXshBNOaB49enSZEq27t956q7ljx47Nd999d6vjQ4cObf7a175WplTr5m//e7lq1arm6urq5n/9139tObZkyZLmioqK5v/8z/8sQ8K182H//X/ppZeakzT/9re/LTTTulqT32V+85vfNCdpfvnll4sJtR7WZD6NjY3NSZp/+ctfFhNqPXzQfF555ZXmfv36NT/zzDPN22+/ffN3vvOdwrNZEWWj9vbbb+fJJ5/M4Ycf3nKsQ4cOOfzww/PrX/+6jMl4P42NjUmSXr16lTnJ+lm5cmVuu+22LFu2LMOGDSt3nPVy5pln5tOf/nSr/x/aVM2bNy99+/bNjjvumNGjR2fBggXljrROfv7zn2fffffN5z73uWy77bbZZ599cuONN5Y7Vpt4++2388Mf/jBf/OIXUyqVyh1nnRx44IF58MEH88ILLyRJZs+enUcffTRHH310mZOtvXfffTcrV67Mlltu2ep4ly5dNtk7Ct7z0ksv5Y9//GOr/22rqqrK/vvv7/eDjVBjY2NKpVJ69uxZ7ijr7e23384NN9yQqqqq7L333uWOs05WrVqVU045JRdccEEGDRpUthydynZlWAOvv/56Vq5cmd69e7c63rt37/zP//xPmVLxflatWpVx48Zl+PDhGTx4cLnjrJM5c+Zk2LBh+ctf/pLKysrceeed2WOPPcoda53ddttteeqppzaZz4N9mP333z91dXXZdddd09DQkAkTJuRTn/pUnnnmmXTv3r3c8dbK73//+0yZMiXnnntu/uVf/iWPP/54zj777HTu3DmnnnpqueOtl7vuuitLlizJmDFjyh1lnX31q19NU1NTdtttt3Ts2DErV67MN77xjYwePbrc0dZa9+7dM2zYsFx++eXZfffd07t37/znf/5nfv3rX2fgwIHljrde/vjHPybJ+/5+8N5rbBz+8pe/5Ctf+UpOOumk9OjRo9xx1tndd9+dUaNG5a233kqfPn3ywAMPZOutty53rHVy1VVXpVOnTjn77LPLmkMRBdrEmWeemWeeeWaT/lv2XXfdNfX19WlsbMxPf/rTnHrqqXn44Yc3yTK6cOHCnHPOOXnggQdWWw3ZFP3v1ai99tor+++/f7bffvv85Cc/yWmnnVbGZGtv1apV2XfffXPllVcmSfbZZ58888wz+fd///dNvoh+//vfz9FHH12+zxu1gZ/85CeZOnVqfvSjH2XQoEGpr6/PuHHj0rdv303yz+fWW2/NF7/4xfTr1y8dO3bM0KFDc9JJJ+XJJ58sdzQ2A++8805GjhyZ5ubmTJkypdxx1sshhxyS+vr6vP7667nxxhszcuTIzJo1K9tuu225o62VJ598Mtdee22eeuqpst+54tZcNmpbb711OnbsmNdee63V8ddeey3V1dVlSsXfOuuss3L33XfnoYceynbbbVfuOOusc+fOGThwYD7+8Y9n4sSJ2XvvvXPttdeWO9Y6efLJJ7No0aIMHTo0nTp1SqdOnfLwww/nu9/9bjp16pSVK1eWO+J66dmzZ3bZZZf87ne/K3eUtdanT5/V/nJj991332RvNX7Pyy+/nF/+8pf50pe+VO4o6+WCCy7IV7/61YwaNSp77rlnTjnllHz5y1/OxIkTyx1tney00055+OGHs3Tp0ixcuDC/+c1v8s4772THHXcsd7T18t7vAH4/2Hi9V0JffvnlPPDAA5v0amiSdOvWLQMHDswBBxyQ73//++nUqVO+//3vlzvWWpsxY0YWLVqUAQMGtPx+8PLLL+e8885LTU1NoVkUUTZqnTt3zsc//vE8+OCDLcdWrVqVBx98cJP/7F570NzcnLPOOit33nln/vu//zs77LBDuSO1qVWrVmXFihXljrFODjvssMyZMyf19fUtj3333TejR49OfX19OnbsWO6I62Xp0qV58cUX06dPn3JHWWvDhw9f7WuOXnjhhWy//fZlStQ2br755my77bb59Kc/Xe4o6+Wtt95Khw6tfz3q2LFjVq1aVaZEbaNbt27p06dP/vznP+e+++7LcccdV+5I62WHHXZIdXV1q98PmpqaMmvWLL8fbATeK6Hz5s3LL3/5y2y11VbljtTmNtXfEU455ZQ8/fTTrX4/6Nu3by644ILcd999hWZxay4bvXPPPTennnpq9t133+y3336ZNGlSli1blrFjx5Y72jpZunRpq1Wcl156KfX19enVq1cGDBhQxmRr78wzz8yPfvSj/OxnP0v37t1bPpdTVVWVLl26lDnd2rnoooty9NFHZ8CAAXnzzTfzox/9KNOnTy/8f5TbSvfu3Vf7rG63bt2y1VZbbZKf4T3//PNz7LHHZvvtt88f/vCHXHrppenYsWNOOumkckdba1/+8pdz4IEH5sorr8zIkSPzm9/8JjfccENuuOGGckdbZ6tWrcrNN9+cU089NZ06bdq/Whx77LH5xje+kQEDBmTQoEH57W9/m2uuuSZf/OIXyx1tndx3331pbm7Orrvumt/97ne54IILsttuu20S/w39qP9ejhs3LldccUV23nnn7LDDDrnkkkvSt2/fjBgxonyhP8RHzWfx4sVZsGBBy/dtvvcXVtXV1RvdKu+HzaVPnz757Gc/m6eeeip33313Vq5c2fL7Qa9evdK5c+dyxf5AHzafrbbaKt/4xjfymc98Jn369Mnrr7+e733ve3n11Vc32q+p+qh/1/72Lwa22GKLVFdXZ9dddy02aOH79MI6+Ld/+7fmAQMGNHfu3Ll5v/32a37sscfKHWmdPfTQQ81JVnuceuqp5Y621t5vHkmab7755nJHW2tf/OIXm7fffvvmzp07N2+zzTbNhx12WPP9999f7lhtalP++pYTTzyxuU+fPs2dO3du7tevX/OJJ57Y/Lvf/a7csdbZ//f//X/NgwcPbq6oqGjebbfdmm+44YZyR1ov9913X3OS5ueff77cUdZbU1NT8znnnNM8YMCA5i233LJ5xx13bP7a177WvGLFinJHWyc//vGPm3fcccfmzp07N1dXVzefeeaZzUuWLCl3rDXyUf+9XLVqVfMll1zS3Lt37+aKiormww47bKP+d/Cj5nPzzTe/7+uXXnppWXO/nw+by3tfP/N+j4ceeqjc0d/Xh81n+fLlzccff3xz3759mzt37tzcp0+f5s985jPNv/nNb8od+wOt7e+a5fr6llJzc3Nz29dbAAAAeH8+IwoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEA4EONGTMmI0aMKHcMANoRRRQAAIBCKaIAQJLkpz/9afbcc8906dIlW221VQ4//PBccMEF+cEPfpCf/exnKZVKKZVKmT59epJk4cKFGTlyZHr27JlevXrluOOOy/z581ve772V1AkTJmSbbbZJjx498o//+I95++23P/Say5YtK3jmABStU7kDAADl19DQkJNOOinf+ta3cvzxx+fNN9/MjBkz8oUvfCELFixIU1NTbr755iRJr1698s477+TII4/MsGHDMmPGjHTq1ClXXHFFjjrqqDz99NPp3LlzkuTBBx/MlltumenTp2f+/PkZO3Zsttpqq3zjG9/4wGs2NzeX80cBQAEUUQAgDQ0Neffdd3PCCSdk++23T5LsueeeSZIuXbpkxYoVqa6ubhn/wx/+MKtWrcpNN92UUqmUJLn55pvTs2fPTJ8+PUcccUSSpHPnzvmP//iPdO3aNYMGDcpll12WCy64IJdffvmHXhOA9s2tuQBA9t577xx22GHZc88987nPfS433nhj/vznP3/g+NmzZ+d3v/tdunfvnsrKylRWVqZXr175y1/+khdffLHV+3bt2rXl+bBhw7J06dIsXLhwra8JQPuhiAIA6dixYx544IHce++92WOPPfJv//Zv2XXXXfPSSy+97/ilS5fm4x//eOrr61s9XnjhhZx88skb5JoAtB+KKACQJCmVShk+fHgmTJiQ3/72t+ncuXPuvPPOdO7cOStXrmw1dujQoZk3b1623XbbDBw4sNWjqqqqZdzs2bOzfPnyluePPfZYKisr079//w+9JgDtmyIKAGTWrFm58sor88QTT2TBggW544478qc//Sm77757ampq8vTTT+f555/P66+/nnfeeSejR4/O1ltvneOOOy4zZszISy+9lOnTp+fss8/OK6+80vK+b7/9dk477bQ899xz+cUvfpFLL700Z511Vjp06PCh1wSgfbNZEQCQHj165JFHHsmkSZPS1NSU7bffPt/+9rdz9NFHZ99998306dOz7777ZunSpXnooYdSW1ubRx55JF/5yldywgkn5M0330y/fv1y2GGHpUePHi3ve9hhh2XnnXfOQQcdlBUrVuSkk07K+PHjP/KaALRvpWZ7pAMAG8CYMWOyZMmS3HXXXeWOAsBGxq25AAAAFEoRBQAAoFBuzQUAAKBQVkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACF+v8Bok++wNo2+psAAAAASUVORK5CYII=",
"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": "c28e001f",
"metadata": {},
"source": [
"Naive DTMC evolution is also available under stormvogel.extensions.visual_algos."
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "5c36c1a6",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-27T16:22:43.007064Z",
"iopub.status.busy": "2025-08-27T16:22:43.006905Z",
"iopub.status.idle": "2025-08-27T16:22:43.010498Z",
"shell.execute_reply": "2025-08-27T16:22:43.010044Z"
}
},
"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.13.3"
},
"widgets": {
"application/vnd.jupyter.widget-state+json": {
"state": {
"1772ce928f9d4390af590e627909c669": {
"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_a4a1f2f4793a4f278796004a7ca2c90c",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "7ea0db5ca8ee4511846a7f1cad5b3583",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"2147b40b22614fb9aa8b2338711ea20a": {
"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
}
},
"2ce52a7767c44f8cb0677df5d9c4960a": {
"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
}
},
"305272dc337e47d685de06cda5b4459d": {
"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
}
},
"36fd463cd4ef4ce9bb4568b0f7a449a0": {
"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_4f8103df68d048ec9768f3ac64222f59",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"4d689049a8a44723b624d9f4d5afc6ba": {
"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
}
},
"4f8103df68d048ec9768f3ac64222f59": {
"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
}
},
"5a8a335547e043e6acc1e386758455c0": {
"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_c461c0092e614f80b89f2b3daa70e555",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"6ce9883421ff44ed887a65bd62836bd1": {
"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
}
},
"76f6d8e943884356ae81030718917b24": {
"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
}
},
"7df565fa28f44a489da1f0630e33689a": {
"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_986412ce99044b0283a454eeadbc6b3b",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"7ea0db5ca8ee4511846a7f1cad5b3583": {
"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_2147b40b22614fb9aa8b2338711ea20a",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"858c9639bb854c259b1623ffbdb9f3b0": {
"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_2ce52a7767c44f8cb0677df5d9c4960a",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"88e12ad362414530a59d918edc163ebf": {
"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_d6146295c0cd41fb8bf5d542ac88db06",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"986412ce99044b0283a454eeadbc6b3b": {
"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
}
},
"a17d2a8f768d41ca9d2eab192e74bf7c": {
"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_4d689049a8a44723b624d9f4d5afc6ba",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"a4a1f2f4793a4f278796004a7ca2c90c": {
"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
}
},
"c197066a6736488aa9a0b3e606f0922e": {
"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_305272dc337e47d685de06cda5b4459d",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"c461c0092e614f80b89f2b3daa70e555": {
"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
}
},
"d6146295c0cd41fb8bf5d542ac88db06": {
"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
}
},
"e5e2b537a5b24920b9ee18e0987a3fd2": {
"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_6ce9883421ff44ed887a65bd62836bd1",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"fd8a8b89088f43a6980f4a521e603909": {
"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_76f6d8e943884356ae81030718917b24",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "7ea0db5ca8ee4511846a7f1cad5b3583",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}