{
"cells": [
{
"cell_type": "markdown",
"id": "6f5faf29",
"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": "b4ce6a4c",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:53.652156Z",
"iopub.status.busy": "2026-04-16T05:27:53.651974Z",
"iopub.status.idle": "2026-04-16T05:27:54.100868Z",
"shell.execute_reply": "2026-04-16T05:27:54.100208Z"
},
"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",
"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",
"show(mdp)"
]
},
{
"cell_type": "markdown",
"id": "bd0bfadb",
"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": "2c26abc2",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:54.107651Z",
"iopub.status.busy": "2026-04-16T05:27:54.107275Z",
"iopub.status.idle": "2026-04-16T05:27:54.114064Z",
"shell.execute_reply": "2026-04-16T05:27:54.113556Z"
},
"lines_to_next_cell": 2
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[(frozenset({State(id=ad55c494-f269-45e1-aef6-10935b2abf99, labels=['mec1']), State(id=f47e3c5a-8d67-4aba-984d-983ffa9e56bb, labels=['mec2'])}), frozenset({(State(id=f47e3c5a-8d67-4aba-984d-983ffa9e56bb, labels=['mec2']), Action('one')), (State(id=ad55c494-f269-45e1-aef6-10935b2abf99, labels=['mec1']), Action('one')), (State(id=f47e3c5a-8d67-4aba-984d-983ffa9e56bb, labels=['mec2']), Action('two')), (State(id=ad55c494-f269-45e1-aef6-10935b2abf99, labels=['mec1']), Action('two'))}))]\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(sv_model.states[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": "markdown",
"id": "e5697cf2",
"metadata": {},
"source": [
"Now we perform end component elimination by converting to stormpy and back."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "9988a712",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:54.115916Z",
"iopub.status.busy": "2026-04-16T05:27:54.115741Z",
"iopub.status.idle": "2026-04-16T05:27:54.121714Z",
"shell.execute_reply": "2026-04-16T05:27:54.121214Z"
}
},
"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": 4,
"id": "5b3d286f",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:54.123374Z",
"iopub.status.busy": "2026-04-16T05:27:54.123191Z",
"iopub.status.idle": "2026-04-16T05:27:54.154398Z",
"shell.execute_reply": "2026-04-16T05:27:54.153729Z"
}
},
"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": [
"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",
"show(sv_mdp_elim)"
]
},
{
"cell_type": "markdown",
"id": "b35276c5",
"metadata": {},
"source": [
"These functions are also available under stormvogel.extensions.ec_elimination."
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "8dbc6dca",
"metadata": {
"execution": {
"iopub.execute_input": "2026-04-16T05:27:54.161337Z",
"iopub.status.busy": "2026-04-16T05:27:54.161136Z",
"iopub.status.idle": "2026-04-16T05:27:54.165513Z",
"shell.execute_reply": "2026-04-16T05:27:54.165010Z"
}
},
"outputs": [
{
"data": {
"text/plain": [
"False"
]
},
"execution_count": 5,
"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": {
"0fe2b96d500f4a0cbb3baf4bc9835332": {
"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_fba0348737154a9f87887f47bdfa8fe2",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"22070952c5ee463689f77667c694e430": {
"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_7823e4f4d805404c963fb26ebbab41df",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"438f2f64703a4a5cb798e18c280d2895": {
"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
}
},
"7823e4f4d805404c963fb26ebbab41df": {
"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
}
},
"7d22de478c284e039fff8353bbfc9b00": {
"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_b0230f61d21e41eea920b80d0251e803",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"a87a0b61343944b1a116fc7873cc2986": {
"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_438f2f64703a4a5cb798e18c280d2895",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"b0230f61d21e41eea920b80d0251e803": {
"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
}
},
"fba0348737154a9f87887f47bdfa8fe2": {
"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
}