{
"cells": [
{
"cell_type": "markdown",
"id": "60210d7e-8f61-4c36-a1e2-2b87fff3ce45",
"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": "9bf66c40-1be3-42b5-9bef-923f69c0ccee",
"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": "333a5dee-bb57-474b-b94f-b6638d1f079c",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:51.652788Z",
"iopub.status.busy": "2025-07-21T08:28:51.652609Z",
"iopub.status.idle": "2025-07-21T08:28:52.799079Z",
"shell.execute_reply": "2025-07-21T08:28:52.798555Z"
}
},
"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.get_states().items():\n",
" transitions = model.get_transitions(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",
" "
]
},
{
"cell_type": "markdown",
"id": "34c60252-6c87-4ba8-b1be-604b7c64da81",
"metadata": {},
"source": [
"To demonstrate the workings of this algorithm, we use the lion model again."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "35f63205-b804-4852-9080-eee3a0429008",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:52.801024Z",
"iopub.status.busy": "2025-07-21T08:28:52.800743Z",
"iopub.status.idle": "2025-07-21T08:28:54.878208Z",
"shell.execute_reply": "2025-07-21T08:28:54.877653Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "a02378d172c649eaa7a2a170d44e8061",
"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', 'vzbMwJcnMsGVEZNFSwzC', '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": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "5c49a23aca9243e7a4d9615a01d7cc5a",
"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": [
"lion = examples.create_lion_mdp()\n",
"vis = show(lion, layout=Layout(\"layouts/lion.json\"))"
]
},