{
"cells": [
{
"cell_type": "markdown",
"id": "8629322434f944b2",
"metadata": {},
"source": [
"# Building DTMCs\n",
"In Stormvogel, a **Discrete Time Markov Chain (DTMC)** consists of:\n",
"* a set of states $S$,\n",
"* an initial state $s_0$,\n",
"* a successor distribution $P(s)$ for every state $s$, i.e., transitions between states $s$ and $s'$, each annotated with a probability.\n",
"* state labels $L(s)$.\n",
"\n",
"In this notebook, we demonstrate how to construct two simple DTMCs from various sources. We show how to construct a model using the `pgc` API and the `model` API. Do note that stormvogel supports seemless conversion to and from stormpy. This means that you can also use any way of buidling models that is supported by stormpy. This includes [PRISM](https://www.prismmodelchecker.org/), [JANI](https://www.stormchecker.org/files/BDHHJT17.pdf) and [stormpy's own APIs](https://moves-rwth.github.io/stormpy/). For these, we refer to their respective documentations.\n",
"\n",
"**Note:** unfortunately, the visualisation of the DTMC is not always correct when it is rendered out of view. To re-center, you can simply double-click inside the window."
]
},
{
"cell_type": "markdown",
"id": "f2dd9ace-06db-41ab-a9db-b3fc11bda1d2",
"metadata": {},
"source": [
"## The Knuth die\n",
"The idea of the Knuth die is to simulate a 6-sided die using coin flips. It is widely used in model checking education."
]
},
{
"cell_type": "markdown",
"id": "e9afb2d9-afff-49c1-b522-86cff0ea5579",
"metadata": {},
"source": [
"### PGC API\n",
"The PGC API is probably the most intuitive way to create a model. The user defines a `delta` function which maps a state to a distribution of successor states. Its design was inspired by the PRISM format."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "abed08f9-9381-4cf1-97b6-582f8a7a7cfb",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-18T15:14:09.207622Z",
"iopub.status.busy": "2025-08-18T15:14:09.207452Z",
"iopub.status.idle": "2025-08-18T15:14:13.384713Z",
"shell.execute_reply": "2025-08-18T15:14:13.384142Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "4e6a088f16484e27aa29af56cf45e491",
"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', 'PcbtppXwrgdDYjQzbJze', 'test message')"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"Test request failed. See 'Implementation details' in docs. Disable warning by use_server=False.\n"
]
},
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"from stormvogel import *\n",
"\n",
"# Create an initial state. States can be of any type. In this case we use integers.\n",
"init = 0\n",
"\n",
"TRANSITIONS = \\\n",
"{0: [(1/2, 1), (1/2, 2)],\n",
" 1: [(1/2, 3), (1/2, 4)],\n",
" 2: [(1/2, 5), (1/2, 6)],\n",
" 3: [(1/2, 1), (1/2, 7)],\n",
" 4: [(1/2, 8), (1/2, 9)],\n",
" 5: [(1/2, 10), (1/2, 11)],\n",
" 6: [(1/2, 2), (1/2, 12)]}\n",
"\n",
"# This user-defined delta function takes as an argument a single state, and returns a \n",
"# list of 2-tuples where the first argument is a probability and the second elment is a state (a distribution).\n",
"def delta(s):\n",
" if s <= 6:\n",
" return TRANSITIONS[s]\n",
" return [(1, s)]\n",
" \n",
"# Labels is a function that tells the pgc API what the label should be for a state.\n",
"def labels(s):\n",
" if s <= 6:\n",
" return [str(s)]\n",
" return [\"r\", str(s-6)]\n",
"\n",
"pgc_die = pgc.build_pgc(\n",
" delta=delta,\n",
" initial_state_pgc=init,\n",
" labels=labels,\n",
" modeltype=ModelType.DTMC\n",
")\n",
"vis = show(pgc_die, layout=Layout(\"layouts/die.json\"))"
]
},