{
"cells": [
{
"cell_type": "markdown",
"id": "6be41ea9",
"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 different sources.\n",
"In particular, we show how to construct a model using our `bird` API and the `model` API.\n",
"Beyond these APIs, stormvogel supports seamless conversion to and from stormpy. This means that you can also use any way of building models that is supported by stormpy.\n",
"This includes the [PRISM](https://www.prismmodelchecker.org/) language and the [JANI](https://www.stormchecker.org/files/BDHHJT17.pdf) modelling language, as well as [stormpy's own APIs](https://stormchecker.github.io/stormpy/).\n",
"For these, we refer to their respective documentations."
]
},
{
"cell_type": "markdown",
"id": "c15645e3",
"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": "857386ec",
"metadata": {},
"source": [
"### Bird API\n",
"The Bird API is probably the most intuitive way to create a model.\n",
"The user defines a `delta` function which maps a state to a distribution of successor states."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "34944b9a",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:41:25.262123Z",
"iopub.status.busy": "2026-03-26T10:41:25.261945Z",
"iopub.status.idle": "2026-03-26T10:41:25.736818Z",
"shell.execute_reply": "2026-03-26T10:41:25.736195Z"
}
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
""
]
},
"execution_count": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"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",
"\n",
"\n",
"# In the bird API, states are given implicitly. Any object can be a state and via the transition relation, we define reachable states.\n",
"# This user-defined delta function encodes the transition relation. It takes as an argument a single state, and returns a\n",
"# list of 2-tuples that encode the distribution over the successor states. More precisely, 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",
"\n",
"# Labels is a function that tells the bird 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",
"\n",
"bird_die = bird.build_bird(\n",
" delta=delta, init=init, labels=labels, modeltype=ModelType.DTMC\n",
")\n",
"show(bird_die)"
]
},
{
"cell_type": "markdown",
"id": "7f4093a8",
"metadata": {},
"source": [
"### Model API\n",
"This same model can also be constructed using the model API.\n",
"This API requires adding states and transition explicitly to the model object and therefore is closer to how the models are represented in stormvogel.\n",
"We generally recommend just using the bird API, but if you need more control, the model API can also be useful."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "3163df56",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:41:25.743867Z",
"iopub.status.busy": "2026-03-26T10:41:25.743517Z",
"iopub.status.idle": "2026-03-26T10:41:25.778957Z",
"shell.execute_reply": "2026-03-26T10:41:25.778302Z"
},
"lines_to_next_cell": 2
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
""
]
},
"execution_count": 2,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# 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.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.states[k] # Get the state at index k\n",
" if k <= 6:\n",
" state.set_choices([(p, die_model.states[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",
"show(die_model)"
]
},
{
"cell_type": "markdown",
"id": "f9675382",
"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": "fc071c4a",
"metadata": {
"lines_to_next_cell": 2
},
"source": [
"### Bird API"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "3907c784",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:41:25.786407Z",
"iopub.status.busy": "2026-03-26T10:41:25.786097Z",
"iopub.status.idle": "2026-03-26T10:41:25.822384Z",
"shell.execute_reply": "2026-03-26T10:41:25.821712Z"
}
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
""
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"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",
"\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",
"\n",
"bird_commu = bird.build_bird(\n",
" delta=delta, init=\"zero\", labels=labels, modeltype=ModelType.DTMC\n",
")\n",
"show(bird_commu)"
]
},