
{
"cell_type": "markdown",
"id": "6a71e2ff-69d3-4b9a-b33c-d1034788306b",
"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": "682664f5-c41d-4d83-a6a9-1a27396e7d33",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:54.929397Z",
"iopub.status.busy": "2025-07-21T08:28:54.929185Z",
"iopub.status.idle": "2025-07-21T08:28:55.036245Z",
"shell.execute_reply": "2025-07-21T08:28:55.035751Z"
}
},
"outputs": [
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAAA5cAAAFUCAYAAACwdsjWAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjMsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvZiW1igAAAAlwSFlzAAAPYQAAD2EBqD+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": "5d98fa60-6f76-48ab-b1f8-c92e33d67b23",
"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": "651c53f9-19d6-434f-89e4-4e91993c8277",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:55.038048Z",
"iopub.status.busy": "2025-07-21T08:28:55.037719Z",
"iopub.status.idle": "2025-07-21T08:28:55.041336Z",
"shell.execute_reply": "2025-07-21T08:28:55.040945Z"
}
},
"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": "775772d4-4351-412a-bb91-cddfcb9f119c",
"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": "411be602-21bd-423a-b15d-493738f02d89",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:55.042885Z",
"iopub.status.busy": "2025-07-21T08:28:55.042721Z",
"iopub.status.idle": "2025-07-21T08:28:55.047149Z",
"shell.execute_reply": "2025-07-21T08:28:55.046737Z"
}
},
"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.get_states().items():\n",
" branch = model.get_branch(s)\n",
" for transition_prob, target in branch.branch:\n",
" current_prob = matrix_steps_states[current_step][s_id]\n",
" matrix_steps_states[next_step][target.id] += current_prob * float(\n",
" transition_prob\n",
" )\n",
"\n",
" return matrix_steps_states"
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "4a3e4fcf-d7f7-4fac-b457-47388315790f",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:55.048633Z",
"iopub.status.busy": "2025-07-21T08:28:55.048469Z",
"iopub.status.idle": "2025-07-21T08:28:55.122199Z",
"shell.execute_reply": "2025-07-21T08:28:55.121703Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "98ac9d34d6b54e40b7fc082652072e72",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "cf995c76f3ae41b0b81e8f2f5c311328",
"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": "f8f81c4b-fc48-4bf9-b933-4f35263f8cee",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:55.173742Z",
"iopub.status.busy": "2025-07-21T08:28:55.173260Z",
"iopub.status.idle": "2025-07-21T08:28:55.320288Z",
"shell.execute_reply": "2025-07-21T08:28:55.319844Z"
}
},
"outputs": [
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAAA6IAAALeCAYAAACwb6yJAAAAOnRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjEwLjMsIGh0dHBzOi8vbWF0cGxvdGxpYi5vcmcvZiW1igAAAAlwSFlzAAAPYQAAD2EBqD+naQAAV0lJREFUeJzt3Xl4VfWBP/73BSQCgSCKBhCMiguCitSqSNW4fF3acZ0WtdaKC6NWR6lrrVVBLdSOttix2Fo7Ui2OdurWcV9+gkjrbhSVulUEbVrqWIgoRoX8/vAxMykuEOK5EF6v5zlPueeee877k1DJO59zP7fU1NTUFAAAAChIh3IHAAAAYPWiiAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKFSncgdg1bdkyZL8+c9/Tvfu3VMqlcodBwAAKJOmpqa89dZb6du3bzp0+OR5T0WUFfbnP/85/fv3L3cMAABgJTF37tysv/76n/i8IsoK6969e5IP/7L16NGjzGnaRnVVVbkjAADAKqcpybv5347wSRRRVthHt+P26NGj3RRRNxgDAEDrfdZb9ixWBAAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliK4EamtrUyqVUiqVUldXt9TzkydPTs+ePZf7nGPGjFmu10yePLk5x/K+FgAAYFkpoiuJ0aNHp76+PkOGDMns2bNTKpWanzv44IPzwgsvLNf5brzxxlxwwQXNj2tqajJx4sQWx0ydOjU1NTUtrlNfX5/hw4e3agwAAADLolO5A/Chrl27prq6+mOf69KlS7p06bJc5+vVq9dyZ/joOp07d17u1wIAACwrM6KrgH+8NXfs2LEZOnRorrnmmtTU1KSqqiqHHHJI3nrrreZj/u+tubW1tXn11Vfz7W9/u/nWWwAAgHJRRFdRL7/8cm6++ebceuutufXWWzNt2rT84Ac/+Nhjb7zxxqy//vo5//zzU19fn/r6+hW6dmNjYxoaGlpsAAAAy0oRXQnV1NSkqanpU49ZsmRJJk+enCFDhmSnnXbK4Ycfnvvuu+9jj+3Vq1c6duyY7t27p7q6uvkW4Nra2syePXu5802YMCFVVVXNW//+/Zf7HAAAwOpLEV1F1dTUpHv37s2P+/Tpk3nz5hVy7bPOOisLFixo3ubOnVvIdQEAgPbBYkWrqDXWWKPF41KplCVLlhRy7YqKilRUVBRyLQAAoP0xI7qa6Ny5cxYvXlzuGAAAAIro6qKmpiYPPPBAXn/99bzxxhvljgMAAKzGFNHVxPnnn5/Zs2dn4403Tu/evcsdBwAAWI2Vmj5reVY+d7W1tRk6dGgmTpxY7ihJlj9PQ0NDqqqqsmDBgvTo0ePzDVeQbj5rFQAAlltTkkXJZ3YDM6IriUmTJqWysjIzZ84sW4YpU6aksrIy06dPL1sGAACg/TMjuhJ4/fXXs2jRoiTJgAED0rlz57LkeOutt/LXv/41SdKzZ8+ss846y/Q6M6IAAECy7DOiPr5lJdCvX79yR0iSdO/evcVnkwIAAHwe3JoLAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAoVKdyB6D9qK6qSqncIdrI24eVO0Hb6Tal3Ana1lfLHaCN/bbcAdpQ73IHaGN/K3eANrZGuQO0offLHQCAFWZGFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkRXU7W1tSmVSimVSqmrq8vs2bObHw8dOrTc8QAAgHZMEV2NjR49OvX19RkyZEj69++f+vr6nHrqqeWOBQAAtHOdyh2A8unatWuqq6ubH1dXV6eysrKMiQAAgNWBGVEAAAAKZUaU5dbY2JjGxsbmxw0NDWVMAwAArGrMiLLcJkyYkKqqquatf//+5Y4EAACsQhRRlttZZ52VBQsWNG9z584tdyQAAGAV4tZclltFRUUqKirKHQMAAFhFmREFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEU0dXYpEmTUllZmZkzZ2bOnDmprKzM+PHjyx0LAABo56yau5qaMmVKFi1alCQZMGBAOnTokLq6uiSxIi4AAPC5UkRXU/369Vtq38CBA8uQBAAAWN24NRcAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiupqqra1NqVRKqVRKXV1dZs+e3fx46NCh5Y4HAAC0Y4roamz06NGpr6/PkCFD0r9//9TX1+fUU08tdywAAKCd61TuAJRP165dU11d3fy4uro6lZWVZUwEAACsDhRRlltjY2MaGxubHzc0NJQxDQAAsKpxay7LbcKECamqqmre+vfvX+5IAADAKkQRZbmdddZZWbBgQfM2d+7cckcCAABWIW7NZblVVFSkoqKi3DEAAIBVlBlRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiuhqbNKkSamsrMzMmTMzZ86cVFZWZvz48eWOBQAAtHM+vmU1NWXKlCxatChJMmDAgHTo0CF1dXVJ4qNZAACAz5Uiuprq16/fUvsGDhxYhiQAAMDqxq25AAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQqE7lDgAro25Typ2g7VxX7gBt7JByB2hjW5Q7QBt6rtwB2li3cgdoY2+XO0Ab6ljuAG1scbkDAJSBGVEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRXU3V1tamVCqlVCqlrq4us2fPbn48dOjQcscDAADaMUV0NTZ69OjU19dnyJAh6d+/f+rr63PqqaeWOxYAANDOdSp3AMqna9euqa6ubn5cXV2dysrKMiYCAABWB2ZEAQAAKJQZUZZbY2NjGhsbmx83NDSUMQ0AALCqMSPKcpswYUKqqqqat/79+5c7EgAAsApRRFluZ511VhYsWNC8zZ07t9yRAACAVYhbc1luFRUVqaioKHcMAABgFWVGFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkRXY5MmTUplZWVmzpyZOXPmpLKyMuPHjy93LAAAoJ2zau5qasqUKVm0aFGSZMCAAenQoUPq6uqSxIq4AADA50oRXU3169dvqX0DBw4sQxIAAGB149ZcAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiuhqqra2NqVSKaVSKXV1dZk9e3bz46FDh5Y7HgAA0I4poqux0aNHp76+PkOGDEn//v1TX1+fU089tdyxAACAdq5TuQNQPl27dk11dXXz4+rq6lRWVpYxEQAAsDowIwoAAEChzIiy3BobG9PY2Nj8uKGhoYxpAACAVY0ZUZbbhAkTUlVV1bz179+/3JEAAIBViCLKcjvrrLOyYMGC5m3u3LnljgQAAKxC3JrLcquoqEhFRUW5YwAAAKsoM6IAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiuhqbNGlSKisrM3PmzMyZMyeVlZUZP358uWMBAADtnFVzV1NTpkzJokWLkiQDBgxIhw4dUldXlyRWxAUAAD5Xiuhqql+/fkvtGzhwYBmSAAAAqxu35gIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEV1O1tbUplUoplUqpq6vL7Nmzmx8PHTq03PEAAIB2TBFdjY0ePTr19fUZMmRI+vfvn/r6+px66qnljgUAALRzncodgPLp2rVrqqurmx9XV1ensrKyjIkAAIDVgSLKcmtsbExjY2Pz44aGhjKmAQAAVjVuzWW5TZgwIVVVVc1b//79yx0JAABYhSiiLLezzjorCxYsaN7mzp1b7kgAAMAqxK25LLeKiopUVFSUOwYAALCKMiMKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEV2NTZo0KZWVlZk5c2bmzJmTysrKjB8/vtyxAACAds7Ht6ympkyZkkWLFiVJBgwYkA4dOqSuri5JfDQLAADwuVJEV1P9+vVbat/AgQPLkAQAAFjduDUXAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAK1aoi+sQTT2TmzJnNj2+55ZYccMAB+e53v5v33nuvzcIBAADQ/rSqiB577LF54YUXkiR/+tOfcsghh6Rr1675r//6r5xxxhltGhAAAID2pVVF9IUXXsjQoUOTJP/1X/+VnXfeOddee20mT56cG264oS3zAQAA0M60qog2NTVlyZIlSZJ77703X/7yl5Mk/fv3zxtvvNF26QAAAGh3WlVEt91221x44YW55pprMm3atHzlK19JkrzyyitZb7312jQgAAAA7UuriujEiRPzxBNP5MQTT8zZZ5+dgQMHJkl++9vfZscdd2zTgAAAALQvpaampqa2Otm7776bjh07Zo011mirU7IKaGhoSFVVVbokKZU7DEu5rtwB2tgh5Q7QxrYod4A29Fy5A7SxbuUO0MbeLneANtSx3AHa2OJyBwBoQ01JFiVZsGBBevTo8YnHtfpzROfPn58rr7wyZ511Vt58880kyXPPPZd58+a19pQAAACsBjq15kVPP/10dt999/Ts2TOzZ8/O6NGj06tXr9x4442ZM2dOrr766rbOCQAAQDvRqhnRU045JUceeWRefPHFrLnmms37v/zlL+eBBx5os3AAAAC0P60qoo8++miOPfbYpfb369cvf/nLX1Y4FAAAAO1Xq4poRUVFGhoaltr/wgsvpHfv3iscCgAAgParVUV0v/32y/nnn5/3338/SVIqlTJnzpyceeaZ+ed//uc2DQgAAED70qoieskll2ThwoVZd911s2jRouyyyy4ZOHBgunfvnu9///ttnZHPQW1tbUqlUkqlUurq6jJ79uzmx0OHDi13PAAAoB1r1aq5VVVVueeeezJjxow89dRTWbhwYYYNG5Y99tijrfPxORo9enTOP//8rLPOOimVSqmvr8/FF1+ce++9t9zRAACAdqxVRfTqq6/OwQcfnBEjRmTEiBHN+997771cd911+eY3v9lmAfn8dO3aNdXV1c2Pq6urU1lZWcZEAADA6qBVt+YeeeSRWbBgwVL733rrrRx55JErHAoAAID2q1Uzok1NTSmVSkvtf+2111JVVbXCoVi5NTY2prGxsfnxx62gDAAA8EmWq4hus802zQva7L777unU6X9fvnjx4rzyyivZe++92zwkK5cJEyZk3Lhx5Y4BAACsopariB5wwAFJkrq6uuy1114t3k/YuXPn1NTU+PiW1cBZZ52VU045pflxQ0ND+vfvX8ZEAADAqmS5iuh5552XJKmpqcnBBx+cNddc83MJxcqtoqIiFRUV5Y4BAACsolr1HtEjjjiirXMAAACwmmhVEV28eHF+/OMf5ze/+U3mzJmT9957r8Xzb775ZpuEAwAAoP1p1ce3jBs3Lj/60Y9y8MEHZ8GCBTnllFNy0EEHpUOHDhk7dmwbRwQAAKA9aVURnTJlSn7xi1/k1FNPTadOnXLooYfmyiuvzLnnnpuHHnqorTMCAADQjrSqiP7lL3/JlltumSSprKzMggULkiT/9E//lNtuu63t0vG5mjRpUiorKzNz5szMmTMnlZWVGT9+fLljAQAA7Vyr3iO6/vrrp76+PgMGDMjGG2+cu+++O8OGDcujjz5qNdVVxJQpU7Jo0aIkyYABA9KhQ4fU1dUlie8hAADwuWpVET3wwANz3333Zfvtt8+//uu/5hvf+EZ++ctfZs6cOfn2t7/d1hn5HPTr12+pfQMHDixDEgAAYHVTampqalrRkzz00EP5/e9/n0022ST77rtvW+RiFdLQ0JCqqqp0SVIqdxiWcl25A7SxQ8odoI1tUe4Abei5cgdoY93KHaCNvV3uAG2oY7kDtLHF5Q4A0IaakixKsmDBgvTo0eMTj2vVjOgDDzyQHXfcMZ06ffjyHXbYITvssEM++OCDPPDAA9l5551bc1oAAABWA61arGjXXXf92M8KXbBgQXbdddcVDgUAAED71aoi2tTUlFJp6Zsw/+d//ifdurW3m5kAAABoS8t1a+5BBx2UJCmVShk1alSL1VUXL16cp59+OjvuuGPbJgQAAKBdWa4iWlVVleTDGdHu3bunS5cuzc917tw5O+ywQ0aPHt22CQEAAGhXlquIXnXVVUmS3r17Z+zYsenatWuSZPbs2bn55pszaNCgrLPOOm2fEgAAgHajVe8RffLJJ3P11VcnSebPn58ddtghl1xySQ444IBcfvnlbRoQAACA9qXVRXSnnXZKkvz2t7/Neuutl1dffTVXX311fvKTn7RpQAAAANqXVhXRd955J927d0+S3H333TnooIPSoUOH7LDDDnn11VfbNCAAAADtS6uK6MCBA3PzzTdn7ty5ueuuu7LnnnsmSebNm5cePXq0aUAAAADal1YV0XPPPTennXZaampqsv3222f48OFJPpwd3Wabbdo0IAAAAO3Lcq2a+5GvfvWr+dKXvpT6+vpsvfXWzft33333HHjggW0WDgAAgPanVUU0Saqrq1NdXd1i33bbbbfCgQAAAGjfWnVrLgAAALSWIgoAAEChWn1rLrBqOKTcAdrYV8sdgE+0S7kD8KnWKHcAAFYLjUl+vAzHmREFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKFWmSJaW1ubUqmUUqmUurq6csdpc7Nnz14pxjZ27Njmr/PEiRPLmgUAAGifVpkimiSjR49OfX19hgwZkuR/y1vRxo4dm1GjRi3Xa2pqajJ16tTPJc+KmDx5cmpra5sfn3baaamvr8/6669fvlAAAEC71qncAZZH165dU11dXe4Y7VplZWUqKyvTsWPHckcBAADaqVVqRnRZ3HDDDRk8eHAqKipSU1OTSy65pMXzNTU1GT9+fI466qh07949AwYMyBVXXNHimLlz52bkyJHp2bNnevXqlf333z+zZ89u05yPPPJIttlmm6y55prZdttt8+STTy51zLRp07LddtuloqIiffr0yXe+85188MEHzc/X1tbmpJNOyhlnnJFevXqluro6Y8eObXGO+fPn55hjjknv3r3To0eP7LbbbnnqqafadCwAAADLo10V0ccffzwjR47MIYcckpkzZ2bs2LE555xzMnny5BbHXXLJJc3l71vf+laOP/74PP/880mS999/P3vttVe6d++e6dOnZ8aMGamsrMzee++d9957r01yLly4MP/0T/+ULbbYIo8//njGjh2b0047rcUxr7/+er785S/ni1/8Yp566qlcfvnl+eUvf5kLL7ywxXG/+tWv0q1btzz88MP54Q9/mPPPPz/33HNP8/Nf+9rXMm/evNxxxx15/PHHM2zYsOy+++558803W52/sbExDQ0NLTYAAIBlVWpqamoqd4hlUVtbm6FDh37qAjqHHXZY/va3v+Xuu+9u3nfGGWfktttuy7PPPpvkwxnRnXbaKddcc02SpKmpKdXV1Rk3blyOO+64/PrXv86FF16YWbNmNb//9L333kvPnj1z8803Z88991zhsVxxxRX57ne/m9deey1rrrlmkuRnP/tZjj/++Dz55JMZOnRozj777Nxwww0tckyaNClnnnlmFixYkA4dOqS2tjaLFy/O9OnTm8+93XbbZbfddssPfvCDPPjgg/nKV76SefPmpaKiovmYgQMH5owzzsi//Mu/fGLGmpqajBkzJmPGjFnqubFjx2bcuHFL7e+SpPh37LK6+Wq5A/CJepc7AJ9qjXIHAGC10Jjkx0kWLFiQHj16fOJx7WpGdNasWRkxYkSLfSNGjMiLL76YxYsXN+/baqutmv9cKpVSXV2defPmJUmeeuqpvPTSS+nevXvz+yV79eqVd999Ny+//HKb5dxqq62aS2iSDB8+fKljhg8f3mIxphEjRmThwoV57bXXPnYsSdKnT58WY1m4cGHWXnvt5rFUVlbmlVdeWaGxnHXWWVmwYEHzNnfu3FafCwAAWP2sUosVtZU11mj5e+FSqZQlS5Yk+fC22S984QuZMmXKUq/r3Xvl+33/Z42lT58+H7tab8+ePVt9zYqKihYzrAAAAMujXRXRQYMGZcaMGS32zZgxI5tuuukyrwI7bNiwXH/99Vl33XU/dSp5RQwaNCjXXHNN3n333eZZ0YceemipY2644YY0NTU1z4rOmDEj3bt3X+aPVhk2bFj+8pe/pFOnTqmpqWnTMQAAALRWu7o199RTT819992XCy64IC+88EJ+9atf5bLLLltqIaBPc9hhh2WdddbJ/vvvn+nTp+eVV17J1KlTc9JJJ7W4JXZFfP3rX0+pVMro0aPz3HPP5fbbb8/FF1/c4phvfetbmTt3bv71X/81f/zjH3PLLbfkvPPOyymnnJIOHZbt27bHHntk+PDhOeCAA3L33Xdn9uzZ+f3vf5+zzz47jz32WJuMBQAAYHm1qyI6bNiw/OY3v8l1112XIUOG5Nxzz83555+fUaNGLfM5unbtmgceeCADBgzIQQcdlEGDBuXoo4/Ou++++4kzpJMnT27xXs7PUllZmf/+7//OzJkzs8022+Tss8/ORRdd1OKYfv365fbbb88jjzySrbfeOscdd1yOPvrofO9731vm65RKpdx+++3Zeeedc+SRR2bTTTfNIYcckldffTXrrbfeMp8HAACgLbWrVXPL5bzzzsu0adM+9r2Yq6pPWzX3HzU0NKSqqsqquRTCqrkrr5XvXfT8X1bNBaAI7XLV3EmTJqWysjIzZ84sd5QW7rjjjvzwhz8sd4w2MX78+FRWVmbOnDnljgIAALRTq8yM6Ouvv55FixYlSQYMGJDOnTuXOVH79Oabb+bNN99M8uEqwVVVVZ/5GjOiFMmM6MrLjOjKzYwoAEVY1hnRVWbV3H79+pU7wmqhV69e6dWrV7ljAAAA7dgqdWsuAAAAqz5FFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFWmWKaG1tbUqlUkqlUurq6sodp82NHTs2Q4cOLXeM1NTUNH+d58+fX+44AABAO7TKFNEkGT16dOrr6zNkyJAkyezZs1MqlZqfnzx5cnr27Pm556ipqcnUqVOX+fipU6empqbmc8uzImprazN58uTmx48++mhuuOGG8gUCAADavU7lDrA8unbtmurq6nLHaNd69+6dXr16lTsGAADQjq1SM6KfZurUqTnyyCOzYMGC5ltLx44dm8suu6x5BjVJbr755pRKpfzsZz9r3rfHHnvke9/7XvPjyy+/PBtvvHE6d+6czTbbLNdcc02b5/3BD36Q9dZbL927d8/RRx+dd999t8XzS5Ysyfnnn5/1118/FRUVGTp0aO68887m5z+aDb7xxhuz6667pmvXrtl6663zhz/8ocV5Hnzwwey0007p0qVL+vfvn5NOOilvv/32CmVvbGxMQ0NDiw0AAGBZtZsiuuOOO2bixInp0aNH6uvrU19fn9NOOy277LJLnnvuufztb39LkkybNi3rrLNO862177//fv7whz+ktrY2SXLTTTfl5JNPzqmnnppnnnkmxx57bI488sjcf//9bZb1N7/5TcaOHZvx48fnscceS58+fTJp0qQWx1x66aW55JJLcvHFF+fpp5/OXnvtlf322y8vvvhii+POPvvsnHbaaamrq8umm26aQw89NB988EGS5OWXX87ee++df/7nf87TTz+d66+/Pg8++GBOPPHEFco/YcKEVFVVNW/9+/dfofMBAACrl1JTU1NTuUMsi9ra2gwdOjQTJ078xGMmT56cMWPGtFhkp6mpKb17987PfvazfPWrX80222yTgw8+OJdeemnq6+szY8aM7Lrrrpk/f366du2aESNGZPDgwbniiiuazzFy5Mi8/fbbue2229pkLDvuuGO22Wab/PSnP23et8MOO+Tdd99tXoipX79+OeGEE/Ld7363+ZjtttsuX/ziF/PTn/40s2fPzoYbbpgrr7wyRx99dJLkueeey+DBgzNr1qxsvvnmOeaYY9KxY8f8/Oc/bz7Hgw8+mF122SVvv/121lxzzY/NN3Xq1Oy66675+9///rHvuW1sbExjY2Pz44aGhvTv3z9dkpSWOhra1lfLHYBP1LvcAfhUa5Q7AACrhcYkP06yYMGC9OjR4xOPazczop+kVCpl5513ztSpUzN//vw899xz+da3vpXGxsb88Y9/zLRp0/LFL34xXbt2TZLMmjUrI0aMaHGOESNGZNasWW2WadasWdl+++1b7Bs+fHjznxsaGvLnP/95mXJstdVWzX/u06dPkmTevHlJkqeeeiqTJ09OZWVl87bXXntlyZIleeWVV1qdv6KiIj169GixAQAALKtVarGi1qqtrc0VV1yR6dOnZ5tttkmPHj2ay+m0adOyyy67lDtiq62xxv/+jvujFYSXLFmSJFm4cGGOPfbYnHTSSUu9bsCAAcUEBAAA+Aftaka0c+fOWbx48VL7P3qf6H/91381vxe0trY29957b2bMmNG8L0kGDRqUGTNmtHj9jBkzssUWW7RZzkGDBuXhhx9use+hhx5q/nOPHj3St2/fFc4xbNiwPPfccxk4cOBSW+fOnVdsEAAAAK3UrmZEa2pqsnDhwtx3333Zeuut07Vr13Tt2jVbbbVV1lprrVx77bW59dZbk3xYRE877bSUSqUWt8CefvrpGTlyZLbZZpvsscce+e///u/ceOONuffee9ss58knn5xRo0Zl2223zYgRIzJlypQ8++yz2WijjVrkOO+887Lxxhtn6NChueqqq1JXV5cpU6Ys83XOPPPM7LDDDjnxxBNzzDHHpFu3bnnuuedyzz335LLLLmuz8QAAACyPdjUjuuOOO+a4447LwQcfnN69e+eHP/xhkg9vWd1pp51SKpXypS99KcmH763s0aNHtt1223Tr1q35HAcccEAuvfTSXHzxxRk8eHB+/vOf56qrrmoxa/qPamtrM2rUqGXOefDBB+ecc87JGWeckS984Qt59dVXc/zxx7c45qSTTsopp5ySU089NVtuuWXuvPPO/O53v8smm2yyzNfZaqutMm3atLzwwgvZaaedss022+Tcc89N3759l/kcAAAAba1drZpbLhtssEHGjRu3XGV0ZfZZq+b+o4aGhlRVVVk1l0JYNXflZdXclZtVcwEoQrtcNXfSpEmprKzMzJkzyx2l2bPPPpuqqqp885vfLHeUNjF48ODss88+5Y4BAAC0Y6vMjOjrr7+eRYsWJflwxVeL7Xw+Xn311bz//vtJko022igdOnz27yrMiFIkM6IrLzOiKzczogAUYVlnRFeZxYr69etX7girhQ022KDcEQAAgHZulbo1FwAAgFWfIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQqLIW0dra2pRKpZRKpdTV1S3z6yZPnpyePXt+brmKVltbmzFjxpQ7RpJk7Nixzd+TiRMnljsOAADQDpV9RnT06NGpr6/PkCFDkiSzZ89OqVQqc6qPN2rUqIwdO3a5XlMqlTJ79uwkydSpU1MqlTJ//vw2z9ZakydPTm1tbfPj0047LfX19Vl//fXLFwoAAGjXOpU7QNeuXVNdXV3uGKuc999/P2ussUabn7eysjKVlZXp2LFjm58bAAAgWQlmRJfF5MmTM2DAgHTt2jUHHnhg/ud//mepYy6//PJsvPHG6dy5czbbbLNcc801LZ4vlUq58sorc+CBB6Zr167ZZJNN8rvf/a7FMc8880z22WefVFZWZr311svhhx+eN954o03GMHv27Oy6665JkrXWWiulUimjRo1qfn7JkiU544wz0qtXr1RXVy8181oqlXL55Zdnv/32S7du3fL9738/SXLLLbdk2LBhWXPNNbPRRhtl3Lhx+eCDD5pfN3/+/BxzzDHp3bt3evTokd122y1PPfVUm4wJAACgNVb6Ivrwww/n6KOPzoknnpi6urrsuuuuufDCC1scc9NNN+Xkk0/OqaeemmeeeSbHHntsjjzyyNx///0tjhs3blxGjhyZp59+Ol/+8pdz2GGH5c0330zyYWHbbbfdss022+Sxxx7LnXfemb/+9a8ZOXJkm4yjf//+ueGGG5Ikzz//fOrr63PppZc2P/+rX/0q3bp1y8MPP5wf/vCHOf/883PPPfe0OMfYsWNz4IEHZubMmTnqqKMyffr0fPOb38zJJ5+c5557Lj//+c8zefLk5pKaJF/72tcyb9683HHHHXn88cczbNiw7L777s3jbo3GxsY0NDS02AAAAJZVqampqalcF6+trc3QoUM/dVGcr3/961mwYEFuu+225n2HHHJI7rzzzub3Wo4YMSKDBw/OFVdc0XzMyJEj8/bbbze/rlQq5Xvf+14uuOCCJMnbb7+dysrK3HHHHdl7771z4YUXZvr06bnrrruaz/Haa6+lf//+ef7557Ppppuu8HinTp2aXXfdNX//+99bLLZUW1ubxYsXZ/r06c37tttuu+y22275wQ9+0Jx/zJgx+fGPf9x8zB577JHdd989Z511VvO+X//61znjjDPy5z//OQ8++GC+8pWvZN68eamoqGg+ZuDAgTnjjDPyL//yL5+YtaamJmPGjPnYRZTGjh2bcePGLbW/S5KV8929tCdfLXcAPlHvcgfgU7X9mzkAYGmNSX6cZMGCBenRo8cnHrfSz4jOmjUr22+/fYt9w4cPX+qYESNGtNg3YsSIzJo1q8W+rbbaqvnP3bp1S48ePTJv3rwkyVNPPZX777+/+T2SlZWV2XzzzZMkL7/8cpuN55P832xJ0qdPn+ZsH9l2221bPH7qqady/vnnt8j80eJP77zzTp566qksXLgwa6+9dotjXnnllRUa01lnnZUFCxY0b3Pnzm31uQAAgNVP2RcrKtI/Lu5TKpWyZMmSJMnChQuz77775qKLLlrqdX369Clrto9069atxeOFCxdm3LhxOeigg5Y635prrpmFCxemT58+mTp16lLPr8jH31RUVLSYYQUAAFgeK30RHTRoUB5++OEW+x566KGljpkxY0aOOOKI5n0zZszIFltssczXGTZsWG644YbU1NSkU6fP58vSuXPnJMnixYvb5HzDhg3L888/n4EDB37i83/5y1/SqVOn1NTUtMk1AQAAVtRKf2vuSSedlDvvvDMXX3xxXnzxxVx22WW58847Wxxz+umnZ/Lkybn88svz4osv5kc/+lFuvPHGnHbaact8nRNOOCFvvvlmDj300Dz66KN5+eWXc9ddd+XII49ss+K4wQYbpFQq5dZbb83f/va3LFy4cIXOd+655+bqq6/OuHHj8uyzz2bWrFm57rrr8r3vfS/Jh+8hHT58eA444IDcfffdmT17dn7/+9/n7LPPzmOPPdYWQwIAAFhuK30R3WGHHfKLX/wil156abbeeuvcfffdzUXrIwcccEAuvfTSXHzxxRk8eHB+/vOf56qrrkptbe0yX6dv376ZMWNGFi9enD333DNbbrllxowZk549e6ZDh4//Mo0dO3a5Zhr79euXcePG5Tvf+U7WW2+9nHjiicv82o+z11575dZbb83dd9+dL37xi9lhhx3y4x//OBtssEGSD2/vvf3227PzzjvnyCOPzKabbppDDjkkr776atZbb70VujYAAEBrrfSr5q7MjjjiiJRKpUyePLncUdrcp62a+48aGhpSVVVl1VwKYdXclZdVc1duVs0FoAirzKq5kyZNSmVlZWbOnFnuKMulqakpU6dObf44mPZi/PjxqayszJw5c8odBQAAaKfKOiP6+uuvZ9GiRUmSAQMGNC/mQ/m8+eabefPNN5MkvXv3TlVV1We+xowoRTIjuvIyI7pyMyMKQBGWdUa0rKvm9uvXr5yX52P06tUrvXr1KncMAACgHSv7rbkAAACsXhRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRqpS6itbW1KZVKKZVKqaur+8Tjbr755gwcODAdO3bMmDFjCsvXlmpqajJx4sSyZpg6dWrz1/uAAw4oaxYAAKD9WqmLaJKMHj069fX1GTJkSJJk9uzZKZVKLY459thj89WvfjVz587NBRdc8LnmmTp1ampqapbrNaNGjcrYsWM/lzwr4h+/ljvuuGPq6+szcuTIMqYCAADau07lDvBZunbtmurq6k98fuHChZk3b1722muv9O3b93PN8v7773+u5y+3zp07p7q6Ol26dEljY2O54wAAAO3USj8j+mmmTp2a7t27J0l22223lEqlTJ06NUlyww03ZPDgwamoqEhNTU0uueSSFq8tlUq5+eabW+zr2bNnJk+enOR/Zwuvv/767LLLLllzzTUzZcqUNsk9b9687LvvvunSpUs23HDDjz3vnDlzsv/++6eysjI9evTIyJEj89e//rX5+bFjx2bo0KG55pprUlNTk6qqqhxyyCF56623mo9ZsmRJJkyYkA033DBdunTJ1ltvnd/+9rdtMgYAAIDWWqWL6I477pjnn38+yYfFs76+PjvuuGMef/zxjBw5MoccckhmzpyZsWPH5pxzzmkumcvjO9/5Tk4++eTMmjUre+21V5vkHjVqVObOnZv7778/v/3tbzNp0qTMmzev+fklS5Zk//33z5tvvplp06blnnvuyZ/+9KccfPDBLc7z8ssv5+abb86tt96aW2+9NdOmTcsPfvCD5ucnTJiQq6++Oj/72c/y7LPP5tvf/na+8Y1vZNq0aSuUv7GxMQ0NDS02AACAZbXS35r7j2pqatLU1JTkw1tJ11133SRJr169mm/h/dGPfpTdd98955xzTpJk0003zXPPPZd/+7d/y6hRo5bremPGjMlBBx3U/LhPnz6ZPXv2cp3j/xbgF154IXfccUceeeSRfPGLX0yS/PKXv8ygQYOaj7nvvvsyc+bMvPLKK+nfv3+S5Oqrr87gwYPz6KOPNr9uyZIlmTx5cvOs8OGHH5777rsv3//+99PY2Jjx48fn3nvvzfDhw5MkG220UR588MH8/Oc/zy677NLia7k8JkyYkHHjxi336wAAAJJVfEb0k8yaNSsjRoxosW/EiBF58cUXs3jx4uU617bbbtuW0TJr1qx06tQpX/jCF5r3bb755unZs2eLY/r3799cQpNkiy22SM+ePTNr1qzmfTU1Nc0lNPmwJH80s/rSSy/lnXfeyf/7f/8vlZWVzdvVV1+dl19+eYXGcNZZZ2XBggXN29y5c1fofAAAwOpllZsRbSulUmmp2cCPW4yoW7duRUVabmussUaLx6VSKUuWLEny4SJOSXLbbbelX79+LY6rqKhYoetWVFSs8DkAAIDVV7ssooMGDcqMGTNa7JsxY0Y23XTTdOzYMUnSu3fv1NfXNz//4osv5p133vncs22++eb54IMP8vjjjzffYvv8889n/vz5LfLPnTs3c+fObZ4Vfe655zJ//vxsscUWy3SdLbbYIhUVFZkzZ0522WWXNh8HAABAa7XLInrqqafmi1/8Yi644IIcfPDB+cMf/pDLLrsskyZNaj5mt912y2WXXZbhw4dn8eLFOfPMM5eaYfw8bLbZZtl7771z7LHH5vLLL0+nTp0yZsyYdOnSpfmYPfbYI1tuuWUOO+ywTJw4MR988EG+9a1vZZdddlnmW4W7d++e0047Ld/+9rezZMmSfOlLX8qCBQsyY8aM9OjRI0ccccTnNUQAAIBP1S7fIzps2LD85je/yXXXXZchQ4bk3HPPzfnnn99ioaJLLrkk/fv3z0477ZSvf/3rOe2009K1a9flvtZHH/Py0cfGLIurrroqffv2zS677JKDDjoo//Iv/9K86FLy4S22t9xyS9Zaa63svPPO2WOPPbLRRhvl+uuvX65sF1xwQc4555xMmDAhgwYNyt57753bbrstG2644XKdBwAAoC2VmlqzbGpBamtrM3To0EycOLHcUT7R/fffn4MOOih/+tOfstZaa5U7TpsYNWpU5s+fv9TnrH6ShoaGVFVVpUuS0ueaDJKvljsAn6h3uQPwqT7/e34AIGlM8uMkCxYsSI8ePT7xuJV+RnTSpEmprKzMzJkzyx3lY91+++357ne/2y5K6PTp01NZWZkpU6aUOwoAANCOrdQzoq+//noWLVqUJBkwYEA6d+5c5kTt26JFi/L6668nSSorK5s/l/WzmBGlSGZEV15mRFduZkQBKMKyzoiu1IsV/ePHjvD56tKlSwYOHFjuGAAAQDu30t+aCwAAQPuiiAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUKtMEa2trU2pVEqpVEpdXd0nHnfzzTdn4MCB6dixY8aMGZPJkyenZ8+eheVsralTp6ZUKmX+/PllzTFq1Kjmr/PNN99c1iwAAED7tMoU0SQZPXp06uvrM2TIkCTJ7NmzUyqVWhxz7LHH5qtf/Wrmzp2bCy64IAcffHBeeOGFNs0xatSojB07drleUyqVMnv27DbN0RbGjh2bUaNGNT++9NJLU19fX75AAABAu9ep3AGWR9euXVNdXf2Jzy9cuDDz5s3LXnvtlb59+zbv79KlSxHx2oWqqqpUVVWVOwYAANCOrVIzop9m6tSp6d69e5Jkt912S6lUytSpU1vcmvvCCy+kVCrlj3/8Y4vX/vjHP87GG2/c/PiZZ57JPvvsk8rKyqy33no5/PDD88Ybb7Rp3ttvvz2bbrppunTpkl133fVjZ0tvuOGGDB48OBUVFampqckll1zS4vmampqMHz8+Rx11VLp3754BAwbkiiuuaHHM3LlzM3LkyPTs2TO9evXK/vvvv8Izs42NjWloaGixAQAALKt2U0R33HHHPP/880k+LHD19fXZcccdWxyz6aabZtttt82UKVNa7J8yZUq+/vWvJ0nmz5+f3XbbLdtss00ee+yx3HnnnfnrX/+akSNHtlnWuXPn5qCDDsq+++6burq6HHPMMfnOd77T4pjHH388I0eOzCGHHJKZM2dm7NixOeecczJ58uQWx11yySXZdttt8+STT+Zb3/pWjj/++Oavw/vvv5+99tor3bt3z/Tp0zNjxoxUVlZm7733znvvvdfq/BMmTGieOa2qqkr//v1bfS4AAGD1U2pqamoqd4hlUVtbm6FDh2bixImfeMz8+fOz1lpr5f77709tbW2SZPLkyRkzZkzzIkATJ07MZZddlpdeeinJh7Okm222WWbNmpXNN988F154YaZPn5677rqr+byvvfZa+vfvn+effz6bbrrpCo/lu9/9bm655ZY8++yzzfu+853v5KKLLsrf//739OzZM4cddlj+9re/5e67724+5owzzshtt93W/LqamprstNNOueaaa5IkTU1Nqa6uzrhx43Lcccfl17/+dS688MLMmjWr+b207733Xnr27Jmbb745e+655ydmLJVKuemmm3LAAQcs9VxjY2MaGxubHzc0NKR///7pkqS01NHQtr5a7gB8ot7lDsCnWqPcAQBYLTQm+XGSBQsWpEePHp94XLuZEV1WhxxySGbPnp2HHnooyYezocOGDcvmm2+eJHnqqady//33p7Kysnn76LmXX365TTLMmjUr22+/fYt9w4cPX+qYESNGtNg3YsSIvPjii1m8eHHzvq222qr5z6VSKdXV1Zk3b17zWF566aV07969eSy9evXKu+++u0JjqaioSI8ePVpsAAAAy2qVWqyoLVRXV2e33XbLtddemx122CHXXnttjj/++ObnFy5cmH333TcXXXTRUq/t06dPkVGXyRprtPwdd6lUypIlS5J8OJYvfOELS92KnCS9e5u7AAAAymO1K6JJcthhh+WMM87IoYcemj/96U855JBDmp8bNmxYbrjhhtTU1KRTp8/nyzNo0KD87ne/a7Hvoxna/3vMjBkzWuybMWNGNt1003Ts2HGZrjNs2LBcf/31WXfddc1aAgAAK43V7tbcJDnooIPy1ltv5fjjj8+uu+7a4qNeTjjhhLz55ps59NBD8+ijj+bll1/OXXfdlSOPPLLFLbEr4rjjjsuLL76Y008/Pc8//3yuvfbapRYhOvXUU3PfffflggsuyAsvvJBf/epXueyyy3Laaact83UOO+ywrLPOOtl///0zffr0vPLKK5k6dWpOOumkvPbaa20yFgAAgOW1WhbR7t27Z999981TTz2Vww47rMVzffv2zYwZM7J48eLsueee2XLLLTNmzJj07NkzHTp8/Jdr7NixqampWebrDxgwIDfccENuvvnmbL311vnZz36W8ePHtzhm2LBh+c1vfpPrrrsuQ4YMybnnnpvzzz8/o0aNWubrdO3aNQ888EAGDBiQgw46KIMGDcrRRx+dd9991wwpAABQNu1q1dxyOeKII1IqlZaa1VyVfdqquf+ooaEhVVVVVs2lEFbNXXl55/nKzaq5ABShXa6aO2nSpFRWVmbmzJnljtKsqakpU6dOzQUXXFDuKG3iuOOOS2VlZbljAAAA7dgqMyP6+uuvZ9GiRUk+vLW1c+fOZU7UPs2bNy8NDQ1JPlwluFu3bp/5GjOiFMmM6MrLjOjKzYwoAEVY1hnRVWbV3H79+pU7wmph3XXXzbrrrlvuGAAAQDu2St2aCwAAwKpPEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAo1CpfRGtra1MqlVIqlVJXV7fMr5s8eXJ69uz5ueUqh9mzZy/31+EfffS1bG9fGwAAYOWxyhfRJBk9enTq6+szZMiQJP9byFZGo0aNytixY5frNaVSKbNnz/7M4/r379/i67AsampqMnXq1ObH9fX1mThx4nLlAwAAWB6dyh2gLXTt2jXV1dXljlF2HTt2XOGvQ3V1daqqqtooEQAAwNLaxYzospg8eXIGDBiQrl275sADD8z//M//LHXM5Zdfno033jidO3fOZpttlmuuuabF86VSKVdeeWUOPPDAdO3aNZtsskl+97vftTjmmWeeyT777JPKysqst956Ofzww/PGG2+02Tj+/ve/57DDDkvv3r3TpUuXbLLJJrnqqquSLH1r7vnnn5++ffu2GOtXvvKV7LrrrlmyZEmbZQIAAFgeq0URffjhh3P00UfnxBNPTF1dXXbddddceOGFLY656aabcvLJJ+fUU0/NM888k2OPPTZHHnlk7r///hbHjRs3LiNHjszTTz+dL3/5yznssMPy5ptvJknmz5+f3XbbLdtss00ee+yx3HnnnfnrX/+akSNHttlYzjnnnDz33HO54447MmvWrFx++eVZZ511PvbYs88+OzU1NTnmmGOSJD/96U/z+9//Pr/61a/SoUPrv/WNjY1paGhosQEAACyrUlNTU1O5Q6yI2traDB069FPf1/j1r389CxYsyG233da875BDDsmdd96Z+fPnJ0lGjBiRwYMH54orrmg+ZuTIkXn77bebX1cqlfK9730vF1xwQZLk7bffTmVlZe64447svffeufDCCzN9+vTcddddzed47bXX0r9//zz//PPZdNNNV3i8++23X9ZZZ538x3/8x1LPzZ49OxtuuGGefPLJDB06NEnypz/9KUOHDs23vvWt/OQnP8mVV16Zr3/96596jcmTJ2fMmDHNX5t/NHbs2IwbN26p/V2SrJzvzKU9+Wq5A/CJepc7AJ9qjXIHAGC10Jjkx0kWLFiQHj16fOJxq8WM6KxZs7L99tu32Dd8+PCljhkxYkSLfSNGjMisWbNa7Ntqq62a/9ytW7f06NEj8+bNS5I89dRTuf/++1NZWdm8bb755kmSl19+uU3Gcvzxx+e6667L0KFDc8YZZ+T3v//9px6/0UYb5eKLL85FF12U/fbb7zNL6LI466yzsmDBguZt7ty5K3xOAABg9dEuFisq0hprtPydcqlUan6/5cKFC7PvvvvmoosuWup1ffr0aZPr77PPPnn11Vdz++2355577snuu++eE044IRdffPEnvuaBBx5Ix44dM3v27HzwwQfp1GnFvu0VFRWpqKhYoXMAAACrr9ViRnTQoEF5+OGHW+x76KGHljpmxowZLfbNmDEjW2yxxTJfZ9iwYXn22WdTU1OTgQMHtti6devW+gH8g969e+eII47Ir3/960ycOLHF7cT/6Prrr8+NN96YqVOnZs6cOc23FQMAAJTLalFETzrppNx55525+OKL8+KLL+ayyy7LnXfe2eKY008/PZMnT87ll1+eF198MT/60Y9y44035rTTTlvm65xwwgl58803c+ihh+bRRx/Nyy+/nLvuuitHHnlkFi9e3CZjOffcc3PLLbfkpZdeyrPPPptbb701gwYN+thjX3vttRx//PG56KKL8qUvfSlXXXVVxo8fv1QJBwAAKNJqUUR32GGH/OIXv8ill16arbfeOnfffXe+973vtTjmgAMOyKWXXpqLL744gwcPzs9//vNcddVVqa2tXebr9O3bNzNmzMjixYuz5557Zsstt8yYMWPSs2fPT1ylduzYsampqVnma3Tu3DlnnXVWttpqq+y8887p2LFjrrvuuqWOa2pqyqhRo7LddtvlxBNPTJLstddeOf744/ONb3wjCxcuXOZrAgAAtKXVYtXcldkRRxyRUqmUyZMnlztKs89aNfcfNTQ0pKqqyqq5FMKquSsvq+au3KyaC0ARlnXV3HaxWNGkSZNy5ZVX5g9/+EO23HLLcsdZZk1NTZk6dWoefPDBckdpVllZmQ8++CBrrrlmuaMAAADt1CpfRKdMmZJFixYlSQYMGFDmNMunVCrl1VdfLXeMFurq6pIkHTt2LG8QAACg3Vrli2i/fv3KHaFdGThwYLkjAAAA7dxqsVgRAAAAKw9FFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoTqVOwCrvqampg//t8w5WD28V+4AfKLGcgfgUy0pdwAAVgsf/TzwUUf4JIooK+ytt95Kkrxb5hysHq4rdwAAAD7TW2+9laqqqk98vtT0WVUVPsOSJUvy5z//Od27d0+pVPrcrtPQ0JD+/ftn7ty56dGjx+d2nSK0p7EkxrMya09jSYxnZdaexpIYz8qsPY0lMZ6VWXsaS1LceJqamvLWW2+lb9++6dDhk98JakaUFdahQ4esv/76hV2vR48e7eI/Bkn7GktiPCuz9jSWxHhWZu1pLInxrMza01gS41mZtaexJMWM59NmQj9isSIAAAAKpYgCAABQKEWUVUZFRUXOO++8VFRUlDvKCmtPY0mMZ2XWnsaSGM/KrD2NJTGelVl7GktiPCuz9jSWZOUbj8WKAAAAKJQZUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShFllfDTn/40NTU1WXPNNbP99tvnkUceKXekVnvggQey7777pm/fvimVSrn55pvLHanVJkyYkC9+8Yvp3r171l133RxwwAF5/vnnyx2rVS6//PJstdVWzR/yPHz48Nxxxx3ljtVmfvCDH6RUKmXMmDHljtIqY8eOTalUarFtvvnm5Y7Vaq+//nq+8Y1vZO21106XLl2y5ZZb5rHHHit3rFapqalZ6ntTKpVywgknlDtaqyxevDjnnHNONtxww3Tp0iUbb7xxLrjggqyqazu+9dZbGTNmTDbYYIN06dIlO+64Yx599NFyx1omn/XvZVNTU84999z06dMnXbp0yR577JEXX3yxPGGXwWeN58Ybb8yee+6ZtddeO6VSKXV1dWXJuSw+bSzvv/9+zjzzzGy55Zbp1q1b+vbtm29+85v585//XL7An+Gzvjdjx47N5ptvnm7dumWttdbKHnvskYcffrg8YZfB8vysedxxx6VUKmXixImF5fuIIspK7/rrr88pp5yS8847L0888US23nrr7LXXXpk3b165o7XK22+/na233jo//elPyx1lhU2bNi0nnHBCHnroodxzzz15//33s+eee+btt98ud7Tltv766+cHP/hBHn/88Tz22GPZbbfdsv/+++fZZ58td7QV9uijj+bnP/95ttpqq3JHWSGDBw9OfX198/bggw+WO1Kr/P3vf8+IESOyxhpr5I477shzzz2XSy65JGuttVa5o7XKo48+2uL7cs899yRJvva1r5U5WetcdNFFufzyy3PZZZdl1qxZueiii/LDH/4w//7v/17uaK1yzDHH5J577sk111yTmTNnZs8998wee+yR119/vdzRPtNn/Xv5wx/+MD/5yU/ys5/9LA8//HC6deuWvfbaK++++27BSZfNZ43n7bffzpe+9KVcdNFFBSdbfp82lnfeeSdPPPFEzjnnnDzxxBO58cYb8/zzz2e//fYrQ9Jl81nfm0033TSXXXZZZs6cmQcffDA1NTXZc88987e//a3gpMtmWX/WvOmmm/LQQw+lb9++BSX7B02wkttuu+2aTjjhhObHixcvburbt2/ThAkTypiqbSRpuummm8odo83MmzevKUnTtGnTyh2lTay11lpNV155ZbljrJC33nqraZNNNmm65557mnbZZZemk08+udyRWuW8885r2nrrrcsdo02ceeaZTV/60pfKHeNzc/LJJzdtvPHGTUuWLCl3lFb5yle+0nTUUUe12HfQQQc1HXbYYWVK1HrvvPNOU8eOHZtuvfXWFvuHDRvWdPbZZ5cpVev847+XS5Ysaaqurm76t3/7t+Z98+fPb6qoqGj6z//8zzIkXD6f9u//K6+80pSk6cknnyw0U2sty88yjzzySFOSpldffbWYUCtgWcazYMGCpiRN9957bzGhVsAnjee1115r6tevX9MzzzzTtMEGGzT9+Mc/LjybGVFWau+9914ef/zx7LHHHs37OnTokD322CN/+MMfypiMj7NgwYIkSa9evcqcZMUsXrw41113Xd5+++0MHz683HFWyAknnJCvfOUrLf4/tKp68cUX07dv32y00UY57LDDMmfOnHJHapXf/e532XbbbfO1r30t6667brbZZpv84he/KHesNvHee+/l17/+dY466qiUSqVyx2mVHXfcMffdd19eeOGFJMlTTz2VBx98MPvss0+Zky2/Dz74IIsXL86aa67ZYn+XLl1W2TsKPvLKK6/kL3/5S4v/tlVVVWX77bf388FKaMGCBSmVSunZs2e5o6yw9957L1dccUWqqqqy9dZblztOqyxZsiSHH354Tj/99AwePLhsOTqV7cqwDN54440sXrw46623Xov96623Xv74xz+WKRUfZ8mSJRkzZkxGjBiRIUOGlDtOq8ycOTPDhw/Pu+++m8rKytx0003ZYostyh2r1a677ro88cQTq8z7wT7N9ttvn8mTJ2ezzTZLfX19xo0bl5122inPPPNMunfvXu54y+VPf/pTLr/88pxyyin57ne/m0cffTQnnXRSOnfunCOOOKLc8VbIzTffnPnz52fUqFHljtJq3/nOd9LQ0JDNN988HTt2zOLFi/P9738/hx12WLmjLbfu3btn+PDhueCCCzJo0KCst956+c///M/84Q9/yMCBA8sdb4X85S9/SZKP/fngo+dYObz77rs588wzc+ihh6ZHjx7ljtNqt956aw455JC888476dOnT+65556ss8465Y7VKhdddFE6deqUk046qaw5FFGgTZxwwgl55plnVunfsm+22Wapq6vLggUL8tvf/jZHHHFEpk2btkqW0blz5+bkk0/OPffcs9RsyKro/85GbbXVVtl+++2zwQYb5De/+U2OPvroMiZbfkuWLMm2226b8ePHJ0m22WabPPPMM/nZz362yhfRX/7yl9lnn33K936jNvCb3/wmU6ZMybXXXpvBgwenrq4uY8aMSd++fVfJ788111yTo446Kv369UvHjh0zbNiwHHrooXn88cfLHY3VwPvvv5+RI0emqakpl19+ebnjrJBdd901dXV1eeONN/KLX/wiI0eOzMMPP5x111233NGWy+OPP55LL700TzzxRNnvXHFrLiu1ddZZJx07dsxf//rXFvv/+te/prq6ukyp+Ecnnnhibr311tx///1Zf/31yx2n1Tp37pyBAwfmC1/4QiZMmJCtt946l156abljtcrjjz+eefPmZdiwYenUqVM6deqUadOm5Sc/+Uk6deqUxYsXlzviCunZs2c23XTTvPTSS+WOstz69Omz1C83Bg0atMreavyRV199Nffee2+OOeaYckdZIaeffnq+853v5JBDDsmWW26Zww8/PN/+9rczYcKEckdrlY033jjTpk3LwoULM3fu3DzyyCN5//33s9FGG5U72gr56GcAPx+svD4qoa+++mruueeeVXo2NEm6deuWgQMHZocddsgvf/nLdOrUKb/85S/LHWu5TZ8+PfPmzcuAAQOafz549dVXc+qpp6ampqbQLIooK7XOnTvnC1/4Qu67777mfUuWLMl99923yr93rz1oamrKiSeemJtuuin/3//3/2XDDTcsd6Q2tWTJkjQ2NpY7RqvsvvvumTlzZurq6pq3bbfdNocddljq6urSsWPHckdcIQsXLszLL7+cPn36lDvKchsxYsRSH3P0wgsvZIMNNihTorZx1VVXZd11181XvvKVckdZIe+88046dGj541HHjh2zZMmSMiVqG926dUufPn3y97//PXfddVf233//ckdaIRtuuGGqq6tb/HzQ0NCQhx9+2M8HK4GPSuiLL76Ye++9N2uvvXa5I7W5VfVnhMMPPzxPP/10i58P+vbtm9NPPz133XVXoVncmstK75RTTskRRxyRbbfdNtttt10mTpyYt99+O0ceeWS5o7XKwoULW8zivPLKK6mrq0uvXr0yYMCAMiZbfieccEKuvfba3HLLLenevXvz+3KqqqrSpUuXMqdbPmeddVb22WefDBgwIG+99VauvfbaTJ06tfD/KLeV7t27L/Ve3W7dumXttddeJd/De9ppp2XffffNBhtskD//+c8577zz0rFjxxx66KHljrbcvv3tb2fHHXfM+PHjM3LkyDzyyCO54oorcsUVV5Q7WqstWbIkV111VY444oh06rRq/2ix77775vvf/34GDBiQwYMH58knn8yPfvSjHHXUUeWO1ip33XVXmpqastlmm+Wll17K6aefns0333yV+Df0s/69HDNmTC688MJssskm2XDDDXPOOeekb9++OeCAA8oX+lN81njefPPNzJkzp/nzNj/6hVV1dfVKN8v7aWPp06dPvvrVr+aJJ57IrbfemsWLFzf/fNCrV6907ty5XLE/0aeNZ+211873v//97LfffunTp0/eeOON/PSnP83rr7++0n5M1Wf9XfvHXwysscYaqa6uzmabbVZs0MLX6YVW+Pd///emAQMGNHXu3Llpu+22a3rooYfKHanV7r///qYkS21HHHFEuaMtt48bR5Kmq666qtzRlttRRx3VtMEGGzR17ty5qXfv3k2777570913313uWG1qVf74loMPPripT58+TZ07d27q169f08EHH9z00ksvlTtWq/33f/9305AhQ5oqKiqaNt9886Yrrrii3JFWyF133dWUpOn5558vd5QV1tDQ0HTyySc3DRgwoGnNNdds2mijjZrOPvvspsbGxnJHa5Xrr7++aaONNmrq3LlzU3V1ddMJJ5zQNH/+/HLHWiaf9e/lkiVLms4555ym9dZbr6mioqJp9913X6n/Dn7WeK666qqPff68884ra+6P82lj+ejjZz5uu//++8sd/WN92ngWLVrUdOCBBzb17du3qXPnzk19+vRp2m+//ZoeeeSRcsf+RMv7s2a5Pr6l1NTU1NT29RYAAAA+nveIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAD4VKNGjcoBBxxQ7hgAtCOKKAAAAIVSRAGAJMlvf/vbbLnllunSpUvWXnvt7LHHHjn99NPzq1/9KrfccktKpVJKpVKmTp2aJJk7d25GjhyZnj17plevXtl///0ze/bs5vN9NJM6bty49O7dOz169Mhxxx2X995771Ov+fbbbxc8cgCK1qncAQCA8quvr8+hhx6aH/7whznwwAPz1ltvZfr06fnmN7+ZOXPmpKGhIVdddVWSpFevXnn//fez1157Zfjw4Zk+fXo6deqUCy+8MHvvvXeefvrpdO7cOUly3333Zc0118zUqVMze/bsHHnkkVl77bXz/e9//xOv2dTUVM4vBQAFUEQBgNTX1+eDDz7IQQcdlA022CBJsuWWWyZJunTpksbGxlRXVzcf/+tf/zpLlizJlVdemVKplCS56qqr0rNnz0ydOjV77rlnkqRz5875j//4j3Tt2jWDBw/O+eefn9NPPz0XXHDBp14TgPbNrbkAQLbeeuvsvvvu2XLLLfO1r30tv/jFL/L3v//9E49/6qmn8tJLL6V79+6prKxMZWVlevXqlXfffTcvv/xyi/N27dq1+fHw4cOzcOHCzJ07d7mvCUD7oYgCAOnYsWPuueee3HHHHdliiy3y7//+79lss83yyiuvfOzxCxcuzBe+8IXU1dW12F544YV8/etf/1yuCUD7oYgCAEmSUqmUESNGZNy4cXnyySfTuXPn3HTTTencuXMWL17c4thhw4blxRdfzLrrrpuBAwe22KqqqpqPe+qpp7Jo0aLmxw899FAqKyvTv3//T70mAO2bIgoA5OGHH8748ePz2GOPZc6cObnxxhvzt7/9LYMGDUpNTU2efvrpPP/883njjTfy/vvv57DDDss666yT/fffP9OnT88rr7ySqVOn5qSTTsprr73WfN733nsvRx99dJ577rncfvvtOe+883LiiSemQ4cOn3pNANo3ixUBAOnRo0ceeOCBTJw4MQ0NDdlggw1yySWXZJ999sm2226bqVOnZtttt83ChQtz//33p7a2Ng888EDOPPPMHHTQQXnrrbfSr1+/7L777unRo0fzeXffffdssskm2XnnndPY2JhDDz00Y8eO/cxrAtC+lZqskQ4AfA5GjRqV+fPn5+abby53FABWMm7NBQAAoFCKKAAAAIVyay4AAACFMiMKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAo1P8PTzTEnNuTcncAAAAASUVORK5CYII=",
"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": "86f1d225-12fd-4dc9-87d0-e3e6ca571655",
"metadata": {},
"source": [
"Naive DTMC evolution is also available under stormvogel.extensions.visual_algos."
]
},