
{
"cell_type": "markdown",
"id": "b5e502f1-dfbe-4362-87eb-01d3ceba2900",
"metadata": {},
"source": [
"### model API\n",
"This same model can also be constructed using the model API. This API requires adding each state and transition explicitly. This is a lot closer to how the models are represented in stormvogel. The pgc API actually uses the model API internally. We generally recommend just using the pgc API, but if you need more control, the model API can also be useful."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "3997a176dfebb345",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-18T15:14:13.396748Z",
"iopub.status.busy": "2025-08-18T15:14:13.396582Z",
"iopub.status.idle": "2025-08-18T15:14:13.433929Z",
"shell.execute_reply": "2025-08-18T15:14:13.433325Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "d8d52cd35d214175bcb25c7eb5706f19",
"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": [
"# If we use the model API, we need to create all states and transitions explicitly.\n",
"# Note the re-use of TRANSITIONS and labels which we defined previously.\n",
"\n",
"# Create a new model with an initial state with id 0.\n",
"die_model = stormvogel.model.new_dtmc(create_initial_state=True)\n",
"init = die_model.get_initial_state()\n",
"\n",
"# Create all the states (need 12 more to have 13 in total).\n",
"for sid in range(1,13):\n",
" die_model.new_state(labels(sid))\n",
"\n",
"# Create all the transitions\n",
"for k,v in TRANSITIONS.items():\n",
" state = die_model.get_state_by_id(k) # Get the state with id k\n",
" if k <= 6:\n",
" state.set_transitions(\n",
" [(p,die_model.get_state_by_id(sid)) for p,sid in TRANSITIONS[k]])\n",
"\n",
"die_model.add_self_loops() # Of course, we could also add the self-loops explicitly like in the previous example.\n",
"vis2 = show(die_model, layout=Layout(\"layouts/die.json\"))"
]
},
{
"cell_type": "markdown",
"id": "2dbc8dcd-d1d9-45d0-a412-5ea726cc7f2d",
"metadata": {},
"source": [
"## Simple communication\n",
"This example is based on slides by Dave Parker and Ralf Wimmer. It models a very simple communication protocol. This time we use the string type for states."
]
},
{
"cell_type": "markdown",
"id": "88bc870c-fbdf-4011-ab1e-7c0927c40013",
"metadata": {},
"source": [
"### PGC API"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "e0f09aac-7248-4b91-8883-0d7961425745",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-18T15:14:13.442333Z",
"iopub.status.busy": "2025-08-18T15:14:13.442180Z",
"iopub.status.idle": "2025-08-18T15:14:13.478838Z",
"shell.execute_reply": "2025-08-18T15:14:13.478077Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "8b7d8cc96ab14db2b26af3adb318174b",
"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": [
"def delta(s):\n",
" match s:\n",
" case \"zero\":\n",
" return [(1, \"one\")]\n",
" case \"one\":\n",
" return [(0.01, \"one\"), (0.01, \"two\"), (0.98, \"three\")]\n",
" case \"two\":\n",
" return [(1, \"zero\")]\n",
" case \"three\":\n",
" return [(1, \"three\")]\n",
"\n",
"def labels(s):\n",
" match s:\n",
" case \"one\":\n",
" return [\"try\"]\n",
" case \"two\":\n",
" return [\"fail\"]\n",
" case \"three\":\n",
" return [\"success\"]\n",
" case _:\n",
" return []\n",
"\n",
"pgc_commu = pgc.build_pgc(\n",
" delta=delta,\n",
" initial_state_pgc=\"zero\",\n",
" labels=labels,\n",
" modeltype=ModelType.DTMC\n",
")\n",
"vis3 = show(pgc_commu, layout=Layout(\"layouts/commu.json\"))"
]
},
{
"cell_type": "markdown",
"id": "e6a72df2-caa5-485d-9819-2f706e06e262",
"metadata": {},
"source": [
"### model API"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "246a9259-5dc8-438c-aeb6-e88a7fb6cfcc",
"metadata": {
"execution": {
"iopub.execute_input": "2025-08-18T15:14:13.489015Z",
"iopub.status.busy": "2025-08-18T15:14:13.488771Z",
"iopub.status.idle": "2025-08-18T15:14:13.525620Z",
"shell.execute_reply": "2025-08-18T15:14:13.525089Z"
}
},
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "2a110212219746399f87ef382566aa73",
"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": [
"commu_model = stormvogel.model.new_dtmc(create_initial_state=True)\n",
"init = die_model.get_initial_state()\n",
"\n",
"TRANSITIONS =\\\n",
"{0: [(1, 1)],\n",
" 1: [(0.01, 1), (0.01, 2), (0.98, 3)],\n",
" 2: [(1, 0)],\n",
" 3: [(1, 3)]}\n",
"\n",
"LABELS =\\\n",
"{0: [],\n",
" 1: [\"try\"],\n",
" 2: [\"fail\"],\n",
" 3: [\"success\"]} \n",
"\n",
"for sid in range(1,4):\n",
" commu_model.new_state(LABELS[sid])\n",
"\n",
"for sid in range(0,4):\n",
" state = commu_model.get_state_by_id(sid)\n",
" state.set_transitions(\n",
" [(p,die_model.get_state_by_id(sid_)) for p,sid_ in TRANSITIONS[sid]])\n",
"\n",
"vis4 = show(commu_model, layout=Layout(\"layouts/commu.json\"))"
]
},