{
"cells": [
{
"cell_type": "markdown",
"id": "ec1528bd",
"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": "129d91b5",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:42:16.902969Z",
"iopub.status.busy": "2026-03-26T10:42:16.902802Z",
"iopub.status.idle": "2026-03-26T10:42:17.363885Z",
"shell.execute_reply": "2026-03-26T10:42:17.363229Z"
},
"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": "06fe8f99",
"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": "d6e1513e",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:42:17.371115Z",
"iopub.status.busy": "2026-03-26T10:42:17.370736Z",
"iopub.status.idle": "2026-03-26T10:42:17.377456Z",
"shell.execute_reply": "2026-03-26T10:42:17.376895Z"
},
"lines_to_next_cell": 2
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"[(frozenset({State(model=, state_id=UUID('7f57eeca-300a-4ea3-b9e2-f27f74c9b36d')), State(model=, state_id=UUID('131d8292-613a-4a49-ac73-64050862a692'))}), frozenset({(State(model=, state_id=UUID('131d8292-613a-4a49-ac73-64050862a692')), Action with label one), (State(model=, state_id=UUID('7f57eeca-300a-4ea3-b9e2-f27f74c9b36d')), Action with label one), (State(model=, state_id=UUID('7f57eeca-300a-4ea3-b9e2-f27f74c9b36d')), Action with label two), (State(model=, state_id=UUID('131d8292-613a-4a49-ac73-64050862a692')), Action with label 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": "93e00384",
"metadata": {},
"source": [
"Now we perform end component elimination by converting to stormpy and back."
]
},
{
"cell_type": "code",
"execution_count": 3,
"id": "60d76a52",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:42:17.379286Z",
"iopub.status.busy": "2026-03-26T10:42:17.379087Z",
"iopub.status.idle": "2026-03-26T10:42:17.385704Z",
"shell.execute_reply": "2026-03-26T10:42:17.385044Z"
}
},
"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": "8d047585",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:42:17.387453Z",
"iopub.status.busy": "2026-03-26T10:42:17.387240Z",
"iopub.status.idle": "2026-03-26T10:42:17.419740Z",
"shell.execute_reply": "2026-03-26T10:42:17.419113Z"
}
},
"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": "f52a5add",
"metadata": {},
"source": [
"These functions are also available under stormvogel.extensions.ec_elimination."
]
},
{
"cell_type": "code",
"execution_count": 5,
"id": "4c1809c1",
"metadata": {
"execution": {
"iopub.execute_input": "2026-03-26T10:42:17.426905Z",
"iopub.status.busy": "2026-03-26T10:42:17.426684Z",
"iopub.status.idle": "2026-03-26T10:42:17.431512Z",
"shell.execute_reply": "2026-03-26T10:42:17.430863Z"
}
},
"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": {
"33e2d04637ea4fe6b6a1d3dcac7c5e27": {
"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_698d19d37c754c07817a2812cf1f2f40",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"3cac557b26a54a70a34d58fa43d93d3c": {
"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_5e778df90c0e4c1f9590697361a5fe25",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"5e778df90c0e4c1f9590697361a5fe25": {
"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
}
},
"683235a755c24f8f8135573f59fed89c": {
"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
}
},
"698d19d37c754c07817a2812cf1f2f40": {
"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
}
},
"81d7c0bed27441d8b0985fcaa3c05187": {
"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
}
},
"a6fa745b4fba48bca6c3bd29f21ae26b": {
"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_683235a755c24f8f8135573f59fed89c",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
},
"f83d65a84fd745b482aa123310b8a51c": {
"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_81d7c0bed27441d8b0985fcaa3c05187",
"msg_id": "",
"outputs": [],
"tabbable": null,
"tooltip": null
}
}
},
"version_major": 2,
"version_minor": 0
}
}
},
"nbformat": 4,
"nbformat_minor": 5
}