
{
"cell_type": "markdown",
"id": "99569dff",
"metadata": {},
"source": [
"### Model API"
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "c2a59893",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:41:25.829180Z",
"iopub.status.busy": "2026-03-26T10:41:25.828978Z",
"iopub.status.idle": "2026-03-26T10:41:25.861611Z",
"shell.execute_reply": "2026-03-26T10:41:25.861029Z"
}
},
"outputs": [
{
"data": {
"text/html": [
"\n",
"\n",
"\n",
" \n",
" Network\n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
" \n",
"\n"
],
"text/plain": [
""
]
},
"metadata": {},
"output_type": "display_data"
},
{
"data": {
"text/plain": [
""
]
},
"execution_count": 4,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"commu_model = stormvogel.model.new_dtmc(create_initial_state=True)\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",
"\n",
"LABELS = {0: [], 1: [\"try\"], 2: [\"fail\"], 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.states[sid]\n",
" state.set_choices([(p, commu_model.states[sid_]) for p, sid_ in TRANSITIONS[sid]])\n",
"\n",
"show(commu_model)"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "Python 3 (ipykernel)",
"language": "python",
"name": "python3"
},
"language_info": {
"codemirror_mode": {
"name": "ipython",
"version": 3
},
"file_extension": ".py",
"mimetype": "text/x-python",
"name": "python",
"nbconvert_exporter": "python",
"pygments_lexer": "ipython3",
"version": "3.12.13"
},
"widgets": {
"application/vnd.jupyter.widget-state+json": {
"state": {
"0f78eea540f642db9fea077d62474bd6": {
"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_be07247dd46340d888c895b2b50b820d",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"4eb650e492a14a70a2d815c8c97561ef": {
"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_9947a948d8ef45fbaa762163e08f5d42",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"5767cc268d9a4287879a40a00ec84602": {
"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
}
},
"5dd9fb6883964b72a1b9c6a397d0e26b": {
"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_5767cc268d9a4287879a40a00ec84602",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"8b42fa94b0b045ae81b398255deee732": {
"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_be8d41a866aa42f699c0d5560f44bf1f",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"8d41b535ea5a4704b9d687ca4ba24290": {
"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_a6730acb9207464585132e8ac90c9e73",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"9947a948d8ef45fbaa762163e08f5d42": {
"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
}
},
"9c2f073b83b541888e18f904b4e442d8": {
"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
}
},
"a6730acb9207464585132e8ac90c9e73": {
"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
}
},
"a8c7726f0b544bc7bb327006be4382f1": {
"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_e1c0ccf5a2c749d38a5edadeff11bcdc",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"be07247dd46340d888c895b2b50b820d": {
"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
}
},
"be8d41a866aa42f699c0d5560f44bf1f": {
"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
}
},
"d8ad5ca5db49432ead3c99edb3081768": {
"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_f8e40d0033d1417d83d7b2e861f55c96",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"e1c0ccf5a2c749d38a5edadeff11bcdc": {
"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
}
},
"e2f77d46fc7142d0ac34fa219cfa96e1": {
"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_9c2f073b83b541888e18f904b4e442d8",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"f8e40d0033d1417d83d7b2e861f55c96": {
"model_module": "@jupyter-widgets/base",
"model_module_version": "2.0.0",
"model_name": "LayoutModel",
"state": {
"_model_module": "@jupyter-widgets/base",
"_model_module_version": "2.0.0",
"_model_name": "LayoutModel",
"_view_count": null,
"_view_module": "@jupyter-widgets/base",
"_view_module_version": "2.0.0",
"_view_name": "LayoutView",
"align_content": null,
"align_items": null,
"align_self": null,
"border_bottom": null,
"border_left": null,
"border_right": null,
"border_top": null,
"bottom": null,
"display": null,
"flex": null,
"flex_flow": null,
"grid_area": null,
"grid_auto_columns": null,
"grid_auto_flow": null,
"grid_auto_rows": null,
"grid_column": null,
"grid_gap": null,
"grid_row": null,
"grid_template_areas": null,
"grid_template_columns": null,
"grid_template_rows": null,
"height": null,
"justify_content": null,
"justify_items": null,
"left": null,
"margin": null,
"max_height": null,
"max_width": null,
"min_height": null,
"min_width": null,
"object_fit": null,
"object_position": null,
"order": null,
"overflow": null,
"padding": null,
"right": null,
"top": null,
"visibility": null,
"width": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}