
{
"cell_type": "code",
"execution_count": null,
"id": "ba7f4ef9-d4fd-4f89-84a7-813bcd37c801",
"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": {
"0c34973d934a4e6aaf47aa1ecf0a4707": {
"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_281808f29e7f41b092ef181bb3dfdc46",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"0d13443ebb31408ab471bcc4e728cd92": {
"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_b2686a6f72d247a9b43807f7b108e6fc",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "523b713991a148a189cc557f03ded6c9",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"20db399b19734ce1b5600d556d5a91bc": {
"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
}
},
"27d641024d1c457a9845e54b48d80b98": {
"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
}
},
"281808f29e7f41b092ef181bb3dfdc46": {
"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
}
},
"2898d2d04ad14cca8d7e8e702e370f71": {
"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
}
},
"2a110212219746399f87ef382566aa73": {
"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_f2b5ca7adc67416aace874aa7a255f30",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"386d5b040eda4f40a1cb26b501a64de7": {
"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
}
},
"4e6a088f16484e27aa29af56cf45e491": {
"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_8e59e8463e5b417b9e7d28e8615d9a82",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"4e71e8bf71304808b60b3eb7a7311a6e": {
"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_9e2fd53b14b74b6aac9961e659530e35",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"4ea97296a1a8419ebcf1c1b23b2c42f4": {
"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
}
},
"523b713991a148a189cc557f03ded6c9": {
"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_2898d2d04ad14cca8d7e8e702e370f71",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"58e51b4f28254132a3515d3350a341cb": {
"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_386d5b040eda4f40a1cb26b501a64de7",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"5aa2da1d3091471d9ae208ae1baafca8": {
"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_840f85390e8e4d8a862faa7a3714c83b",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "523b713991a148a189cc557f03ded6c9",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"6030862ee6b14227877b217fdd7e90a3": {
"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
}
},
"7629a86c137c479694e7d97c7ef002cb": {
"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_dc652620fbcf474ab19560ae3802e8ff",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"7b261d48426f4ea79e64d9f35ca29967": {
"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_6030862ee6b14227877b217fdd7e90a3",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "523b713991a148a189cc557f03ded6c9",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
},
"840f85390e8e4d8a862faa7a3714c83b": {
"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
}
},
"8b7d8cc96ab14db2b26af3adb318174b": {
"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_c340f05ae26241d7bdfaeebb6b29fdec",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"8e59e8463e5b417b9e7d28e8615d9a82": {
"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
}
},
"924f66ab34da4d18b949e5778fe159d3": {
"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_4ea97296a1a8419ebcf1c1b23b2c42f4",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"9e2fd53b14b74b6aac9961e659530e35": {
"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
}
},
"b01d16602cb445a4bb55f9e593365bdd": {
"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_20db399b19734ce1b5600d556d5a91bc",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"b2686a6f72d247a9b43807f7b108e6fc": {
"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
}
},
"c340f05ae26241d7bdfaeebb6b29fdec": {
"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
}
},
"cc744edfa8934e189752128a754c61a0": {
"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
}
},
"d8d52cd35d214175bcb25c7eb5706f19": {
"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_cc744edfa8934e189752128a754c61a0",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"dc652620fbcf474ab19560ae3802e8ff": {
"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
}
},
"f2b5ca7adc67416aace874aa7a255f30": {
"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
}
},
"f752b59f42384d7fa0bb0b7a99316ce2": {
"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_27d641024d1c457a9845e54b48d80b98",
"msg_id": "",
"outputs": [
{
"data": {
"application/vnd.jupyter.widget-view+json": {
"model_id": "523b713991a148a189cc557f03ded6c9",
"version_major": 2,
"version_minor": 0
},
"text/plain": "Output()"
},
"metadata": {},
"output_type": "display_data"
}
],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}