{
"cells": [
{
"cell_type": "markdown",
"id": "e2092f85",
"metadata": {},
"source": [
"# End component elimination\n",
"End Components (ECs) are sets of states in an MDP where:\n",
"* Every state can reach every other state. (Strongly Connected Component)\n",
"* All actions always lead to a state that is also in the MEC (there is no escape)\n",
"\n",
"For analysis, it is often useful to eliminate these MECs to a single state. We will show how to do this using stormpy and stormvogel."
]
},
{
"cell_type": "code",
"execution_count": 1,
"id": "4b2e315c",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:27.643268Z",
"iopub.status.busy": "2026-03-26T10:48:27.643116Z",
"iopub.status.idle": "2026-03-26T10:48:28.049088Z",
"shell.execute_reply": "2026-03-26T10:48:28.048538Z"
},
"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"
}
],
"source": [
"from stormvogel import *\n",
"\n",
"init = \"init\"\n",
"\n",
"\n",
"def available_actions(s: bird.State):\n",
" if s == \"init\":\n",
" return [\"one\", \"two\"]\n",
" elif s == \"mec1\" or s == \"mec2\":\n",
" return [\"one\", \"two\"]\n",
" return [\"\"]\n",
"\n",
"\n",
"def delta(s: bird.State, a: bird.Action):\n",
" if s == \"init\" and a == \"one\":\n",
" return [(0.5, \"mec1\"), (0.5, \"mec2\")]\n",
" elif s == \"mec1\":\n",
" return [(1, \"mec2\")]\n",
" elif s == \"mec2\":\n",
" return [(1, \"mec1\")]\n",
" elif s == \"init\" and a == \"two\":\n",
" return [(1, \"mec1\")]\n",
" return [(1, s)]\n",
"\n",
"\n",
"labels = lambda s: s\n",
"\n",
"mdp = bird.build_bird(\n",
" delta=delta,\n",
" init=init,\n",
" available_actions=available_actions,\n",
" labels=labels,\n",
" modeltype=ModelType.MDP,\n",
")\n",
"vis = show(mdp, layout=Layout(\"layouts/mec.json\"))"
]
},
{
"cell_type": "markdown",
"id": "d0325f20",
"metadata": {
"lines_to_next_cell": 2
},
"source": [
"First, let's show the maximal end components of this model."
]
},
{
"cell_type": "code",
"execution_count": 2,
"id": "5d0c5e15",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:28.056482Z",
"iopub.status.busy": "2026-03-26T10:48:28.056125Z",
"iopub.status.idle": "2026-03-26T10:48:28.061865Z",
"shell.execute_reply": "2026-03-26T10:48:28.061385Z"
}
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[(frozenset({1, 2}), frozenset({(1, Action(label='two')), (1, Action(label='one')), (2, Action(label='two')), (2, Action(label='one'))}))]\n"
]
}
],
"source": [
"def stormvogel_get_maximal_end_components(sv_model):\n",
" sp_model = stormpy_utils.mapping.stormvogel_to_stormpy(sv_model)\n",
" f = extensions.choice_mapping(sv_model, sp_model)\n",
" decomposition = stormpy.get_maximal_end_components(sp_model)\n",
" res = []\n",
" for mec in decomposition:\n",
" states = set()\n",
" actions = set()\n",
" for s_id, choices in mec:\n",
" states.add(s_id)\n",
" actions = actions | set(map(lambda x: f.inverse[x], choices))\n",
" res.append((frozenset(states), frozenset(actions)))\n",
" return res\n",
"\n",
"\n",
"decomp = stormvogel_get_maximal_end_components(mdp)\n",
"print(decomp)"
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "1f0e6070",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:28.063507Z",
"iopub.status.busy": "2026-03-26T10:48:28.063328Z",
"iopub.status.idle": "2026-03-26T10:48:28.075301Z",
"shell.execute_reply": "2026-03-26T10:48:28.074750Z"
}
},
"outputs": [],
"source": [
"vis.highlight_decomposition(decomp)"
]
},
{
"cell_type": "markdown",
"id": "55083d2b",
"metadata": {},
"source": [
"Now we perform end component elimination by converting to stormpy and back."
]
},