{
"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-04-24T14:31:52.009859Z",
"iopub.status.busy": "2025-04-24T14:31:52.009439Z",
"iopub.status.idle": "2025-04-24T14:31:52.680237Z",
"shell.execute_reply": "2025-04-24T14:31:52.679744Z"
}
},
"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-04-24T14:31:52.683042Z",
"iopub.status.busy": "2025-04-24T14:31:52.682540Z",
"iopub.status.idle": "2025-04-24T14:31:54.743161Z",
"shell.execute_reply": "2025-04-24T14:31:54.742565Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "148e81f1bc1e4bf48b002f5524939039",
"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": [
"return_id_result('http://127.0.0.1:8889', 'phmcXwgpxaJuvapfZODs', 'test message')"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Test request failed. See 'Communication server remark' in docs. Disable warning by use_server=False.\n"
]
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "2590b013567b495f96f95e330a937769",
"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"
],
"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-04-24T14:31:54.778814Z",
"iopub.status.busy": "2025-04-24T14:31:54.778590Z",
"iopub.status.idle": "2025-04-24T14:31:54.915951Z",
"shell.execute_reply": "2025-04-24T14:31:54.915455Z"
}
},
"outputs": [
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAAA5cAAAFUCAYAAACwdsjWAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjkuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8hTgPZAAAACXBIWXMAAA9hAAAPYQGoP6dpAAAzmUlEQVR4nO3deXwU9eH/8fcmMRe5CFcSIFkOReQUU06rwSCICAYUAancVBQqgS8KqEC4RFQoCIIFLVEEURGwRZFLzlq5A0EUEAmkEIqIJIQjQDK/P/yxdeXIMbuZZHk9H499yMzOzrw/hJh95zMzazMMwxAAAAAAACZ4WR0AAAAAAFD6US4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKb5WB0AJVNeXp6OHz+u4OBg2Ww2q+MAAAAAsIhhGDp79qyioqLk5XXj+UnKJa7r+PHjqlq1qtUxAAAAAJQQ6enpqlKlyg2fp1ziuoKDgyVJ/pI8cd5yrdUB3KxOc6sTuNF9Vgdwo9utDuBmkVYHcKNQqwO4UaDVAdzsNqsDuJG31QHcjIu7gGKTlS1Vved/HeFGKJe4rqunwtrkmeUyyOoAbhbiyd/Z/lYHcCNPfxNfxuoAbuTJ/1Px5K+bRLkszSiXQLHL73I5vi0BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLt0kLi5ONptNNptNKSkp1zyfnJyssLCwQu8zMTGxUK9JTk525CjsawEAAACgoCiXbtS/f39lZGSobt26SktLk81mczzXpUsXHThwoFD7W7JkicaPH+9YttvtmjZtmtM269evl91udzpORkaGmjVrVqQxAAAAAEBB+FgdwJMFBgYqIiLius8FBAQoICCgUPsLDw8vdIarx/H19S30awEAAACgoJi5tMjvT4tNSkpSw4YNNX/+fNntdoWGhqpr1646e/asY5vfnhYbFxenI0eOaMiQIY7TXgEAAADAKpTLEuTQoUNatmyZli9fruXLl2vDhg169dVXr7vtkiVLVKVKFY0bN04ZGRnKyMgo5rQAAAAA8D+cFltM7Ha7DMO46TZ5eXlKTk5WcHCwJOmpp57S2rVrNXHixGu2DQ8Pl7e3t4KDg51OvY2Li1NaWlqh8+Xk5CgnJ8exnJWVVeh9AAAAALh1MXNZgtjtdkexlKTIyEidPHmyWI49adIkhYaGOh5Vq1YtluMCAAAA8AyUyxLktttuc1q22WzKy8srlmOPHDlSmZmZjkd6enqxHBcAAACAZ+C02FLM19dXubm5LtmXn5+f/Pz8XLIvAAAAALceZi5LMbvdro0bN+rYsWM6deqU1XEAAAAA3MIol6XYuHHjlJaWpho1aqhChQpWxwEAAABwC7MZ+d3CFEUSFxenhg0batq0aVZHkVT4PFlZWQoNDVWAJE/8BM1vrA7gZvXuszqBGz1gdQA3qmV1ADeLsjqAG4VZHcCNylgdwM1uy3+TUsvb6gBuxhQJUGyyzkqhtaTMzEyFhITccDu+Ld1o1qxZCgoKUmpqqmUZFixYoKCgIG3atMmyDAAAAAA8Hzf0cZMFCxbowoULkqTo6GjLcnTo0EFNmjSRJIWFhVmWAwAAAIBno1y6SeXKla2OIEkKDg52+uxMAAAAAHAHTosFAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACY5mN1AJRsJzIzFRISYnUMN3jX6gBu9i+rA7jRfqsDuNEJqwO42SmrA7jRRasDuI9xyeoE7pVrdQA3yrM6gJt58tfOk8fm6Tz1+66A/yaZuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5BAAAAACYRrkEAAAAAJhGuQQAAAAAmEa5dJO4uDjZbDbZbDalpKRcd5tly5apZs2a8vb2VmJiYoH226tXLyUkJDgd52avtdvtjhxnzpwpcH4AAAAAKAzKpRv1799fGRkZqlu3rtLS0mSz2Zyef/rpp/X4448rPT1d48ePd8kx4+LilJyc7Fjetm2bPv30U5fsGwAAAABuxMfqAJ4sMDBQERER130uOztbJ0+eVJs2bRQVFeW2DBUqVFB4eLjb9g8AAAAAEjOXlli/fr2Cg4MlSQ888IBsNpvWr1+vpKQkNWzY0GnbadOmyW63F39IAAAAACgEyqUFmjdvrv3790uSPv30U2VkZKh58+aWZsrJyVFWVpbTAwAAAAAKitNii4ndbpdhGJIkX19fVaxYUZIUHh5+w1Nni2L9+vVFet2kSZM0duxYl+UAAAAAcGth5hKSpJEjRyozM9PxSE9PtzoSAAAAgFKEmcsSxMvLyzG7edXly5eL5dh+fn7y8/MrlmMBAAAA8DzMXJYgFSpU0IkTJ5wK5o0+IxMAAAAAShLKZQkSFxenn376Sa+99poOHTqkt956SytWrLA6FgAAAADki3JZgtSuXVuzZs3SW2+9pQYNGmjr1q0aNmyY1bEAAAAAIF9cc2mRsLCwa66vlKQBAwZowIABTutefPFFx5+Tk5Odnivq3WEBAAAAwJWYuXSjWbNmKSgoSKmpqZZlqFOnjtq2bWvZ8QEAAADcGpi5dJMFCxbowoULkqTo6GjLcnzxxReOO86GhIRYlgMAAACAZ6NcuknlypWtjiBJiomJsToCAAAAgFsAp8UCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABM87E6AEq2iNBQ2awO4QavWB3AzQZ78q+NOlodwI0aWR3AzexWB3CjcKsDuFGw1QHczN/qAG7kbXUAN/Pkn3We/rVD6ZNdsM08+dsSAAAAAFBMKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANOKVC537typ1NRUx/Jnn32mhIQEvfjii7p06ZLLwgEAAAAASocilcunn35aBw4ckCT9+OOP6tq1qwIDA/XJJ5/ohRdecGlAAAAAAEDJV6RyeeDAATVs2FCS9Mknn+i+++7TwoULlZycrE8//dSV+QAAAAAApUCRyqVhGMrLy5MkrVmzRg8//LAkqWrVqjp16pTr0gEAAAAASoUilcvY2FhNmDBB8+fP14YNG9SuXTtJ0uHDh1WpUiWXBgQAAAAAlHxFKpfTpk3Tzp07NWjQIL300kuqWbOmJGnx4sVq3ry5SwMCAAAAAEo+n6K8qH79+k53i73q9ddfl7e3t+lQAAAAAIDSpcifc3nmzBm98847GjlypE6fPi1J2rdvn06ePOmycAAAAACA0qFIM5d79uxRfHy8wsLClJaWpv79+ys8PFxLlizR0aNH9f7777s6JwAAAACgBCvSzOXQoUPVu3dvHTx4UP7+/o71Dz/8sDZu3OiycAAAAACA0qFI5XLbtm16+umnr1lfuXJlnThxwnQoAAAAAEDpUqRy6efnp6ysrGvWHzhwQBUqVDAdCgAAAABQuhSpXHbo0EHjxo3T5cuXJUk2m01Hjx7V8OHD9dhjj7k0IAAAAACg5CtSuZwyZYqys7NVsWJFXbhwQffff79q1qyp4OBgTZw40dUZncTFxclms8lmsyklJeW62yQnJyssLMytOUqSUaNG6c9//vMNny/I3xkAAAAAmFGku8WGhoZq9erV+te//qXdu3crOztbjRo1UqtWrVyd77r69++vcePGqXz58pKktLQ0VatWTYZhFMvxS5ITJ05o+vTpTp872qtXL9ntdiUlJUmSlixZokOHDqlx48YWpQQAAADg6YpULt9//3116dJFLVq0UIsWLRzrL126pEWLFqlHjx4uC3g9gYGBioiIcOsx3MUwDOXm5srHp0h/9dd455131Lx5c8XExNxwm/Dw8OteIwsAAAAArlKk02J79+6tzMzMa9afPXtWvXv3Nh3KVVauXKnatWsrKChIDz30kDIyMhzPxcXFKTEx0Wn7hIQE9erVy7Fst9v1yiuvqE+fPgoODlZ0dLTmzJnj9Jqvv/5aDRs2lL+/v2JjY7Vs2TKn00/Xr18vm82mFStW6J577pGfn58++OADeXl5afv27U77mjZtmmJiYpSXl1fgMS5atEjt27cv8PYAAAAA4A5FKpeGYchms12z/j//+Y9CQ0NNh3KF8+fP64033tD8+fO1ceNGHT16VMOGDSv0fqZMmaLY2Fjt2rVLzz77rJ555hnt379fkpSVlaX27durXr162rlzp8aPH6/hw4dfdz8jRozQq6++qu+++04dOnRQq1atNG/ePKdt5s2bp169esnL6/pflqSkJNntdsfy6dOntW/fPsXGxhZ6XL+Xk5OjrKwspwcAAAAAFFShzs28++67HTeGiY+Pdzq1Mzc3V4cPH9ZDDz3k8pD5sdvt11xvefnyZb399tuqUaOGJGnQoEEaN25coff98MMP69lnn5UkDR8+XH/961+1bt061apVSwsXLpTNZtPcuXPl7++vu+66S8eOHVP//v2v2c+4ceP04IMPOpb79eunAQMGaOrUqfLz89POnTuVmpqqzz777IZZypcv7xiPJB09elSGYSgqKsppu+Tk5EKPc9KkSRo7dmyhXwcAAAAAUiHLZUJCgiQpJSVFbdq0UVBQkOM5X19f2e32EvNRJIGBgU5FLDIyUidPniz0furXr+/4s81mU0REhGM/+/fvV/369eXv7+/Y5kY3zfn97GJCQoIGDhyopUuXqmvXrkpOTlbLli2dZiZ/b9CgQRo0aJBj+cKFC5LkdPyiGjlypIYOHepYzsrKUtWqVU3vFwAAAMCtoVDlcsyYMZJ+nSns0qWLS0qNu9x2221OyzabzWl208vL67qznQXZT2GuibyqTJkyTsu+vr7q0aOH5s2bp06dOmnhwoWaPn16ofZ59W65v/zyiypUqFDoTL/l5+cnPz8/U/sAAAAAcOsq0jWXPXv2LNHFsiAqVKjgdIOf3Nxc7d27t1D7qFWrllJTU5WTk+NYt23btgK/vl+/flqzZo1mzZqlK1euqFOnToU6fo0aNRQSEqJ9+/YV6nUAAAAA4GpFKpe5ubl644031LhxY0VERCg8PNzpURo88MAD+vzzz/X555/r+++/1zPPPKMzZ84Uah9PPvmk8vLy9Oc//1nfffedVq5cqTfeeEOSrnvDo9+rXbu2mjZtquHDh6tbt24KCAi46fYzZ85UfHy8Y9nLy0utWrXS5s2bC5UbAAAAAFytSOVy7Nixmjp1qrp06aLMzEwNHTpUnTp1kpeXl5KSklwc0T369Omjnj17qkePHrr//vtVvXp1tWzZslD7CAkJ0T//+U+lpKSoYcOGeumllzR69GhJBb8Osm/fvrp06ZL69OmT77anTp3SoUOHnNb169dPixYtKtKpugAAAADgKjbj9xceFkCNGjX05ptvql27dgoODlZKSopj3TfffKOFCxe6I6ukXz+fsmHDhpo2bZrbjmHGggULHJ8Dmt9MpCSNHz9en3zyifbs2VOk4xmGoSZNmmjIkCHq1q3bDbdLS0tTtWrVtGvXLjVs2DDf/WZlZSk0NFQBkvKfgy19XrE6gJsNLtKvjUqJjlYHcKNGVgdwM7vVAdyodJy0UzTBVgdws9J9lc/NeVsdwM08+Wedp3/tUOpkZUuhTaXMzEyFhITccLsifVueOHFC9erVkyQFBQUpMzNTkvTII4/o888/L8ouC2XWrFkKCgpSamqq24+Vn/fff1+bN2/W4cOHtWzZMg0fPlxPPPFEvsUyOztbe/fu1cyZM/WXv/ylyMe32WyaM2eOrly5csNt2rZtqzp16hT5GAAAAACQn0LdLfaqKlWqKCMjQ9HR0apRo4ZWrVqlRo0aadu2bW6/4+iCBQscH8ERHR3t1mMVxIkTJzR69GidOHFCkZGR6ty5syZOnJjv6wYNGqQPP/xQCQkJBTol9mYaNmx409nId955p0T9nQEAAADwPEU6LXbEiBEKCQnRiy++qI8++kh/+tOfZLfbdfToUQ0ZMkSvvvqqO7KiGHFabOnGabGlFKfFll6cFlt6cVps6eXJP+s8/WuHUqegp8UWaebyt+WxS5cuiomJ0ddff63bb79d7du3L8ouAQAAAAClWJHK5caNG9W8eXP5+Pz68qZNm6pp06a6cuWKNm7cqPvuu8+lIQEAAAAAJVuRTiho2bKlTp8+fc36zMzMQn+cBwAAAACg9CtSuTQMQzbbtVfi/fzzzypTpozpUAAAAACA0qVQp8V26tRJ0q8ff9GrVy+nO8Pm5uZqz549at68uWsTAgAAAABKvEKVy9DQUEm/zlwGBwc7fZajr6+vmjZtqv79+7s2IQAAAACgxCtUuZw3b54kqUKFCkpKSlJgYKAkKS0tTcuWLVPt2rVVvnx516cEAAAAAJRoRbrmcteuXXr//fclSWfOnFHTpk01ZcoUJSQkaPbs2S4NCAAAAAAo+YpcLv/4xz9KkhYvXqxKlSrpyJEjev/99/Xmm2+6NCAAAAAAoOQrUrk8f/68goODJUmrVq1Sp06d5OXlpaZNm+rIkSMuDQgAAAAAKPmKVC5r1qypZcuWKT09XStXrlTr1q0lSSdPnlRISIhLAwIAAAAASr4ilcvRo0dr2LBhstvtatKkiZo1aybp11nMu+++26UBAQAAAAAlX6HuFnvV448/rnvvvVcZGRlq0KCBY318fLw6duzosnAAAAAAgNKhSOVSkiIiIhQREeG0rnHjxqYDAQAAAABKnyKdFgsAAAAAwG9RLgEAAAAAplEuAQAAAACmUS4BAAAAAKYV+YY+QGm2xuoAbhabZ3UC92nhyV+8/1odwM2qWh3AjcKtDuBGgVYHcDN/qwO4kbfVAdzMk8fH9A9KmosF24x/ugAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMolwAAAAAA0yiXAAAAAADTKJcAAAAAANMsLZdxcXGy2Wyy2WxKSUmxMkqBpKWlWZr10qVLqlmzpr7++mun9e+++65at259w9f16tXL8fe8bNkyN6cEAAAAcCuyfOayf//+ysjIUN26dSX9r8AVxPr162Wz2XTmzBk3JvyfqlWrOmUtbm+//baqVaum5s2bO9ZdvHhRo0aN0pgxYxzrkpKS1KtXL8fy9OnTlZGRUZxRAQAAANxiLC+XgYGBioiIkI+Pj6U5Ll++nO823t7elmU1DEMzZ85U3759ndYvXrxYISEhatGixQ1fGxoaqoiICHdHBAAAAHALs7xc5ufIkSNq3769ypYtqzJlyqhOnTr64osvlJaWppYtW0qSypYtK5vN5pit+/LLL3XvvfcqLCxM5cqV0yOPPKJDhw459nl1dvSjjz7S/fffL39/f82ePVsBAQFasWKF0/GXLl2q4OBgnT9//prTYq/OnK5du1axsbEKDAxU8+bNtX//fqd9TJgwQRUrVlRwcLD69eunESNGqGHDhoX6e9ixY4cOHTqkdu3aOa1ftGiR2rdvX6h9AQAAAICrlfhyOXDgQOXk5Gjjxo1KTU3V5MmTFRQUpKpVq+rTTz+VJO3fv18ZGRmaPn26JOncuXMaOnSotm/frrVr18rLy0sdO3ZUXl6e075HjBihwYMH67vvvlPnzp31yCOPaOHChU7bLFiwQAkJCQoMDLxhxpdeeklTpkzR9u3b5ePjoz59+ji9fuLEiZo8ebJ27Nih6OhozZ49O99x2+12JSUlOZY3bdqkO+64Q8HBwU7bbd68WbGxsfnuDwAAAADcydpzUa/DbrfLMAzH8tGjR/XYY4+pXr16kqTq1as7ngsPD5ckVaxYUWFhYY71jz32mNM+//73v6tChQrat2+f0/WSiYmJ6tSpk2O5e/fueuqpp3T+/HkFBgYqKytLn3/+uZYuXXrTzBMnTtT9998v6dfC2q5dO128eFH+/v6aMWOG+vbtq969e0uSRo8erVWrVik7O/um+6xRo4bKly/vWD5y5IiioqKctjlz5owyMzOvWf/bUlpQOTk5ysnJcSxnZWUVeh8AAAAAbl0lfubyueee04QJE9SiRQuNGTNGe/bsyfc1Bw8eVLdu3VS9enWFhITIbrdL+rWo/tbvZ/wefvhh3XbbbfrHP/4hSfr0008VEhKiVq1a3fR49evXd/w5MjJSknTy5ElJv86qNm7c2Gn73y9fz9q1azVo0CDH8oULF+Tv7++0zYULFyTpmvVFMWnSJIWGhjoeVatWNb1PAAAAALeOEl8u+/Xrpx9//FFPPfWUUlNTFRsbqxkzZtz0Ne3bt9fp06c1d+5cbdmyRVu2bJH060d5/FaZMmWcln19ffX44487To1duHChunTpku8NfG677TbHn6/e6fb3p+CaVb58ef3yyy9O68qVKyebzXbN+qIYOXKkMjMzHY/09HTT+wQAAABw6yjx5VL69SNABgwYoCVLluj//u//NHfuXEm/lkFJys3NdWz7888/a//+/Xr55ZcVHx+v2rVrF6p8de/eXV9++aW+/fZbffXVV+revbup7LVq1dK2bduc1v1+uSDuvvtuff/9906nDPv6+uquu+7Svn37TGWUJD8/P4WEhDg9AAAAAKCgSny5TExM1MqVK3X48GHt3LlT69atU+3atSVJMTExstlsWr58uX766SdlZ2erbNmyKleunObMmaMffvhBX331lYYOHVrg4913332KiIhQ9+7dVa1aNTVp0sRU/r/85S9699139d577+ngwYOaMGGC9uzZk+9necbHx2vmzJmO5ZYtWyo7O1vffvut03Zt2rTR5s2bTWUEAAAAALNKfLnMzc3VwIEDVbt2bT300EO64447NGvWLElS5cqVNXbsWI0YMUKVKlXSoEGD5OXlpUWLFmnHjh2qW7euhgwZotdff73Ax7PZbOrWrZt2795tetZS+nUmdOTIkRo2bJgaNWqkw4cPq1evXvleJ3no0CGdOnXKsVyuXDl17NhRCxYscNqub9+++uKLL5SZmWk6KwAAAAAUlc347XmWxSwuLk4NGzbUtGnTrIpgiQcffFARERGaP39+oV63Z88ePfjggzp06JCCgoIc6zt37qxGjRpp5MiRN329zWbT0qVLlZCQkO+xsrKyFBoaqgBJN59jLZ0esDqAm42wOoAbtQi1OoEb1bM6gJt58n3Cwq0O4EY3/iQuz2D+nngll7fVAdzMk8dX4qd/cKvJuiiFjpcyMzNvevmc5f90Z82apaCgIKWmplodxS3Onz+vqVOn6ttvv9X333+vMWPGaM2aNerZs2eh91W/fn1NnjxZhw8fdlr/+uuvO5XN3xswYMBNnwcAAAAAsyyduTx27Jjj4zSio6MdN+jxJBcuXFD79u21a9cuXbx4UbVq1dLLL7/s9Pma7nby5EnH51ZGRkZec5fc62HmsnRj5rKUYuay9GLmsvRi5rL08uTxWT79Azgr6MzlzT9jw80qV65s5eGLRUBAgNasWWNphooVK6pixYqWZgAAAADg2fi9CAAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDTKJQAAAADANMolAAAAAMA0yiUAAAAAwDSbYRiG1SFQ8mRlZSk0NFQBkmxWhwEAAABgGUPSBUmZmZkKCQm54XbMXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcFkBcXJxsNptsNptSUlIK9Jrk5GSFhYW5NVdBjpOUlOTIPm3aNLfnAQAAAHBrolwWUP/+/ZWRkaG6desqLS1NNpvN6kjXlZycrLi4OMfysGHDlJGRoSpVqlgXCgAAAIDH87E6QGkRGBioiIgIq2MUWlBQkIKCguTt7W11FAAAAAAejJlLF0lOTlZ0dLQCAwPVsWNH/fzzz9ds89lnn6lRo0by9/dX9erVNXbsWF25csXx/NSpU1WvXj2VKVNGVatW1bPPPqvs7OxCHwcAAAAAihvl0gW2bNmivn37atCgQUpJSVHLli01YcIEp202bdqkHj16aPDgwdq3b5/+9re/KTk5WRMnTnRs4+XlpTfffFPffvut3nvvPX311Vd64YUXCnWcosrJyVFWVpbTAwAAAAAKymYYhmF1iJIuLi5ODRs2vOENcZ588kllZmbq888/d6zr2rWrvvzyS505c0aS1KpVK8XHx2vkyJGObT744AO98MILOn78+HX3u3jxYg0YMECnTp0q8HFuxG63KzExUYmJidd9PikpSWPHjr1mfYCkknl1KQAAAIDiYEi6ICkzM1MhISE33I6ZSxf47rvv1KRJE6d1zZo1c1revXu3xo0b57gGMigoyHGToPPnz0uS1qxZo/j4eFWuXFnBwcF66qmn9PPPPzueL8hximrkyJHKzMx0PNLT012yXwAAAAC3Bm7oU0yys7M1duxYderU6Zrn/P39lZaWpkceeUTPPPOMJk6cqPDwcG3evFl9+/bVpUuXFBgY6NZ8fn5+8vPzc+sxAAAAAHguyqUL1K5dW1u2bHFa98033zgtN2rUSPv371fNmjWvu48dO3YoLy9PU6ZMkZfXrxPKH3/8caGPAwAAAABWoFy6wHPPPacWLVrojTfe0KOPPqqVK1fqyy+/dNpm9OjReuSRRxQdHa3HH39cXl5e2r17t/bu3asJEyaoZs2aunz5smbMmKH27dvrX//6l95+++1CHwcAAAAArMA1ly7QtGlTzZ07V9OnT1eDBg20atUqvfzyy07btGnTRsuXL9eqVav0hz/8QU2bNtVf//pXxcTESJIaNGigqVOnavLkyapbt64WLFigSZMmFfo4AAAAAGAF7hZbAPndLbY0yO9usb+XlZWl0NBQ7hYLAAAA3OK4W6yLzZo1S0FBQUpNTbU6SqG88sorCgoK0tGjR62OAgAAAMCDMXNZAMeOHdOFCxckSdHR0fL19bU4UcGdPn1ap0+fliRVqFBBoaGhBXodM5cAAAAApILPXHJDnwKoXLmy1RGKLDw8XOHh4VbHAAAAAODhOC0WAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYBrlEgAAAABgGuUSAAAAAGAa5RIAAAAAYJqP1QFQMhmG8et/Lc4BAAAAwFpXO8HVjnAjlEtc19mzZyVJFy3OAQAAAKBkOHv2rEJDQ2/4vM3Ir37ilpSXl6fjx48rODhYNpvNrcfKyspS1apVlZ6erpCQELceywqePD5PHpvk2eNjbKWXJ4+PsZVenjw+xlZ6efL4intshmHo7NmzioqKkpfXja+sZOYS1+Xl5aUqVaoU6zFDQkI87hv/tzx5fJ48Nsmzx8fYSi9PHh9jK708eXyMrfTy5PEV59huNmN5FTf0AQAAAACYRrkEAAAAAJhGuYTl/Pz8NGbMGPn5+VkdxS08eXyePDbJs8fH2EovTx4fYyu9PHl8jK308uTxldSxcUMfAAAAAIBpzFwCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXMJyb731lux2u/z9/dWkSRNt3brV6kgusXHjRrVv315RUVGy2WxatmyZ1ZFcZtKkSfrDH/6g4OBgVaxYUQkJCdq/f7/VsVxi9uzZql+/vuNDiZs1a6YVK1ZYHcstXn31VdlsNiUmJlodxSWSkpJks9mcHnfeeafVsVzm2LFj+tOf/qRy5copICBA9erV0/bt262O5RJ2u/2ar53NZtPAgQOtjmZabm6uRo0apWrVqikgIEA1atTQ+PHj5Sn3Uzx79qwSExMVExOjgIAANW/eXNu2bbM6VpHk93PbMAyNHj1akZGRCggIUKtWrXTw4EFrwhZSfmNbsmSJWrdurXLlyslmsyklJcWSnEVxs7FdvnxZw4cPV7169VSmTBlFRUWpR48eOn78uHWBCym/r11SUpLuvPNOlSlTRmXLllWrVq20ZcsWa8KKcgmLffTRRxo6dKjGjBmjnTt3qkGDBmrTpo1OnjxpdTTTzp07pwYNGuitt96yOorLbdiwQQMHDtQ333yj1atX6/Lly2rdurXOnTtndTTTqlSpoldffVU7duzQ9u3b9cADD+jRRx/Vt99+a3U0l9q2bZv+9re/qX79+lZHcak6deooIyPD8di8ebPVkVzil19+UYsWLXTbbbdpxYoV2rdvn6ZMmaKyZctaHc0ltm3b5vR1W716tSSpc+fOFiczb/LkyZo9e7Zmzpyp7777TpMnT9Zrr72mGTNmWB3NJfr166fVq1dr/vz5Sk1NVevWrdWqVSsdO3bM6miFlt/P7ddee01vvvmm3n77bW3ZskVlypRRmzZtdPHixWJOWnj5je3cuXO69957NXny5GJOZt7Nxnb+/Hnt3LlTo0aN0s6dO7VkyRLt379fHTp0sCBp0eT3tbvjjjs0c+ZMpaamavPmzbLb7WrdurV++umnYk76/xmAhRo3bmwMHDjQsZybm2tERUUZkyZNsjCV60kyli5danUMtzl58qQhydiwYYPVUdyibNmyxjvvvGN1DJc5e/ascfvttxurV6827r//fmPw4MFWR3KJMWPGGA0aNLA6hlsMHz7cuPfee62OUWwGDx5s1KhRw8jLy7M6imnt2rUz+vTp47SuU6dORvfu3S1K5Drnz583vL29jeXLlzutb9SokfHSSy9ZlMo1fv9zOy8vz4iIiDBef/11x7ozZ84Yfn5+xocffmhBwqK72XuSw4cPG5KMXbt2FWsmVynI+62tW7cakowjR44UTygXKsj4MjMzDUnGmjVriifU7zBzCctcunRJO3bsUKtWrRzrvLy81KpVK/373/+2MBkKKzMzU5IUHh5ucRLXys3N1aJFi3Tu3Dk1a9bM6jguM3DgQLVr187pe89THDx4UFFRUapevbq6d++uo0ePWh3JJf7xj38oNjZWnTt3VsWKFXX33Xdr7ty5Vsdyi0uXLumDDz5Qnz59ZLPZrI5jWvPmzbV27VodOHBAkrR7925t3rxZbdu2tTiZeVeuXFFubq78/f2d1gcEBHjMWQNXHT58WCdOnHD6/2ZoaKiaNGnCe5ZSJjMzUzabTWFhYVZHcblLly5pzpw5Cg0NVYMGDSzJ4GPJUQFJp06dUm5uripVquS0vlKlSvr+++8tSoXCysvLU2Jiolq0aKG6detaHcclUlNT1axZM128eFFBQUFaunSp7rrrLqtjucSiRYu0c+fOUntN1M00adJEycnJqlWrljIyMjR27Fj98Y9/1N69exUcHGx1PFN+/PFHzZ49W0OHDtWLL76obdu26bnnnpOvr6969uxpdTyXWrZsmc6cOaNevXpZHcUlRowYoaysLN15553y9vZWbm6uJk6cqO7du1sdzbTg4GA1a9ZM48ePV+3atVWpUiV9+OGH+ve//62aNWtaHc+lTpw4IUnXfc9y9TmUfBcvXtTw4cPVrVs3hYSEWB3HZZYvX66uXbvq/PnzioyM1OrVq1W+fHlLslAuAZgycOBA7d2716N+S12rVi2lpKQoMzNTixcvVs+ePbVhw4ZSXzDT09M1ePBgrV69+pqZBk/w25mg+vXrq0mTJoqJidHHH3+svn37WpjMvLy8PMXGxuqVV16RJN19993au3ev3n77bY8rl++++67atm2rqKgoq6O4xMcff6wFCxZo4cKFqlOnjlJSUpSYmKioqCiP+NrNnz9fffr0UeXKleXt7a1GjRqpW7du2rFjh9XRACeXL1/WE088IcMwNHv2bKvjuFTLli2VkpKiU6dOae7cuXriiSe0ZcsWVaxYsdizcFosLFO+fHl5e3vrv//9r9P6//73v4qIiLAoFQpj0KBBWr58udatW6cqVapYHcdlfH19VbNmTd1zzz2aNGmSGjRooOnTp1sdy7QdO3bo5MmTatSokXx8fOTj46MNGzbozTfflI+Pj3Jzc62O6FJhYWG644479MMPP1gdxbTIyMhrfrlRu3Ztjznt96ojR45ozZo16tevn9VRXOb555/XiBEj1LVrV9WrV09PPfWUhgwZokmTJlkdzSVq1KihDRs2KDs7W+np6dq6dasuX76s6tWrWx3Npa6+L+E9S+l0tVgeOXJEq1ev9qhZS0kqU6aMatasqaZNm+rdd9+Vj4+P3n33XUuyUC5hGV9fX91zzz1au3atY11eXp7Wrl3rUde3eSLDMDRo0CAtXbpUX331lapVq2Z1JLfKy8tTTk6O1TFMi4+PV2pqqlJSUhyP2NhYde/eXSkpKfL29rY6oktlZ2fr0KFDioyMtDqKaS1atLjm434OHDigmJgYixK5x7x581SxYkW1a9fO6iguc/78eXl5Ob/d8vb2Vl5enkWJ3KNMmTKKjIzUL7/8opUrV+rRRx+1OpJLVatWTREREU7vWbKysrRlyxbes5RwV4vlwYMHtWbNGpUrV87qSG5n5fsWTouFpYYOHaqePXsqNjZWjRs31rRp03Tu3Dn17t3b6mimZWdnO82YHD58WCkpKQoPD1d0dLSFycwbOHCgFi5cqM8++0zBwcGO601CQ0MVEBBgcTpzRo4cqbZt2yo6Olpnz57VwoULtX79eq1cudLqaKYFBwdfc11smTJlVK5cOY+4XnbYsGFq3769YmJidPz4cY0ZM0be3t7q1q2b1dFMGzJkiJo3b65XXnlFTzzxhLZu3ao5c+Zozpw5Vkdzmby8PM2bN089e/aUj4/nvD1p3769Jk6cqOjoaNWpU0e7du3S1KlT1adPH6ujucTKlStlGIZq1aqlH374Qc8//7zuvPPOUvlzPL+f24mJiZowYYJuv/12VatWTaNGjVJUVJQSEhKsC11A+Y3t9OnTOnr0qOPzH6/+MisiIqLEz8zebGyRkZF6/PHHtXPnTi1fvly5ubmO9yzh4eHy9fW1KnaB3Wx85cqV08SJE9WhQwdFRkbq1KlTeuutt3Ts2DHrPsrJknvUAr8xY8YMIzo62vD19TUaN25sfPPNN1ZHcol169YZkq559OzZ0+popl1vXJKMefPmWR3NtD59+hgxMTGGr6+vUaFCBSM+Pt5YtWqV1bHcxpM+iqRLly5GZGSk4evra1SuXNno0qWL8cMPP1gdy2X++c9/GnXr1jX8/PyMO++805gzZ47VkVxq5cqVhiRj//79VkdxqaysLGPw4MFGdHS04e/vb1SvXt146aWXjJycHKujucRHH31kVK9e3fD19TUiIiKMgQMHGmfOnLE6VpHk93M7Ly/PGDVqlFGpUiXDz8/PiI+PLzX/XvMb27x58677/JgxYyzNXRA3G9vVj1a53mPdunVWRy+Qm43vwoULRseOHY2oqCjD19fXiIyMNDp06GBs3brVsrw2wzAMN/VWAAAAAMAtgmsuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAAAAAplEuAQAAAACmUS4BAAAAAKZRLgEAuMX06tVLCQkJVscAAHgYyiUAAAAAwDTKJQAAHmrx4sWqV6+eAgICVK5cObVq1UrPP/+83nvvPX322Wey2Wyy2Wxav369JCk9PV1PPPGEwsLCFB4erkcffVRpaWmO/V2d8Rw7dqwqVKigkJAQDRgwQJcuXbrpMc+dO1fMIwcAWMHH6gAAAMD1MjIy1K1bN7322mvq2LGjzp49q02bNqlHjx46evSosrKyNG/ePElSeHi4Ll++rDZt2qhZs2batGmTfHx8NGHCBD300EPas2ePfH19JUlr166Vv7+/1q9fr7S0NPXu3VvlypXTxIkTb3hMwzCs/KsAABQTyiUAAB4oIyNDV65cUadOnRQTEyNJqlevniQpICBAOTk5ioiIcGz/wQcfKC8vT++8845sNpskad68eQoLC9P69evVunVrSZKvr6/+/ve/KzAwUHXq1NG4ceP0/PPPa/z48Tc9JgDA83FaLAAAHqhBgwaKj49XvXr11LlzZ82dO1e//PLLDbffvXu3fvjhBwUHBysoKEhBQUEKDw/XxYsXdejQIaf9BgYGOpabNWum7OxspaenF/qYAADPQrkEAMADeXt7a/Xq1VqxYoXuuusuzZgxQ7Vq1dLhw4evu312drbuuecepaSkOD0OHDigJ5980i3HBAB4FsolAAAeymazqUWLFho7dqx27dolX19fLV26VL6+vsrNzXXatlGjRjp48KAqVqyomjVrOj1CQ0Md2+3evVsXLlxwLH/zzTcKCgpS1apVb3pMAIDno1wCAOCBtmzZoldeeUXbt2/X0aNHtWTJEv3000+qXbu27Ha79uzZo/379+vUqVO6fPmyunfvrvLly+vRRx/Vpk2bdPjwYa1fv17PPfec/vOf/zj2e+nSJfXt21f79u3TF198oTFjxmjQoEHy8vK66TEBAJ6PG/oAAOCBQkJCtHHjRk2bNk1ZWVmKiYnRlClT1LZtW8XGxmr9+vWKjY1Vdna21q1bp7i4OG3cuFHDhw9Xp06ddPbsWVWuXFnx8fEKCQlx7Dc+Pl6333677rvvPuXk5Khbt25KSkrK95gAAM9nM7g/OAAAKIBevXrpzJkzWrZsmdVRAAAlEKfFAgAAAABMo1wCAAAAAEzjtFgAAAAAgGnMXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEyjXAIAAAAATKNcAgAAAABMo1wCAAAAAEz7fz8nSRQd2FirAAAAAElFTkSuQmCC",
"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-04-24T14:31:54.918529Z",
"iopub.status.busy": "2025-04-24T14:31:54.918135Z",
"iopub.status.idle": "2025-04-24T14:31:54.922227Z",
"shell.execute_reply": "2025-04-24T14:31:54.921752Z"
}
},
"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-04-24T14:31:54.924393Z",
"iopub.status.busy": "2025-04-24T14:31:54.924003Z",
"iopub.status.idle": "2025-04-24T14:31:54.928130Z",
"shell.execute_reply": "2025-04-24T14:31:54.927709Z"
}
},
"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-04-24T14:31:54.930034Z",
"iopub.status.busy": "2025-04-24T14:31:54.929772Z",
"iopub.status.idle": "2025-04-24T14:31:54.979587Z",
"shell.execute_reply": "2025-04-24T14:31:54.979124Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "dc1f0d8f72c74ba5b014bbfa02850528",
"version_major": 2,
"version_minor": 0
},
"text/plain": [
"Output()"
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "58941e55421d4b84afbfe38e62c83e2b",
"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"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"stormvogel_dtmc = 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-04-24T14:31:55.010176Z",
"iopub.status.busy": "2025-04-24T14:31:55.010015Z",
"iopub.status.idle": "2025-04-24T14:31:55.153155Z",
"shell.execute_reply": "2025-04-24T14:31:55.152597Z"
}
},
"outputs": [
{
"data": {
"image/png": "iVBORw0KGgoAAAANSUhEUgAAA6IAAALeCAYAAACwb6yJAAAAOXRFWHRTb2Z0d2FyZQBNYXRwbG90bGliIHZlcnNpb24zLjkuMiwgaHR0cHM6Ly9tYXRwbG90bGliLm9yZy8hTgPZAAAACXBIWXMAAA9hAAAPYQGoP6dpAABXs0lEQVR4nO39e5xVdaE//r82IMNlhkG8DSA4KqkoKhKpQOZ4OWoX08y8ZCZeKC8dJe/mUfAG6cmiMjTTI2V4sqNmJ9O8fQSVk5dUlJK8JYI2RX0NRhRGhfn94c99zuSNGca1YXg+H4/9OLPWfu+1XmvGE/Oa99rvXWppaWkJAAAAFKRLpQMAAACwdlFEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUqlulA7DmW7FiRf785z+npqYmpVKp0nEAAIAKaWlpySuvvJIBAwakS5f3nvdURFllf/7znzNo0KBKxwAAAFYTCxYsyMYbb/yezyuirLKampokb/3H1qdPnwqn6Rh1tbWVjgAAAGucliTL8r8d4b0ooqyyt2/H7dOnT6cpom4wBgCA9vugt+xZrAgAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShFdDTQ0NKRUKqVUKmX27NnveH7atGnp27dvm485fvz4Nr1m2rRp5RxtfS0AAMDKUkRXE+PGjUtjY2OGDRuWefPmpVQqlZ87+OCD8/TTT7fpeDfddFMuuOCC8nZ9fX2mTJnSasyMGTNSX1/f6jyNjY0ZNWpUu64BAABgZXSrdADe0qtXr9TV1b3rcz179kzPnj3bdLx+/fq1OcPb5+nevXubXwsAALCyzIiuAf751tyJEydm+PDhufbaa1NfX5/a2toccsgheeWVV8pj/u+tuQ0NDXnhhRfy9a9/vXzrLQAAQKUoomuo5557LjfffHNuueWW3HLLLZk5c2a++c1vvuvYm266KRtvvHHOP//8NDY2prGxcZXO3dzcnKamplYPAACAlaWIrobq6+vT0tLyvmNWrFiRadOmZdiwYdlll11y+OGH5+67737Xsf369UvXrl1TU1OTurq68i3ADQ0NmTdvXpvzTZ48ObW1teXHoEGD2nwMAABg7aWIrqHq6+tTU1NT3u7fv38WLlxYyLnPOuusLF68uPxYsGBBIecFAAA6B4sVraHWWWedVtulUikrVqwo5NxVVVWpqqoq5FwAAEDnY0Z0LdG9e/csX7680jEAAAAU0bVFfX197r333rz00kv5+9//Xuk4AADAWkwRXUucf/75mTdvXjbffPNssMEGlY4DAACsxUotH7Q8Kx+6hoaGDB8+PFOmTKl0lCRtz9PU1JTa2tosXrw4ffr0+XDDFaS3z1oFAIA2a0myNPnAbmBGdDUxderUVFdXZ86cORXLMH369FRXV+e+++6rWAYAAKDzMyO6GnjppZeydOnSJMngwYPTvXv3iuR45ZVX8te//jVJ0rdv36y//vor9TozogAAQLLyM6I+vmU1MHDgwEpHSJLU1NS0+mxSAACAD4NbcwEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIXqVukAdB51tbUpVTpEB3n1sEon6Di9p1c6Qcc6sNIBOtgNlQ7QgfpVOkAHe7nSATrYOpUO0IHeqHQAAFaZGVEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRXUs1NDSkVCqlVCpl9uzZmTdvXnl7+PDhlY4HAAB0YoroWmzcuHFpbGzMsGHDMmjQoDQ2NuaUU06pdCwAAKCT61bpAFROr169UldXV96uq6tLdXV1BRMBAABrAzOiAAAAFMqMKG3W3Nyc5ubm8nZTU1MF0wAAAGsaM6K02eTJk1NbW1t+DBo0qNKRAACANYgiSpudddZZWbx4cfmxYMGCSkcCAADWIG7Npc2qqqpSVVVV6RgAAMAayowoAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliK7Fpk6dmurq6syZMyfz589PdXV1Jk2aVOlYAABAJ2fV3LXU9OnTs3Tp0iTJ4MGD06VLl8yePTtJrIgLAAB8qBTRtdTAgQPfsW/IkCEVSAIAAKxt3JoLAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEV1LNTQ0pFQqpVQqZfbs2Zk3b155e/jw4ZWOBwAAdGKK6Fps3LhxaWxszLBhwzJo0KA0NjbmlFNOqXQsAACgk+tW6QBUTq9evVJXV1ferqurS3V1dQUTAQAAawNFlDZrbm5Oc3NzebupqamCaQAAgDWNW3Nps8mTJ6e2trb8GDRoUKUjAQAAaxBFlDY766yzsnjx4vJjwYIFlY4EAACsQdyaS5tVVVWlqqqq0jEAAIA1lBlRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiuhabOrUqamurs6cOXMyf/78VFdXZ9KkSZWOBQAAdHI+vmUtNX369CxdujRJMnjw4HTp0iWzZ89OEh/NAgAAfKgU0bXUwIED37FvyJAhFUgCAACsbdyaCwAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhepW6QCwOuo9vdIJOs7PKh2ggx1S6QAdbOtKB+hAT1Y6QAfrUekAHWxZpQN0oK6VDtDBllc6AEAFmBEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEU0bVUQ0NDSqVSSqVSZs+enXnz5pW3hw8fXul4AABAJ6aIrsXGjRuXxsbGDBs2LIMGDUpjY2NOOeWUSscCAAA6uW6VDkDl9OrVK3V1deXturq6VFdXVzARAACwNjAjCgAAQKHMiNJmzc3NaW5uLm83NTVVMA0AALCmMSNKm02ePDm1tbXlx6BBgyodCQAAWIMoorTZWWedlcWLF5cfCxYsqHQkAABgDeLWXNqsqqoqVVVVlY4BAACsocyIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiuhabOrUqamurs6cOXMyf/78VFdXZ9KkSZWOBQAAdHJWzV1LTZ8+PUuXLk2SDB48OF26dMns2bOTxIq4AADAh0oRXUsNHDjwHfuGDBlSgSQAAMDaxq25AAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFNG1VENDQ0qlUkqlUmbPnp158+aVt4cPH17peAAAQCemiK7Fxo0bl8bGxgwbNiyDBg1KY2NjTjnllErHAgAAOrlulQ5A5fTq1St1dXXl7bq6ulRXV1cwEQAAsDYwIwoAAEChzIjSZs3NzWlubi5vNzU1VTANAACwpjEjSptNnjw5tbW15cegQYMqHQkAAFiDKKK02VlnnZXFixeXHwsWLKh0JAAAYA3i1lzarKqqKlVVVZWOAQAArKHMiAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIroWmzq1Kmprq7OnDlzMn/+/FRXV2fSpEmVjgUAAHRyVs1dS02fPj1Lly5NkgwePDhdunTJ7Nmzk8SKuAAAwIdKEV1LDRw48B37hgwZUoEkAADA2satuQAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRTRtVRDQ0NKpVJKpVJmz56defPmlbeHDx9e6XgAAEAnpoiuxcaNG5fGxsYMGzYsgwYNSmNjY0455ZRKxwIAADq5bpUOQOX06tUrdXV15e26urpUV1dXMBEAALA2UERps+bm5jQ3N5e3m5qaKpgGAABY07g1lzabPHlyamtry49BgwZVOhIAALAGUURps7POOiuLFy8uPxYsWFDpSAAAwBrErbm0WVVVVaqqqiodAwAAWEOZEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIrsWmTp2a6urqzJkzJ/Pnz091dXUmTZpU6VgAAEAn5+Nb1lLTp0/P0qVLkySDBw9Oly5dMnv27CTx0SwAAMCHShFdSw0cOPAd+4YMGVKBJAAAwNrGrbkAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFCodhXRRx99NHPmzClv//KXv8z++++fb3zjG3n99dc7LBwAAACdT7uK6Fe/+tU8/fTTSZI//elPOeSQQ9KrV6/813/9V04//fQODQgAAEDn0q4i+vTTT2f48OFJkv/6r//KJz7xiVx33XWZNm1abrzxxo7MBwAAQCfTriLa0tKSFStWJEnuuuuufOpTn0qSDBo0KH//+987Lh0AAACdTruK6MiRI3PhhRfm2muvzcyZM/PpT386SfL8889no4026tCAAAAAdC7tKqJTpkzJo48+mq997Ws5++yzM2TIkCTJDTfckNGjR3doQAAAADqXUktLS0tHHWzZsmXp2rVr1llnnY46JGuApqam1NbWpmeSUqXD8A4/q3SADnZIpQN0sK0rHaADPVnpAB2sR6UDdLBllQ7QgbpWOkAHW17pAAAdqCXJ0iSLFy9Onz593nNcuz9HdNGiRbnqqqty1lln5eWXX06SPPnkk1m4cGF7DwkAAMBaoFt7XvTEE09kjz32SN++fTNv3ryMGzcu/fr1y0033ZT58+fnJz/5SUfnBAAAoJNo14zoySefnCOPPDLPPPNMevT435uXPvWpT+Xee+/tsHAAAAB0Pu0qog8//HC++tWvvmP/wIED85e//GWVQwEAANB5tauIVlVVpamp6R37n3766WywwQarHAoAAIDOq11F9LOf/WzOP//8vPHGG0mSUqmU+fPn54wzzsjnP//5Dg0IAABA59KuInrppZdmyZIl2XDDDbN06dLsuuuuGTJkSGpqanLRRRd1dEY+BA0NDSmVSimVSpk9e3bmzZtX3h4+fHil4wEAAJ1Yu1bNra2tzZ133plZs2bl8ccfz5IlSzJixIjsueeeHZ2PD9G4ceNy/vnnZ/3110+pVEpjY2O+9a1v5a677qp0NAAAoBNrVxH9yU9+koMPPjhjxozJmDFjyvtff/31/OxnP8uXv/zlDgvIh6dXr16pq6srb9fV1aW6urqCiQAAgLVBu27NPfLII7N48eJ37H/llVdy5JFHrnIoAAAAOq92zYi2tLSkVCq9Y/+LL76Y2traVQ7F6q25uTnNzc3l7XdbQRkAAOC9tKmI7rDDDuUFbfbYY4906/a/L1++fHmef/757LPPPh0ektXL5MmTc95551U6BgAAsIZqUxHdf//9kySzZ8/O3nvv3er9hN27d099fb2Pb1kLnHXWWTn55JPL201NTRk0aFAFEwEAAGuSNhXRCRMmJEnq6+tz8MEHp0ePHh9KKFZvVVVVqaqqqnQMAABgDdWu94geccQRHZ0DAACAtUS7iujy5cvzne98Jz//+c8zf/78vP76662ef/nllzskHAAAAJ1Puz6+5bzzzsu3v/3tHHzwwVm8eHFOPvnkHHDAAenSpUsmTpzYwREBAADoTNpVRKdPn54f/ehHOeWUU9KtW7cceuihueqqq3LuuefmgQce6OiMAAAAdCLtKqJ/+ctfsu222yZJqqurs3jx4iTJZz7zmfz617/uuHR8qKZOnZrq6urMmTMn8+fPT3V1dSZNmlTpWAAAQCfXrveIbrzxxmlsbMzgwYOz+eab54477siIESPy8MMPW011DTF9+vQsXbo0STJ48OB06dIls2fPThI/QwAA4EPVriL6uc99LnfffXd22mmn/Ou//mu+9KUv5eqrr878+fPz9a9/vaMz8iEYOHDgO/YNGTKkAkkAAIC1TamlpaVlVQ/ywAMP5H/+53/ykY98JPvuu29H5GIN0tTUlNra2vRMUqp0GN7hZ5UO0MEOqXSADrZ1pQN0oCcrHaCDdbZPyl5W6QAdqGulA3Sw5ZUOANCBWpIsTbJ48eL06dPnPce1a0b03nvvzejRo9Ot21sv33nnnbPzzjvnzTffzL333ptPfOIT7TksAAAAa4F2LVa02267vetnhS5evDi77bbbKocCAACg82pXEW1paUmp9M6bMP+//+//S+/evVc5FAAAAJ1Xm27NPeCAA5IkpVIpY8eObbW66vLly/PEE09k9OjRHZsQAACATqVNRbS2tjbJWzOiNTU16dmzZ/m57t27Z+edd864ceM6NiEAAACdSpuK6DXXXJMk2WCDDTJx4sT06tUrSTJv3rzcfPPNGTp0aNZff/2OTwkAAECn0a73iD722GP5yU9+kiRZtGhRdt5551x66aXZf//9c/nll3doQAAAADqXdhfRXXbZJUlyww03ZKONNsoLL7yQn/zkJ/ne977XoQEBAADoXNpVRF977bXU1NQkSe64444ccMAB6dKlS3beeee88MILHRoQAACAzqVdRXTIkCG5+eabs2DBgtx+++3Za6+9kiQLFy5Mnz59OjQgAAAAnUu7iui5556bU089NfX19dlpp50yatSoJG/Nju6www4dGhAAAIDOpU2r5r7twAMPzMc//vE0NjZm++23L+/fY4898rnPfa7DwgEAAND5tKuIJkldXV3q6upa7dtxxx1XORAAAACdW7tuzQUAAID2UkQBAAAoVLtvzQXWDIdUOkAHO7DSAXhPu1Y6AO9rnUoHAGCt0JzkOysxzowoAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAq1xhTRhoaGlEqllEqlzJ49u9JxOty8efNWi2ubOHFi+fs8ZcqUimYBAAA6pzWmiCbJuHHj0tjYmGHDhiX53/JWtIkTJ2bs2LFtek19fX1mzJjxoeRZFdOmTUtDQ0N5+9RTT01jY2M23njjyoUCAAA6tW6VDtAWvXr1Sl1dXaVjdGrV1dWprq5O165dKx0FAADopNaoGdGVceONN2abbbZJVVVV6uvrc+mll7Z6vr6+PpMmTcpRRx2VmpqaDB48OFdeeWWrMQsWLMhBBx2Uvn37pl+/ftlvv/0yb968Ds350EMPZYcddkiPHj0ycuTIPPbYY+8YM3PmzOy4446pqqpK//79c+aZZ+bNN98sP9/Q0JATTzwxp59+evr165e6urpMnDix1TEWLVqUY445JhtssEH69OmT3XffPY8//niHXgsAAEBbdKoi+sgjj+Sggw7KIYcckjlz5mTixIk555xzMm3atFbjLr300nL5O/7443PcccflqaeeSpK88cYb2XvvvVNTU5P77rsvs2bNSnV1dfbZZ5+8/vrrHZJzyZIl+cxnPpOtt946jzzySCZOnJhTTz211ZiXXnopn/rUp/Kxj30sjz/+eC6//PJcffXVufDCC1uN+/GPf5zevXvnwQcfzCWXXJLzzz8/d955Z/n5L3zhC1m4cGFuu+22PPLIIxkxYkT22GOPvPzyy+3O39zcnKamplYPAACAlVVqaWlpqXSIldHQ0JDhw4e/7wI6hx12WP72t7/ljjvuKO87/fTT8+tf/zp/+MMfkrw1I7rLLrvk2muvTZK0tLSkrq4u5513Xo499tj89Kc/zYUXXpi5c+eW33/6+uuvp2/fvrn55puz1157rfK1XHnllfnGN76RF198MT169EiSXHHFFTnuuOPy2GOPZfjw4Tn77LNz4403tsoxderUnHHGGVm8eHG6dOmShoaGLF++PPfdd1/52DvuuGN23333fPOb38z999+fT3/601m4cGGqqqrKY4YMGZLTTz89X/nKV94zY319fcaPH5/x48e/47mJEyfmvPPOe8f+nkmKf8cua5sDKx2A97RBpQPwvtapdAAA1grNSb6TZPHixenTp897jutUM6Jz587NmDFjWu0bM2ZMnnnmmSxfvry8b7vttit/XSqVUldXl4ULFyZJHn/88Tz77LOpqakpv1+yX79+WbZsWZ577rkOy7nddtuVS2iSjBo16h1jRo0a1WoxpjFjxmTJkiV58cUX3/VakqR///6trmXJkiVZb731ytdSXV2d559/fpWu5ayzzsrixYvLjwULFrT7WAAAwNpnjVqsqKOss07rvwuXSqWsWLEiyVu3zX70ox/N9OnT3/G6DTZY/f7e/0HX0r9//3ddrbdv377tPmdVVVWrGVYAAIC26FRFdOjQoZk1a1arfbNmzcoWW2yx0qvAjhgxItdff3023HDD951KXhVDhw7Ntddem2XLlpVnRR944IF3jLnxxhvT0tJSnhWdNWtWampqVvqjVUaMGJG//OUv6datW+rr6zv0GgAAANqrU92ae8opp+Tuu+/OBRdckKeffjo//vGPc9lll71jIaD3c9hhh2X99dfPfvvtl/vuuy/PP/98ZsyYkRNPPLHVLbGr4otf/GJKpVLGjRuXJ598Mrfeemu+9a1vtRpz/PHHZ8GCBfnXf/3X/PGPf8wvf/nLTJgwISeffHK6dFm5H9uee+6ZUaNGZf/9988dd9yRefPm5X/+539y9tln53e/+12HXAsAAEBbdaoiOmLEiPz85z/Pz372swwbNiznnntuzj///IwdO3alj9GrV6/ce++9GTx4cA444IAMHTo0Rx99dJYtW/aeM6TTpk1r9V7OD1JdXZ1f/epXmTNnTnbYYYecffbZufjii1uNGThwYG699dY89NBD2X777XPsscfm6KOPzr/927+t9HlKpVJuvfXWfOITn8iRRx6ZLbbYIoccckheeOGFbLTRRit9HAAAgI7UqVbNrZQJEyZk5syZ7/pezDXV+62a+8+amppSW1tr1VwKYdXc1dfq9y56/i+r5gJQhE65au7UqVNTXV2dOXPmVDpKK7fddlsuueSSSsfoEJMmTUp1dXXmz59f6SgAAEAntcbMiL700ktZunRpkmTw4MHp3r17hRN1Ti+//HJefvnlJG+tElxbW/uBrzEjSpHMiK6+zIiu3syIAlCElZ0RXWNWzR04cGClI6wV+vXrl379+lU6BgAA0ImtUbfmAgAAsOZTRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQqDWmiDY0NKRUKqVUKmX27NmVjtPhJk6cmOHDh1c6Rurr68vf50WLFlU6DgAA0AmtMUU0ScaNG5fGxsYMGzYsSTJv3ryUSqXy89OmTUvfvn0/9Bz19fWZMWPGSo+fMWNG6uvrP7Q8q6KhoSHTpk0rbz/88MO58cYbKxcIAADo9LpVOkBb9OrVK3V1dZWO0altsMEG6devX6VjAAAAndgaNSP6fmbMmJEjjzwyixcvLt9aOnHixFx22WXlGdQkufnmm1MqlXLFFVeU9+255575t3/7t/L25Zdfns033zzdu3fPlltumWuvvbbD837zm9/MRhttlJqamhx99NFZtmxZq+dXrFiR888/PxtvvHGqqqoyfPjw/OY3vyk///Zs8E033ZTddtstvXr1yvbbb5/f/va3rY5z//33Z5dddknPnj0zaNCgnHjiiXn11VdXKXtzc3OamppaPQAAAFZWpymio0ePzpQpU9KnT580NjamsbExp556anbdddc8+eST+dvf/pYkmTlzZtZff/3yrbVvvPFGfvvb36ahoSFJ8otf/CInnXRSTjnllPz+97/PV7/61Rx55JG55557Oizrz3/+80ycODGTJk3K7373u/Tv3z9Tp05tNea73/1uLr300nzrW9/KE088kb333juf/exn88wzz7Qad/bZZ+fUU0/N7Nmzs8UWW+TQQw/Nm2++mSR57rnnss8+++Tzn/98nnjiiVx//fW5//7787WvfW2V8k+ePDm1tbXlx6BBg1bpeAAAwNql1NLS0lLpECujoaEhw4cPz5QpU95zzLRp0zJ+/PhWi+y0tLRkgw02yBVXXJEDDzwwO+ywQw4++OB897vfTWNjY2bNmpXddtstixYtSq9evTJmzJhss802ufLKK8vHOOigg/Lqq6/m17/+dYdcy+jRo7PDDjvkBz/4QXnfzjvvnGXLlpUXYho4cGBOOOGEfOMb3yiP2XHHHfOxj30sP/jBDzJv3rxsuummueqqq3L00UcnSZ588slss802mTt3brbaaqscc8wx6dq1a374wx+Wj3H//fdn1113zauvvpoePXq8a74ZM2Zkt912yz/+8Y93fc9tc3Nzmpuby9tNTU0ZNGhQeiYpvWM0dKwDKx2A97RBpQPwvtapdAAA1grNSb6TZPHixenTp897jus0M6LvpVQq5ROf+ERmzJiRRYsW5cknn8zxxx+f5ubm/PGPf8zMmTPzsY99LL169UqSzJ07N2PGjGl1jDFjxmTu3Lkdlmnu3LnZaaedWu0bNWpU+eumpqb8+c9/Xqkc2223Xfnr/v37J0kWLlyYJHn88cczbdq0VFdXlx977713VqxYkeeff77d+auqqtKnT59WDwAAgJW1Ri1W1F4NDQ258sorc99992WHHXZInz59yuV05syZ2XXXXSsdsd3WWed//8b99grCK1asSJIsWbIkX/3qV3PiiSe+43WDBw8uJiAAAMA/6VQzot27d8/y5cvfsf/t94n+13/9V/m9oA0NDbnrrrsya9as8r4kGTp0aGbNmtXq9bNmzcrWW2/dYTmHDh2aBx98sNW+Bx54oPx1nz59MmDAgFXOMWLEiDz55JMZMmTIOx7du3dftYsAAABop041I1pfX58lS5bk7rvvzvbbb59evXqlV69e2W677bLuuuvmuuuuyy233JLkrSJ66qmnplQqtboF9rTTTstBBx2UHXbYIXvuuWd+9atf5aabbspdd93VYTlPOumkjB07NiNHjsyYMWMyffr0/OEPf8hmm23WKseECROy+eabZ/jw4bnmmmsye/bsTJ8+faXPc8YZZ2TnnXfO1772tRxzzDHp3bt3nnzyydx555257LLLOux6AAAA2qJTzYiOHj06xx57bA4++OBssMEGueSSS5K8dcvqLrvsklKplI9//ONJ3npvZZ8+fTJy5Mj07t27fIz9998/3/3ud/Otb30r22yzTX74wx/mmmuuaTVr+s8aGhoyduzYlc558MEH55xzzsnpp5+ej370o3nhhRdy3HHHtRpz4okn5uSTT84pp5ySbbfdNr/5zW/y3//93/nIRz6y0ufZbrvtMnPmzDz99NPZZZddssMOO+Tcc8/NgAEDVvoYAAAAHa1TrZpbKZtssknOO++8NpXR1dkHrZr7z5qamlJbW2vVXAph1dzVl1VzV29WzQWgCJ1y1dypU6emuro6c+bMqXSUsj/84Q+pra3Nl7/85UpH6RDbbLNNPvnJT1Y6BgAA0ImtMTOiL730UpYuXZrkrRVfLbbz4XjhhRfyxhtvJEk222yzdOnywX+rMCNKkcyIrr7MiK7ezIgCUISVnRFdYxYrGjhwYKUjrBU22WSTSkcAAAA6uTXq1lwAAADWfIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEqWkQbGhpSKpVSKpUye/bsNr22vr4+U6ZM+VByVcK8efPa9X3oaBMnTiz/TDrT9xcAAFh9VHxGdNy4cWlsbMywYcOS/G8he9u0adPSt2/fCqV7dxMnTszYsWPb9Jr6+vrMmDHjQ8mzKqZNm5aGhoby9qmnnprGxsZsvPHGlQsFAAB0at0qHaBXr16pq6sr5FxvvPFG1llnnULOtaaqrq5OdXV1unbtWukoAABAJ1XxGdH3M2PGjBx55JFZvHhx+XbRiRMnlp9/7bXXctRRR6WmpiaDBw/OlVdeWX7u7ZnV66+/Prvuumt69OiR6dOnJ0muuuqqDB06ND169MhWW22VqVOntjrvggULctBBB6Vv377p169f9ttvv8ybN69Dr+2hhx7KDjvskB49emTkyJF57LHH3jFm5syZ2XHHHVNVVZX+/fvnzDPPzJtvvll+vqGhISeeeGJOP/309OvXL3V1da2+P0myaNGiHHPMMdlggw3Sp0+f7L777nn88cc79FoAAADaYrUuoqNHj86UKVPSp0+fNDY2prGxMaeeemr5+UsvvbRc4o4//vgcd9xxeeqpp1od48wzz8xJJ52UuXPnZu+998706dNz7rnn5qKLLsrcuXMzadKknHPOOfnxj3+c5K1Z07333js1NTW57777MmvWrFRXV2efffbJ66+/3iHXtWTJknzmM5/J1ltvnUceeSQTJ05sdV1J8tJLL+VTn/pUPvaxj+Xxxx/P5ZdfnquvvjoXXnhhq3E//vGP07t37zz44IO55JJLcv755+fOO+8sP/+FL3whCxcuzG233ZZHHnkkI0aMyB577JGXX3653fmbm5vT1NTU6gEAALCyKn5r7j+rr69PS0tLkqR79+6pra1NqVR619t3P/WpT+X4449Pkpxxxhn5zne+k3vuuSdbbrllecz48eNzwAEHlLcnTJiQSy+9tLxv0003zZNPPpkf/vCHOeKII3L99ddnxYoVueqqq8rvVb3mmmvSt2/fzJgxI3vttdc7Zh1Xxv+dUb3uuuuyYsWKXH311enRo0e22WabvPjiiznuuOPKY6ZOnZpBgwblsssuS6lUylZbbZU///nPOeOMM3LuueemS5e3/oaw3XbbZcKECUmSj3zkI7nsssty991351/+5V9y//3356GHHsrChQtTVVWVJPnWt76Vm2++OTfccEO+8pWvZOzYsW1+v+vkyZNz3nnntfl7AAAAkKyGRbQttttuu/LXb5fVhQsXthozcuTI8tevvvpqnnvuuRx99NEZN25cef+bb76Z2traJMnjjz+eZ599NjU1Na2Os2zZsjz33HMdknvu3LnZbrvt0qNHj/K+UaNGvWPMqFGjWi3cNGbMmCxZsiQvvvhiBg8enKT19yBJ+vfvX/4ePP7441myZEnWW2+9VmOWLl26Stdy1lln5eSTTy5vNzU1ZdCgQe0+HgAAsHZZo4voPy88VCqVsmLFilb7evfuXf56yZIlSZIf/ehH2WmnnVqNe3txniVLluSjH/1o+f2k/9cGG2zQIbk70vt9D5YsWZL+/fu/62q9q7IScVVVVXmGFQAAoK1W+yLavXv3LF++vEOOtdFGG2XAgAH505/+lMMOO+xdx4wYMSLXX399Ntxww/Tp06dDzvvPhg4dmmuvvTbLli0rz4o+8MAD7xhz4403pqWlpTwrOmvWrNTU1Kz0R6uMGDEif/nLX9KtW7fU19d36DUAAAC012q9WFHy1ntGlyxZkrvvvjt///vf89prr63S8c4777xMnjw53/ve9/L0009nzpw5ueaaa/Ltb387SXLYYYdl/fXXz3777Zf77rsvzz//fGbMmJETTzwxL774YkdcUr74xS+mVCpl3LhxefLJJ3PrrbfmW9/6Vqsxxx9/fBYsWJB//dd/zR//+Mf88pe/zIQJE3LyySeX3x/6Qfbcc8+MGjUq+++/f+64447Mmzcv//M//5Ozzz47v/vd7zrkWgAAANpqtS+io0ePzrHHHpuDDz44G2ywQS655JJVOt4xxxyTq666Ktdcc0223Xbb7Lrrrpk2bVo23XTTJG99rum9996bwYMH54ADDsjQoUNz9NFHZ9myZe85Qzpt2rRW7+X8INXV1fnVr36VOXPmZIcddsjZZ5+diy++uNWYgQMH5tZbb81DDz2U7bffPscee2yOPvro/Nu//dtKn6dUKuXWW2/NJz7xiRx55JHZYostcsghh+SFF17IRhtttNLHAQAA6EillreXqK2AhoaGDB8+PFOmTKlUhA4xYcKEzJw5813fi7mmqq+vz/jx4zN+/PgPHNvU1JTa2tr0TLLydRza58BKB+A9rX7vouf/WueDhwDAKmtO8p0kixcvft+3OlZ8RnTq1Kmprq7OnDlzKh2l3W677bZVnqldXUyaNCnV1dWZP39+paMAAACdVEVnRF966aUsXbo0STJ48OB07969UlH4/3v55Zfz8ssvJ3lrleC3P9bm/ZgRpUhmRFdfZkRXb2ZEASjCys6IVnTV3IEDB1by9LyLfv36pV+/fpWOAQAAdGIVvzUXAACAtYsiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCrdZFtKGhIaVSKaVSKbNnz37PcTfffHOGDBmSrl27Zvz48YXl60j19fWZMmVKRTPMmDGj/P3ef//9K5oFAADovFbrIpok48aNS2NjY4YNG5YkmTdvXkqlUqsxX/3qV3PggQdmwYIFueCCCz7UPDNmzEh9fX2bXjN27NhMnDjxQ8mzKv75ezl69Og0NjbmoIMOqmAqAACgs+tW6QAfpFevXqmrq3vP55csWZKFCxdm7733zoABAz7ULG+88caHevxK6969e+rq6tKzZ880NzdXOg4AANBJrfYzou9nxowZqampSZLsvvvuKZVKmTFjRpLkxhtvzDbbbJOqqqrU19fn0ksvbfXaUqmUm2++udW+vn37Ztq0aUn+d7bw+uuvz6677poePXpk+vTpHZJ74cKF2XfffdOzZ89suumm73rc+fPnZ7/99kt1dXX69OmTgw46KH/961/Lz0+cODHDhw/Ptddem/r6+tTW1uaQQw7JK6+8Uh6zYsWKTJ48OZtuuml69uyZ7bffPjfccEOHXAMAAEB7rdFFdPTo0XnqqaeSvFU8GxsbM3r06DzyyCM56KCDcsghh2TOnDmZOHFizjnnnHLJbIszzzwzJ510UubOnZu99967Q3KPHTs2CxYsyD333JMbbrghU6dOzcKFC8vPr1ixIvvtt19efvnlzJw5M3feeWf+9Kc/5eCDD251nOeeey4333xzbrnlltxyyy2ZOXNmvvnNb5afnzx5cn7yk5/kiiuuyB/+8Id8/etfz5e+9KXMnDlzlfI3Nzenqamp1QMAAGBlrfa35v6z+vr6tLS0JHnrVtINN9wwSdKvX7/yLbzf/va3s8cee+Scc85JkmyxxRZ58skn8+///u8ZO3Zsm843fvz4HHDAAeXt/v37Z968eW06xv8twE8//XRuu+22PPTQQ/nYxz6WJLn66qszdOjQ8pi77747c+bMyfPPP59BgwYlSX7yk59km222ycMPP1x+3YoVKzJt2rTyrPDhhx+eu+++OxdddFGam5szadKk3HXXXRk1alSSZLPNNsv999+fH/7wh9l1111bfS/bYvLkyTnvvPPa/DoAAIBkDZ8RfS9z587NmDFjWu0bM2ZMnnnmmSxfvrxNxxo5cmRHRsvcuXPTrVu3fPSjHy3v22qrrdK3b99WYwYNGlQuoUmy9dZbp2/fvpk7d255X319fbmEJm+V5LdnVp999tm89tpr+Zd/+ZdUV1eXHz/5yU/y3HPPrdI1nHXWWVm8eHH5sWDBglU6HgAAsHZZ42ZEO0qpVHrHbOC7LUbUu3fvoiK12TrrrNNqu1QqZcWKFUneWsQpSX79619n4MCBrcZVVVWt0nmrqqpW+RgAAMDaq1MW0aFDh2bWrFmt9s2aNStbbLFFunbtmiTZYIMN0tjYWH7+mWeeyWuvvfahZ9tqq63y5ptv5pFHHinfYvvUU09l0aJFrfIvWLAgCxYsKM+KPvnkk1m0aFG23nrrlTrP1ltvnaqqqsyfPz+77rprh18HAABAe3XKInrKKafkYx/7WC644IIcfPDB+e1vf5vLLrssU6dOLY/Zfffdc9lll2XUqFFZvnx5zjjjjHfMMH4Yttxyy+yzzz756le/mssvvzzdunXL+PHj07Nnz/KYPffcM9tuu20OO+ywTJkyJW+++WaOP/747Lrrrit9q3BNTU1OPfXUfP3rX8+KFSvy8Y9/PIsXL86sWbPSp0+fHHHEER/WJQIAALyvTvke0REjRuTnP/95fvazn2XYsGE599xzc/7557daqOjSSy/NoEGDsssuu+SLX/xiTj311PTq1avN53r7Y17e/tiYlXHNNddkwIAB2XXXXXPAAQfkK1/5SnnRpeStW2x/+ctfZt11180nPvGJ7Lnnntlss81y/fXXtynbBRdckHPOOSeTJ0/O0KFDs88+++TXv/51Nt100zYdBwAAoCOVWtqzbGpBGhoaMnz48EyZMqXSUd7TPffckwMOOCB/+tOfsu6661Y6TocYO3ZsFi1a9I7PWX0vTU1Nqa2tTc8kpQ81GSQHVjoA72mDSgfgfX349/wAQNKc5DtJFi9enD59+rznuNV+RnTq1Kmprq7OnDlzKh3lXd166635xje+0SlK6H333Zfq6upMnz690lEAAIBObLWeEX3ppZeydOnSJMngwYPTvXv3Cifq3JYuXZqXXnopSVJdXV3+XNYPYkaUIpkRXX2ZEV29mREFoAgrOyO6Wi9W9M8fO8KHq2fPnhkyZEilYwAAAJ3can9rLgAAAJ2LIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQq0xRbShoSGlUimlUimzZ89+z3E333xzhgwZkq5du2b8+PGZNm1a+vbtW1jO9poxY0ZKpVIWLVpU0Rxjx44tf59vvvnmimYBAAA6pzWmiCbJuHHj0tjYmGHDhiVJ5s2bl1Kp1GrMV7/61Rx44IFZsGBBLrjgghx88MF5+umnOzTH2LFjM3HixDa9plQqZd68eR2aoyNMnDgxY8eOLW9/97vfTWNjY+UCAQAAnV63Sgdoi169eqWuru49n1+yZEkWLlyYvffeOwMGDCjv79mzZxHxOoXa2trU1tZWOgYAANCJrVEzou9nxowZqampSZLsvvvuKZVKmTFjRqtbc59++umUSqX88Y9/bPXa73znO9l8883L27///e/zyU9+MtXV1dloo41y+OGH5+9//3uH5r311luzxRZbpGfPntltt93edbb0xhtvzDbbbJOqqqrU19fn0ksvbfV8fX19Jk2alKOOOio1NTUZPHhwrrzyylZjFixYkIMOOih9+/ZNv379st9++63yzGxzc3OamppaPQAAAFZWpymio0ePzlNPPZXkrQLX2NiY0aNHtxqzxRZbZOTIkZk+fXqr/dOnT88Xv/jFJMmiRYuy++67Z4cddsjvfve7/OY3v8lf//rXHHTQQR2WdcGCBTnggAOy7777Zvbs2TnmmGNy5plnthrzyCOP5KCDDsohhxySOXPmZOLEiTnnnHMybdq0VuMuvfTSjBw5Mo899liOP/74HHfcceXvwxtvvJG99947NTU1ue+++zJr1qxUV1dnn332yeuvv97u/JMnTy7PnNbW1mbQoEHtPhYAALD2KbW0tLRUOsTKaGhoyPDhwzNlypT3HLNo0aKsu+66ueeee9LQ0JAkmTZtWsaPH19eBGjKlCm57LLL8uyzzyZ5a5Z0yy23zNy5c7PVVlvlwgsvzH333Zfbb7+9fNwXX3wxgwYNylNPPZUttthila/lG9/4Rn75y1/mD3/4Q3nfmWeemYsvvjj/+Mc/0rdv3xx22GH529/+ljvuuKM85vTTT8+vf/3r8uvq6+uzyy675Nprr02StLS0pK6uLuedd16OPfbY/PSnP82FF16YuXPnlt9L+/rrr6dv3765+eabs9dee71nxlKplF/84hfZf//93/Fcc3Nzmpuby9tNTU0ZNGhQeiYpvWM0dKwDKx2A97RBpQPwvtapdAAA1grNSb6TZPHixenTp897jus0M6Ir65BDDsm8efPywAMPJHlrNnTEiBHZaqutkiSPP/547rnnnlRXV5cfbz/33HPPdUiGuXPnZqeddmq1b9SoUe8YM2bMmFb7xowZk2eeeSbLly8v79tuu+3KX5dKpdTV1WXhwoXla3n22WdTU1NTvpZ+/fpl2bJlq3QtVVVV6dOnT6sHAADAylqjFivqCHV1ddl9991z3XXXZeedd851112X4447rvz8kiVLsu++++biiy9+x2v79+9fZNSVss46rf/GXSqVsmLFiiRvXctHP/rRd9yKnCQbbGDuAgAAqIy1rogmyWGHHZbTTz89hx56aP70pz/lkEMOKT83YsSI3Hjjjamvr0+3bh/Ot2fo0KH57//+71b73p6h/b9jZs2a1WrfrFmzssUWW6Rr164rdZ4RI0bk+uuvz4YbbmjWEgAAWG2sdbfmJskBBxyQV155Jccdd1x22223Vh/1csIJJ+Tll1/OoYcemocffjjPPfdcbr/99hx55JGtboldFccee2yeeeaZnHbaaXnqqady3XXXvWMRolNOOSV33313Lrjggjz99NP58Y9/nMsuuyynnnrqSp/nsMMOy/rrr5/99tsv9913X55//vnMmDEjJ554Yl588cUOuRYAAIC2WiuLaE1NTfbdd988/vjjOeyww1o9N2DAgMyaNSvLly/PXnvtlW233Tbjx49P375906XLu3+7Jk6cmPr6+pU+/+DBg3PjjTfm5ptvzvbbb58rrrgikyZNajVmxIgR+fnPf56f/exnGTZsWM4999ycf/75GTt27Eqfp1evXrn33nszePDgHHDAARk6dGiOPvroLFu2zAwpAABQMZ1q1dxKOeKII1Iqld4xq7kme79Vc/9ZU1NTamtrrZpLIayau/ryzvPVm1VzAShCp1w1d+rUqamurs6cOXMqHaWspaUlM2bMyAUXXFDpKB3i2GOPTXV1daVjAAAAndgaMyP60ksvZenSpUneurW1e/fuFU7UOS1cuDBNTU1J3loluHfv3h/4GjOiFMmM6OrLjOjqzYwoAEVY2RnRNWbV3IEDB1Y6wlphww03zIYbbljpGAAAQCe2Rt2aCwAAwJpPEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAolCIKAABAoRRRAAAACqWIAgAAUChFFAAAgEIpogAAABRKEQUAAKBQiigAAACFUkQBAAAo1BpfRBsaGlIqlVIqlTJ79uw2v37GjBkplUpZtGhRh2dri7Fjx2b//fevaIYk5e9l3759Kx0FAADopNb4Ipok48aNS2NjY4YNG5YkmTdvXkql0kq9dvTo0WlsbExtbe1Kn69UKmXevHkrPX7atGlpaGhY6fFFqq+vz4wZM8rbjY2NmTJlSsXyAAAAnV+3SgfoCL169UpdXV27Xtu9e/d2v7Yzqqura1MpBwAAaKtOMSP6QV544YXsu+++WXfdddO7d+9ss802ufXWW5O889bco446Ktttt12am5uTJK+//np22GGHfPnLX+6wPMuXL8/JJ5+cvn37Zr311svpp5+elpaWVmOam5tz4oknZsMNN0yPHj3y8Y9/PA8//HD5+bdz33333Rk5cmR69eqV0aNH56mnnmp1nF/+8pcZMWJEevTokc022yznnXde3nzzzQ67FgAAgLZaK4roCSeckObm5tx7772ZM2dOLr744lRXV7/r2O9973t59dVXc+aZZyZJzj777CxatCiXXXZZh+W59NJLM23atPzHf/xH7r///rz88sv5xS9+0WrM6aefnhtvvDE//vGP8+ijj2bIkCHZe++98/LLL7cad/bZZ+fSSy/N7373u3Tr1i1HHXVU+bn77rsvX/7yl3PSSSflySefzA9/+MNMmzYtF1100Srlb25uTlNTU6sHAADAyuoUt+b+s/r6+lYzjPPnz8/nP//5bLvttkmSzTbb7D1fW11dnZ/+9KfZddddU1NTkylTpuSee+5Jnz59ymP+efbyg4wdOzZjx44tb0+ZMiVnnXVWDjjggCTJFVdckdtvv738/KuvvprLL78806ZNyyc/+ckkyY9+9KPceeedufrqq3PaaaeVx1500UXZddddkyRnnnlmPv3pT2fZsmXp0aNHzjvvvJx55pk54ogjytd9wQUX5PTTT8+ECROSpE3vdX3b5MmTc95557X5dQAAAMlaMiN64okn5sILL8yYMWMyYcKEPPHEE+87ftSoUTn11FNzwQUX5JRTTsnHP/7xDsuyePHiNDY2Zqeddirv69atW0aOHFnefu655/LGG29kzJgx5X3rrLNOdtxxx8ydO7fV8bbbbrvy1/3790+SLFy4MEny+OOP5/zzz091dXX58fbCTq+99lq7r+Gss87K4sWLy48FCxa0+1gAAMDaZ60oosccc0z+9Kc/5fDDD8+cOXMycuTIfP/733/P8StWrMisWbPStWvXPPvsswUmbbt11lmn/PXbKwWvWLEiSbJkyZKcd955mT17dvkxZ86cPPPMM+nRo0e7z1lVVZU+ffq0egAAAKystaKIJsmgQYNy7LHH5qabbsopp5ySH/3oR+859t///d/zxz/+MTNnzsxvfvObXHPNNR2Wo7a2Nv3798+DDz5Y3vfmm2/mkUceKW9vvvnm6d69e2bNmlXe98Ybb+Thhx/O1ltvvdLnGjFiRJ566qkMGTLkHY8uXdaaHz0AALCa6ZTvEf1n48ePzyc/+clsscUW+cc//pF77rknQ4cOfdexjz32WM4999zccMMNGTNmTL797W/npJNOyq677vq+7y1ti5NOOinf/OY385GPfCRbbbVVvv3tb5dX7U2S3r1757jjjstpp52Wfv36ZfDgwbnkkkvy2muv5eijj17p85x77rn5zGc+k8GDB+fAAw9Mly5d8vjjj+f3v/99Lrzwwg65FgAAgLZaK6bFli9fnhNOOCFDhw7NPvvsky222CJTp059x7hly5blS1/6UsaOHZt99903SfKVr3wlu+22Ww4//PAsX778XY9fX1+fiRMnrnSeU045JYcffniOOOKIjBo1KjU1Nfnc5z7Xasw3v/nNfP7zn8/hhx+eESNG5Nlnn83tt9+eddddd6XPs/fee+eWW27JHXfckY997GPZeeed853vfCebbLLJSh8DAACgo5Va2roE7GqmoaEhw4cPz5QpUypy/tdeey3rrbdebrvttjQ0NFQkQ0ebNm1axo8f32qW9v00NTWltrY2PZOUPtRkkBxY6QC8pw0qHYD3tc4HDwGAVdac5Dt5a5HW91tLplPMiE6dOjXV1dWZM2dO4ee+5557svvuu3eaElpdXZ1jjz220jEAAIBObI2fEX3ppZeydOnSJMngwYPTvXv3Cidas729SnDXrl2z6aabrtRrzIhSJDOiqy8zoqs3M6IAFGFlZ0TX+MWKBg4cWOkIncqQIUMqHQEAAOjkOsWtuQAAAKw5FFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIVSRAEAACiUIgoAAEChFFEAAAAKpYgCAABQKEUUAACAQimiAAAAFEoRBQAAoFCKKAAAAIXqVukArPlaWlre+r8VzsHa4fVKB+A9NVc6AO9rRaUDALBWePv3gbc7wntRRFllr7zySpJkWYVzsHb4WaUDAADwgV555ZXU1ta+5/Ollg+qqvABVqxYkT//+c+pqalJqVT60M7T1NSUQYMGZcGCBenTp8+Hdp4idKZrSVzP6qwzXUvielZnnelaEtezOutM15K4ntVZZ7qWpLjraWlpySuvvJIBAwakS5f3fieoGVFWWZcuXbLxxhsXdr4+ffp0iv8xSDrXtSSuZ3XWma4lcT2rs850LYnrWZ11pmtJXM/qrDNdS1LM9bzfTOjbLFYEAABAoRRRAAAACqWIssaoqqrKhAkTUlVVVekoq6wzXUvielZnnelaEtezOutM15K4ntVZZ7qWxPWszjrTtSSr3/VYrAgAAIBCmREFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUdYIP/jBD1JfX58ePXpkp512ykMPPVTpSO127733Zt99982AAQNSKpVy8803VzpSu02ePDkf+9jHUlNTkw033DD7779/nnrqqUrHapfLL7882223XflDnkeNGpXbbrut0rE6zDe/+c2USqWMHz++0lHaZeLEiSmVSq0eW221VaVjtdtLL72UL33pS1lvvfXSs2fPbLvttvnd735X6VjtUl9f/46fTalUygknnFDpaO2yfPnynHPOOdl0003Ts2fPbL755rnggguypq7t+Morr2T8+PHZZJNN0rNnz4wePToPP/xwpWOtlA/697KlpSXnnntu+vfvn549e2bPPffMM888U5mwK+GDruemm27KXnvtlfXWWy+lUimzZ8+uSM6V8X7X8sYbb+SMM87Itttum969e2fAgAH58pe/nD//+c+VC/wBPuhnM3HixGy11Vbp3bt31l133ey555558MEHKxN2JbTld81jjz02pVIpU6ZMKSzf2xRRVnvXX399Tj755EyYMCGPPvpott9+++y9995ZuHBhpaO1y6uvvprtt98+P/jBDyodZZXNnDkzJ5xwQh544IHceeedeeONN7LXXnvl1VdfrXS0Ntt4443zzW9+M4888kh+97vfZffdd89+++2XP/zhD5WOtsoefvjh/PCHP8x2221X6SirZJtttkljY2P5cf/991c6Urv84x//yJgxY7LOOuvktttuy5NPPplLL7006667bqWjtcvDDz/c6udy5513Jkm+8IUvVDhZ+1x88cW5/PLLc9lll2Xu3Lm5+OKLc8kll+T73/9+paO1yzHHHJM777wz1157bebMmZO99tore+65Z1566aVKR/tAH/Tv5SWXXJLvfe97ueKKK/Lggw+md+/e2XvvvbNs2bKCk66cD7qeV199NR//+Mdz8cUXF5ys7d7vWl577bU8+uijOeecc/Loo4/mpptuylNPPZXPfvazFUi6cj7oZ7PFFlvksssuy5w5c3L//fenvr4+e+21V/72t78VnHTlrOzvmr/4xS/ywAMPZMCAAQUl+yctsJrbcccdW0444YTy9vLly1sGDBjQMnny5Aqm6hhJWn7xi19UOkaHWbhwYUuSlpkzZ1Y6SodYd911W6666qpKx1glr7zySstHPvKRljvvvLNl1113bTnppJMqHaldJkyY0LL99ttXOkaHOOOMM1o+/vGPVzrGh+akk05q2XzzzVtWrFhR6Sjt8ulPf7rlqKOOarXvgAMOaDnssMMqlKj9XnvttZauXbu23HLLLa32jxgxouXss8+uUKr2+ed/L1esWNFSV1fX8u///u/lfYsWLWqpqqpq+c///M8KJGyb9/v3//nnn29J0vLYY48Vmqm9VuZ3mYceeqglScsLL7xQTKhVsDLXs3jx4pYkLXfddVcxoVbBe13Piy++2DJw4MCW3//+9y2bbLJJy3e+853Cs5kRZbX2+uuv55FHHsmee+5Z3telS5fsueee+e1vf1vBZLybxYsXJ0n69etX4SSrZvny5fnZz36WV199NaNGjap0nFVywgkn5NOf/nSr/x9aUz3zzDMZMGBANttssxx22GGZP39+pSO1y3//939n5MiR+cIXvpANN9wwO+ywQ370ox9VOlaHeP311/PTn/40Rx11VEqlUqXjtMvo0aNz99135+mnn06SPP7447n//vvzyU9+ssLJ2u7NN9/M8uXL06NHj1b7e/bsucbeUfC2559/Pn/5y19a/W9bbW1tdtppJ78frIYWL16cUqmUvn37VjrKKnv99ddz5ZVXpra2Nttvv32l47TLihUrcvjhh+e0007LNttsU7Ec3Sp2ZlgJf//737N8+fJstNFGrfZvtNFG+eMf/1ihVLybFStWZPz48RkzZkyGDRtW6TjtMmfOnIwaNSrLli1LdXV1fvGLX2TrrbeudKx2+9nPfpZHH310jXk/2PvZaaedMm3atGy55ZZpbGzMeeedl1122SW///3vU1NTU+l4bfKnP/0pl19+eU4++eR84xvfyMMPP5wTTzwx3bt3zxFHHFHpeKvk5ptvzqJFizJ27NhKR2m3M888M01NTdlqq63StWvXLF++PBdddFEOO+ywSkdrs5qamowaNSoXXHBBhg4dmo022ij/+Z//md/+9rcZMmRIpeOtkr/85S9J8q6/H7z9HKuHZcuW5Ywzzsihhx6aPn36VDpOu91yyy055JBD8tprr6V///658847s/7661c6VrtcfPHF6datW0488cSK5lBEgQ5xwgkn5Pe///0a/Vf2LbfcMrNnz87ixYtzww035IgjjsjMmTPXyDK6YMGCnHTSSbnzzjvfMRuyJvq/s1Hbbbdddtppp2yyySb5+c9/nqOPPrqCydpuxYoVGTlyZCZNmpQk2WGHHfL73/8+V1xxxRpfRK+++up88pOfrNz7jTrAz3/+80yfPj3XXXddttlmm8yePTvjx4/PgAED1sifz7XXXpujjjoqAwcOTNeuXTNixIgceuiheeSRRyodjbXAG2+8kYMOOigtLS25/PLLKx1nley2226ZPXt2/v73v+dHP/pRDjrooDz44IPZcMMNKx2tTR555JF897vfzaOPPlrxO1fcmstqbf3110/Xrl3z17/+tdX+v/71r6mrq6tQKv7Z1772tdxyyy255557svHGG1c6Trt17949Q4YMyUc/+tFMnjw522+/fb773e9WOla7PPLII1m4cGFGjBiRbt26pVu3bpk5c2a+973vpVu3blm+fHmlI66Svn37Zosttsizzz5b6Sht1r9//3f8cWPo0KFr7K3Gb3vhhRdy11135Zhjjql0lFVy2mmn5cwzz8whhxySbbfdNocffni+/vWvZ/LkyZWO1i6bb755Zs6cmSVLlmTBggV56KGH8sYbb2SzzTardLRV8vbvAH4/WH29XUJfeOGF3HnnnWv0bGiS9O7dO0OGDMnOO++cq6++Ot26dcvVV19d6Vhtdt9992XhwoUZPHhw+feDF154Iaecckrq6+sLzaKIslrr3r17PvrRj+buu+8u71uxYkXuvvvuNf69e51BS0tLvva1r+UXv/hF/t//+3/ZdNNNKx2pQ61YsSLNzc2VjtEue+yxR+bMmZPZs2eXHyNHjsxhhx2W2bNnp2vXrpWOuEqWLFmS5557Lv379690lDYbM2bMOz7m6Omnn84mm2xSoUQd45prrsmGG26YT3/605WOskpee+21dOnS+tejrl27ZsWKFRVK1DF69+6d/v375x//+Eduv/327LfffpWOtEo23XTT1NXVtfr9oKmpKQ8++KDfD1YDb5fQZ555JnfddVfWW2+9SkfqcGvq7wiHH354nnjiiVa/HwwYMCCnnXZabr/99kKzuDWX1d7JJ5+cI444IiNHjsyOO+6YKVOm5NVXX82RRx5Z6WjtsmTJklazOM8//3xmz56dfv36ZfDgwRVM1nYnnHBCrrvuuvzyl79MTU1N+X05tbW16dmzZ4XTtc1ZZ52VT37ykxk8eHBeeeWVXHfddZkxY0bh/6PcUWpqat7xXt3evXtnvfXWWyPfw3vqqadm3333zSabbJI///nPmTBhQrp27ZpDDz200tHa7Otf/3pGjx6dSZMm5aCDDspDDz2UK6+8MldeeWWlo7XbihUrcs011+SII45It25r9q8W++67by666KIMHjw422yzTR577LF8+9vfzlFHHVXpaO1y++23p6WlJVtuuWWeffbZnHbaadlqq63WiH9DP+jfy/Hjx+fCCy/MRz7ykWy66aY555xzMmDAgOy///6VC/0+Puh6Xn755cyfP7/8eZtv/8Gqrq5utZvlfb9r6d+/fw488MA8+uijueWWW7J8+fLy7wf9+vVL9+7dKxX7Pb3f9ay33nq56KKL8tnPfjb9+/fP3//+9/zgBz/ISy+9tNp+TNUH/bf2z38YWGeddVJXV5ctt9yy2KCFr9ML7fD973+/ZfDgwS3du3dv2XHHHVseeOCBSkdqt3vuuaclyTseRxxxRKWjtdm7XUeSlmuuuabS0drsqKOOatlkk01aunfv3rLBBhu07LHHHi133HFHpWN1qDX541sOPvjglv79+7d07969ZeDAgS0HH3xwy7PPPlvpWO32q1/9qmXYsGEtVVVVLVtttVXLlVdeWelIq+T2229vSdLy1FNPVTrKKmtqamo56aSTWgYPHtzSo0ePls0226zl7LPPbmlubq50tHa5/vrrWzbbbLOW7t27t9TV1bWccMIJLYsWLap0rJXyQf9erlixouWcc85p2WijjVqqqqpa9thjj9X6v8EPup5rrrnmXZ+fMGFCRXO/m/e7lrc/fubdHvfcc0+lo7+r97uepUuXtnzuc59rGTBgQEv37t1b+vfv3/LZz3625aGHHqp07PfU1t81K/XxLaWWlpaWjq+3AAAA8O68RxQAAIBCKaIAAAAUShEFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAwPsaO3Zs9t9//0rHAKATUUQBAAAolCIKACRJbrjhhmy77bbp2bNn1ltvvey555457bTT8uMf/zi//OUvUyqVUiqVMmPGjCTJggULctBBB6Vv377p169f9ttvv8ybN698vLdnUs8777xssMEG6dOnT4499ti8/vrr73vOV199teArB6Bo3SodAACovMbGxhx66KG55JJL8rnPfS6vvPJK7rvvvnz5y1/O/Pnz09TUlGuuuSZJ0q9fv7zxxhvZe++9M2rUqNx3333p1q1bLrzwwuyzzz554okn0r179yTJ3XffnR49emTGjBmZN29ejjzyyKy33nq56KKL3vOcLS0tlfxWAFAARRQASGNjY958880ccMAB2WSTTZIk2267bZKkZ8+eaW5uTl1dXXn8T3/606xYsSJXXXVVSqVSkuSaa65J3759M2PGjOy1115Jku7du+c//uM/0qtXr2yzzTY5//zzc9ppp+WCCy5433MC0Lm5NRcAyPbbb5899tgj2267bb7whS/kRz/6Uf7xj3+85/jHH388zz77bGpqalJdXZ3q6ur069cvy5Yty3PPPdfquL169Spvjxo1KkuWLMmCBQvafE4AOg9FFABI165dc+edd+a2227L1ltvne9///vZcsst8/zzz7/r+CVLluSjH/1oZs+e3erx9NNP54tf/OKHck4AOg9FFABIkpRKpYwZMybnnXdeHnvssXTv3j2/+MUv0r179yxfvrzV2BEjRuSZZ57JhhtumCFDhrR61NbWlsc9/vjjWbp0aXn7gQceSHV1dQYNGvS+5wSgc1NEAYA8+OCDmTRpUn73u99l/vz5uemmm/K3v/0tQ4cOTX19fZ544ok89dRT+fvf/5433ngjhx12WNZff/3st99+ue+++/L8889nxowZOfHEE/Piiy+Wj/v666/n6KOPzpNPPplbb701EyZMyNe+9rV06dLlfc8JQOdmsSIAIH369Mm9996bKVOmpKmpKZtsskkuvfTSfPKTn8zIkSMzY8aMjBw5MkuWLMk999yThoaG3HvvvTnjjDNywAEH5JVXXsnAgQOzxx57pE+fPuXj7rHHHvnIRz6ST3ziE2lubs6hhx6aiRMnfuA5AejcSi3WSAcAPgRjx47NokWLcvPNN1c6CgCrGbfmAgAAUChFFAAAgEK5NRcAAIBCmREFAACgUIooAAAAhVJEAQAAKJQiCgAAQKEUUQAAAAqliAIAAFAoRRQAAIBCKaIAAAAU6v8Hn/jMkiPysIwAAAAASUVORK5CYII=",
"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-04-24T14:31:55.155600Z",
"iopub.status.busy": "2025-04-24T14:31:55.155302Z",
"iopub.status.idle": "2025-04-24T14:31:55.159193Z",
"shell.execute_reply": "2025-04-24T14:31:55.158775Z"
}
},
"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.12.3"
},
"widgets": {
"application/vnd.jupyter.widget-state+json": {
"state": {
"01c064189ee94a3196570f07eab318cb": {
"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_db1054a5236e4c4bbd805f4f827cc6c6",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"148e81f1bc1e4bf48b002f5524939039": {
"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_6df4aa7ebc024f55ac2e74fc35539851",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"2590b013567b495f96f95e330a937769": {
"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_fc3f7bbf61274d1c9846186ad09e866f",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"25dade5fea08454a842c4e1da0525908": {
"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
}
},
"42c14fcc90864654ad37aeed26eb1107": {
"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_af455b67ad5d47bc87f4394344cbd986",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"4f2de7047d0a497e85fee5da095ad2e9": {
"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
}
},
"58941e55421d4b84afbfe38e62c83e2b": {
"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_f72849e23b5e4eb08a38ab71aeca23da",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"62d0cbd4f8f14d178a1f28405d2513de": {
"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
}
},
"638083a9fabf47899b4c285a93bca997": {
"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
}
},
"6565cf9d70a14f4e9cafd2123b709987": {
"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
}
},
"6df4aa7ebc024f55ac2e74fc35539851": {
"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
}
},
"6ed717ea24bb483f8afb5cdcb0551c3d": {
"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_25dade5fea08454a842c4e1da0525908",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"6f71bc29bd5440aa83b224667ef5d7fb": {
"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
}
},
"81cd6de7edda47d0898b06d4fb63ff5e": {
"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_f2712db1ff024dc6a4e32a3c2a917dc4",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"8c2be90425a94f1197579e0f4d2ba5b4": {
"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
}
},
"8eb17020f7a24d328b8e4860b4b73a81": {
"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
}
},
"8f051a3fa07d40f1a8ebceb77e2a40e7": {
"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_4f2de7047d0a497e85fee5da095ad2e9",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"8f3d3183cc7844b2888992d28f48b08c": {
"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_62d0cbd4f8f14d178a1f28405d2513de",
"msg_id": "",
"outputs": [
{
"data": {
"text/html": "\n\n\n \n Network\n \n \n \n \n \n \n \n \n\n",
"text/plain": ""
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"9858216b8fe340caaac69afa0b28d2f5": {
"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_638083a9fabf47899b4c285a93bca997",
"msg_id": "",
"outputs": [
{
"data": {
"text/html": "\n\n\n \n Network\n \n \n \n \n \n \n \n \n\n",
"text/plain": ""
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"9f750447597943c291217d5903bc70c2": {
"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
}
},
"af455b67ad5d47bc87f4394344cbd986": {
"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
}
},
"afdc64f9986b45478e1e759fba13f92e": {
"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_6565cf9d70a14f4e9cafd2123b709987",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"b664894a41424fa58d2ee10bd3a9e9ca": {
"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_9f750447597943c291217d5903bc70c2",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"db1054a5236e4c4bbd805f4f827cc6c6": {
"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
}
},
"dc1f0d8f72c74ba5b014bbfa02850528": {
"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_8c2be90425a94f1197579e0f4d2ba5b4",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"ef9d13a86671442197be3d1888781bff": {
"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_6f71bc29bd5440aa83b224667ef5d7fb",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"f2712db1ff024dc6a4e32a3c2a917dc4": {
"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
}
},
"f72849e23b5e4eb08a38ab71aeca23da": {
"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
}
},
"fc3f7bbf61274d1c9846186ad09e866f": {
"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
}
},
"fdabe69c5a4a435ca1d39d9fb093b5a8": {
"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_8eb17020f7a24d328b8e4860b4b73a81",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}