{
"cells": [
{
"cell_type": "markdown",
"id": "8132589c",
"metadata": {},
"source": [
"# Parallel composition\n",
"Using the Bird API, you can define your own parallel composition logic. This works similar to PRISM models. We give an example here. We create two MDP models `m1` and `m2`, and then we create the quotient model `q`. They synchronize on the action `r`."
]
},
{
"cell_type": "markdown",
"id": "abbb9c0a",
"metadata": {},
"source": [
"## m1\n",
"`m1` is a simple 2x2 grid model where taking `l` `r` `u` and `d` move to the next tile."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "3b02f81c",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:51.632423Z",
"iopub.status.busy": "2026-04-16T05:27:51.632232Z",
"iopub.status.idle": "2026-04-16T05:27:52.081525Z",
"shell.execute_reply": "2026-04-16T05:27:52.080942Z"
},
"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": 1,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"from stormvogel import *\n",
"\n",
"N = 2\n",
"\n",
"ACTION_SEMANTICS = {\"l\": (-1, 0), \"r\": (1, 0), \"u\": (0, -1), \"d\": (0, 1)}\n",
"\n",
"\n",
"def available_actions_m1(s):\n",
" res = []\n",
" if s[0] > 0:\n",
" res.append(\"l\")\n",
" if s[0] < N - 1:\n",
" res.append(\"r\")\n",
" if s[1] > 0:\n",
" res.append(\"u\")\n",
" if s[1] < N - 1:\n",
" res.append(\"d\")\n",
" return res\n",
"\n",
"\n",
"def pairwise_plus(t1, t2):\n",
" return (t1[0] + t2[0], t1[1] + t2[1])\n",
"\n",
"\n",
"def delta_m1(s, a):\n",
" return [(1, pairwise_plus(s, ACTION_SEMANTICS[a]))]\n",
"\n",
"\n",
"def labels_m1(s):\n",
" return [str(s)]\n",
"\n",
"\n",
"m1 = bird.build_bird(\n",
" init=(0, 0),\n",
" available_actions=available_actions_m1,\n",
" labels=labels_m1,\n",
" delta=delta_m1,\n",
")\n",
"show(m1)"
]
},
{
"cell_type": "markdown",
"id": "e01a074b",
"metadata": {
"lines_to_next_cell": 2
},
"source": [
"## m2\n",
"`m2` is a model that counts the number of `r` up until two, and has a faulty reset button `c` to reset the counter. It only works in 80% of the cases. It only allows `r` if the count is not already 2."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "d1e982ad",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:52.088665Z",
"iopub.status.busy": "2026-04-16T05:27:52.088313Z",
"iopub.status.idle": "2026-04-16T05:27:52.121813Z",
"shell.execute_reply": "2026-04-16T05:27:52.121173Z"
}
},
"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": [
"def available_actions_m2(s):\n",
" if s <= 1:\n",
" return [\"r\", \"c\"]\n",
" if s == 2:\n",
" return [\"c\"]\n",
"\n",
"\n",
"def delta_m2(s, a):\n",
" if s <= 1:\n",
" if \"r\" in a:\n",
" return [(1, s + 1)]\n",
" elif s == 0:\n",
" return [(1, 0)]\n",
" else:\n",
" return [(0.8, 0), (0.2, s)]\n",
" else:\n",
" return [(0.8, 0), (0.2, s)]\n",
"\n",
"\n",
"def labels_m2(s):\n",
" return [str(s)]\n",
"\n",
"\n",
"m2 = bird.build_bird(\n",
" init=0, available_actions=available_actions_m2, labels=labels_m2, delta=delta_m2\n",
")\n",
"show(m2)"
]
},
{
"cell_type": "markdown",
"id": "bac59b46",
"metadata": {},
"source": [
"## Quotient model\n",
"Now we construct the quotient model."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "d4f0bfc7",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:52.128907Z",
"iopub.status.busy": "2026-04-16T05:27:52.128697Z",
"iopub.status.idle": "2026-04-16T05:27:52.165390Z",
"shell.execute_reply": "2026-04-16T05:27:52.164802Z"
}
},
"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": [
"SYNC = [\"r\"]\n",
"\n",
"\n",
"def prob_product(branch1, branch2):\n",
" return [(p1 * p2, (r1, r2)) for p1, r1 in branch1 for p2, r2 in branch2]\n",
"\n",
"\n",
"def available_actions(s):\n",
" a1 = available_actions_m1(s[0])\n",
" a2 = available_actions_m2(s[1])\n",
" union = set(a1 + a2)\n",
" intersection = set(a1) & set(a2)\n",
" return [x for x in union if x in intersection or x not in SYNC]\n",
"\n",
"\n",
"def delta(s, a):\n",
" a1 = available_actions_m1(s[0])\n",
" a2 = available_actions_m2(s[1])\n",
"\n",
" if a in a1 and a in a2:\n",
" return prob_product(delta_m1(s[0], a), delta_m2(s[1], a))\n",
" elif a in a1:\n",
" return [(p, (s_, s[1])) for p, s_ in delta_m1(s[0], a)]\n",
" elif a in a2:\n",
" return [(p, (s[0], s_)) for p, s_ in delta_m2(s[1], a)]\n",
" else:\n",
" return [(1, s)]\n",
"\n",
"\n",
"def labels(s):\n",
" return labels_m1(s[0]) + labels_m2(s[1])\n",
"\n",
"\n",
"q = bird.build_bird(\n",
" init=((0, 0), 0), available_actions=available_actions, labels=labels, delta=delta\n",
")\n",
"show(q)"
]
}
],
"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": {
"0aec00d39ba546c698974a8cdcdc994a": {
"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
}
},
"0c2909e2d771454b809ce38e3b0f938a": {
"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_0aec00d39ba546c698974a8cdcdc994a",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"19c57d1da2f84c81940f125b7d45de8a": {
"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
}
},
"2d19eef4f5ca48e49e9b8c6e41292884": {
"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
}
},
"44764430b7ec4811ac2e9cda7e470ada": {
"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
}
},
"502ddd1501b7475b81772d88b7d7e9c4": {
"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_52a4bd12eb8d4f66b8870edde61f0291",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"52a4bd12eb8d4f66b8870edde61f0291": {
"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
}
},
"567207a10e4347739855a7f9db5ad00b": {
"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
}
},
"7a27d3f9efe149148b7cf98642cbf837": {
"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_44764430b7ec4811ac2e9cda7e470ada",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"afa98ec36ce44bc28b090eb5dd426f5e": {
"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_567207a10e4347739855a7f9db5ad00b",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"c20cfff232aa4044a7b559db1c596662": {
"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_19c57d1da2f84c81940f125b7d45de8a",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"ef4d26c206d2415085687132324e5f8a": {
"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_2d19eef4f5ca48e49e9b8c6e41292884",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}