
{
"cell_type": "code",
"execution_count": 4,
"id": "9f24d7e2",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:28.076943Z",
"iopub.status.busy": "2026-03-26T10:48:28.076772Z",
"iopub.status.idle": "2026-03-26T10:48:28.082556Z",
"shell.execute_reply": "2026-03-26T10:48:28.082068Z"
}
},
"outputs": [],
"source": [
"import stormpy\n",
"\n",
"\n",
"def map_state_labels(m, res):\n",
" \"\"\"Based on the result of EC elimination, create a new state labeling that can be used for a new model that captures the result.\n",
" Args:\n",
" m: stormpy model\n",
" res (EndComponentEliminatorReturnTypeDouble): EC result\n",
" \"\"\"\n",
" old_nr_columns = m.transition_matrix.nr_columns\n",
" new_nr_columns = res.matrix.nr_columns\n",
" sl = stormpy.StateLabeling(new_nr_columns)\n",
"\n",
" for s_old in range(old_nr_columns):\n",
" s_new = res.old_to_new_state_mapping[s_old]\n",
" for l in m.labeling.get_labels_of_state(s_old):\n",
" sl.add_label(l)\n",
" sl.add_label_to_state(l, s_new)\n",
" return sl\n",
"\n",
"\n",
"def map_choice_labels(m_old, m_new, res):\n",
" \"\"\"Based on the result of EC elimination, create a new choice labeling that can be used for a new model that captures the result.\n",
" Args:\n",
" m_old: old stormpy model\n",
" m_new: new strompy model that is based on res\n",
" res (EndComponentEliminatorReturnTypeDouble): EC result\n",
" \"\"\"\n",
" new_nr_rows = m_new.transition_matrix.nr_rows\n",
" cl = stormpy.storage.ChoiceLabeling(new_nr_rows)\n",
" old_nr_columns = m_old.transition_matrix.nr_columns\n",
"\n",
" for s_old in range(old_nr_columns):\n",
" s_new = res.old_to_new_state_mapping[s_old]\n",
" old_no_choices = m_old.get_nr_available_actions(s_old)\n",
" new_no_choices = m_new.get_nr_available_actions(s_new)\n",
" if old_no_choices == new_no_choices:\n",
" for action_no in range(old_no_choices):\n",
" old_index = m_old.get_choice_index(s_old, action_no)\n",
" labels = m_old.choice_labeling.get_labels_of_choice(old_index)\n",
" new_index = m_new.get_choice_index(s_new, action_no)\n",
" for l in labels:\n",
" cl.add_label(l)\n",
" cl.add_label_to_choice(l, new_index)\n",
" return cl\n",
"\n",
"\n",
"def simple_ec_elimination(m):\n",
" \"\"\"Perform EC elimination on a stormpy model while preserving labels.\n",
" Label sets of merged states are unified.\n",
" Action labels are preserved when possible.\n",
" Args:\n",
" m: stormpy model\n",
" \"\"\"\n",
" # Keep all states, and consider ecs to be possible anywhere in the model\n",
" subsystem = stormpy.BitVector(m.nr_states, True)\n",
" possible_ec_rows = stormpy.BitVector(m.nr_choices, True)\n",
" res = stormpy.eliminate_ECs(\n",
" matrix=m.transition_matrix,\n",
" subsystem=subsystem,\n",
" possible_ecs=possible_ec_rows,\n",
" add_sink_row_states=subsystem,\n",
" add_self_loop_at_sink_states=True,\n",
" )\n",
" new_labels = map_state_labels(m, res)\n",
" components = stormpy.SparseModelComponents(\n",
" transition_matrix=res.matrix, state_labeling=new_labels\n",
" )\n",
" m_new = stormpy.storage.SparseMdp(components)\n",
" components.choice_labeling = map_choice_labels(m, m_new, res)\n",
" m_updated = stormpy.storage.SparseMdp(components)\n",
" return m_updated"
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "613ab746",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:28.084134Z",
"iopub.status.busy": "2026-03-26T10:48:28.083971Z",
"iopub.status.idle": "2026-03-26T10:48:28.112231Z",
"shell.execute_reply": "2026-03-26T10:48:28.111706Z"
}
},
"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"
}
],
"source": [
"sp_mdp = stormpy_utils.mapping.stormvogel_to_stormpy(mdp)\n",
"sp_mdp_elim = simple_ec_elimination(sp_mdp)\n",
"sv_mdp_elim = stormpy_utils.mapping.stormpy_to_stormvogel(sp_mdp_elim)\n",
"vis = show(sv_mdp_elim)"
]
},
{
"cell_type": "markdown",
"id": "daae8f72",
"metadata": {},
"source": [
"These functions are also available under stormvogel.extensions.ec_elimination."
]
},
{
"cell_type": "code",
"execution_count": 6,
"id": "5bd832fa",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:48:28.119514Z",
"iopub.status.busy": "2026-03-26T10:48:28.119334Z",
"iopub.status.idle": "2026-03-26T10:48:28.123769Z",
"shell.execute_reply": "2026-03-26T10:48:28.123193Z"
}
},
"outputs": [
{
"data": {
"text/plain": [
"True"
]
},
"execution_count": 6,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"sp_mdp_elim2 = extensions.simple_ec_elimination(sp_mdp)\n",
"sv_mdp_elim2 = stormpy_utils.mapping.stormpy_to_stormvogel(sp_mdp_elim2)\n",
"sv_mdp_elim == sv_mdp_elim2"
]
}
],
"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": {
"078a59fe742049e39baf59f845362c05": {
"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_6d8b57f954694b2b81d91f5d6c00ad6a",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"2c9341914bb0408ea27c56173e36f3e4": {
"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_b7129a170f7d459bb821d05bf840f6aa",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"52f219e654f94aafb1837da685a0bddb": {
"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
}
},
"6b6bc067ccc54db2abc33ab91a3e3447": {
"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_8243d65760d84b19a0d6c5a5edb29a9e",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"6d8b57f954694b2b81d91f5d6c00ad6a": {
"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
}
},
"8243d65760d84b19a0d6c5a5edb29a9e": {
"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
}
},
"b7129a170f7d459bb821d05bf840f6aa": {
"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
}
},
"c50fc1e1c47a423b8c9c89491e124265": {
"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_52f219e654f94aafb1837da685a0bddb",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}