
{
"cell_type": "code",
"execution_count": 8,
"id": "570fa473-9954-415e-8e1d-3fd203ca05de",
"metadata": {
"execution": {
"iopub.execute_input": "2025-07-21T08:28:55.322246Z",
"iopub.status.busy": "2025-07-21T08:28:55.321861Z",
"iopub.status.idle": "2025-07-21T08:28:55.325722Z",
"shell.execute_reply": "2025-07-21T08:28:55.325227Z"
}
},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 8,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"res4 = extensions.dtmc_evolution(stormvogel_dtmc, 15)\n",
"res3 == res4"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "0f3f33f6-3bb3-408e-b24a-57c3b3775d0e",
"metadata": {},
"outputs": [],
"source": []
}
],
"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": {
"0076d5939680468bb158b6c9ec183b58": {
"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
}
},
"01e0ceb661b146d696a7a351753317ce": {
"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_7a5798a20ba04d8bbe883c46bc0d20f2",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"0a1dba882c7847409f3f6a7a311cae58": {
"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
}
},
"18e78c834d954e4e928199fc530b3491": {
"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_ed66384bc2404103bafc6d41b2923d10",
"msg_id": "",
"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"
}
],
"tabbable": null,
"tooltip": null
}
},
"1929d443d89249178d6ae12b07724082": {
"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_0a1dba882c7847409f3f6a7a311cae58",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"1dbc3ca8de0c4d1287ecb3125b1206d1": {
"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
}
},
"1e3b5d3d9eaf4476a644bd2aa6262d12": {
"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
}
},
"25d20b9ae69541d0a384df9093f1a30a": {
"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
}
},
"2937d22fd1e34a138ee18714fabc29ac": {
"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
}
},
"2a58f62e1898456f807d22883c2c5a91": {
"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_1dbc3ca8de0c4d1287ecb3125b1206d1",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"2b02307b3bb74f59bf23f3ee29206d40": {
"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_0076d5939680468bb158b6c9ec183b58",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"477bb236c1924f1ab54d0f4205962b7d": {
"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
}
},
"5c49a23aca9243e7a4d9615a01d7cc5a": {
"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_e014757a9f6a4966b15ca391f601d636",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"5d4697e570a148529a3567f54c263b30": {
"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
}
},
"5f7b21abb1e04413a5cddd5fc5d3c83f": {
"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_477bb236c1924f1ab54d0f4205962b7d",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"6d2331db9fc8493db7df26f99b99e5f8": {
"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_bc448f8bbca644e88bf74f767e20a2cd",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"7a5798a20ba04d8bbe883c46bc0d20f2": {
"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
}
},
"8778d4a1a7984db1b5057872aa3f20b0": {
"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_5d4697e570a148529a3567f54c263b30",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"8809e619630645a4a7c0239a9618639d": {
"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_1e3b5d3d9eaf4476a644bd2aa6262d12",
"msg_id": "",
"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"
}
],
"tabbable": null,
"tooltip": null
}
},
"98ac9d34d6b54e40b7fc082652072e72": {
"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_e6ffdb7e4b4e4d44a012c9cac19c1055",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"a02378d172c649eaa7a2a170d44e8061": {
"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_25d20b9ae69541d0a384df9093f1a30a",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"bc448f8bbca644e88bf74f767e20a2cd": {
"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
}
},
"cc52c8617d29479195293d6e27762cb6": {
"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
}
},
"cf995c76f3ae41b0b81e8f2f5c311328": {
"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_2937d22fd1e34a138ee18714fabc29ac",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"e014757a9f6a4966b15ca391f601d636": {
"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
}
},
"e6ffdb7e4b4e4d44a012c9cac19c1055": {
"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
}
},
"ec33151a2b5b4510a4bd72c649125b3b": {
"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_cc52c8617d29479195293d6e27762cb6",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"ed66384bc2404103bafc6d41b2923d10": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}