{ "cells": [ { "cell_type": "markdown", "id": "31f7a2f6-4a03-47fa-848c-a2e05bc91090", "metadata": {}, "source": [ "# Extracting macro-dynamics\n", "\n", "We use the termites model to show how macro-dynamics can be extracted.\n", "\n", "First, we load the model and build its state-space as a single-node component-graph `g`. Then, we define our target formula: all kind of termites are present." ] }, { "cell_type": "code", "execution_count": 1, "id": "56c4c490-2e5a-4ff3-8ddd-0a0563f3982f", "metadata": {}, "outputs": [], "source": [ "%run -m ecco rr-termites.rr\n", "g = model()\n", "phi = \"(Rp & Sd & Wk)\"" ] }, { "cell_type": "markdown", "id": "717e08ea-f7a9-4afc-a997-d8f82a0bda2f", "metadata": {}, "source": [ "Then, we split against two properties: `phi` itself, and `f\"EF{phi}\"` (where `f\"...{phi}...\"` allows in Python to insert formula `phi` into another string)." ] }, { "cell_type": "code", "execution_count": 2, "id": "3c2fb4f1-fc6f-4946-a77c-e73336593b4b", "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "3897ff12514f4922b554d1baaab17d88", "version_major": 2, "version_minor": 0 }, "text/plain": [ "VBox(children=(Accordion(children=(VBox(children=(HBox(children=(Dropdown(description='layout', index=3, optio…" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "g1 = g.split(phi=phi, EF_phi=f\"EF{phi}\")\n", "g1" ] }, { "cell_type": "code", "execution_count": 3, "id": "3a6bd2b5-bc62-45b6-9b35-45760026ebd3", "metadata": {}, "outputs": [ { "data": { "text/html": [ "
\n", "\n", "\n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", " \n", "
trapssizeconstsHASNOHASCONTAINSISINEQUALS
node
1()12(Ec+, Fg+, Md+, Rp+, Sd+, Wk+)(DEAD, INIT)(scc)(hull)(EF_phi, HULL)(phi)
3(1)34(Rp+)(DEAD, phi)(HULL)(INIT, hull, scc)(EF_phi)()
4()68(Rp-, Wk-)(EF_phi, HULL, INIT, hull, phi, scc)()(DEAD)()()
\n", "
" ], "text/plain": [ " traps size consts \\\n", "node \n", "1 () 12 (Ec+, Fg+, Md+, Rp+, Sd+, Wk+) \n", "3 (1) 34 (Rp+) \n", "4 () 68 (Rp-, Wk-) \n", "\n", " HASNO HAS CONTAINS \\\n", "node \n", "1 (DEAD, INIT) (scc) (hull) \n", "3 (DEAD, phi) (HULL) (INIT, hull, scc) \n", "4 (EF_phi, HULL, INIT, hull, phi, scc) () (DEAD) \n", "\n", " ISIN EQUALS \n", "node \n", "1 (EF_phi, HULL) (phi) \n", "3 (EF_phi) () \n", "4 () () " ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "g1.nodes" ] }, { "cell_type": "markdown", "id": "38309a13-12b2-4308-8ec7-fc31c37451ca", "metadata": {}, "source": [ "We observe that `phi` is reachable and the corresponding states are in component `#1`, the rest of the state space is split into the states that allow to reach `phi` (`#3`) and those where `phi` has been lost forever (`#4`).\n", "\n", "We also observe that `phi` may persist forever since `#1` contains a SCC.\n", "\n", "Finally, we observe that `#3` is a trap and we shall fix this:" ] }, { "cell_type": "code", "execution_count": 4, "id": "ff3b74c5-c8bf-4ee1-b0ac-d99543e19176", "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "5e229e7c4ff94f2ca727ded205db4398", "version_major": 2, "version_minor": 0 }, "text/plain": [ "VBox(children=(Accordion(children=(VBox(children=(HBox(children=(Dropdown(description='layout', index=3, optio…" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "g2 = g1.untrap(3)\n", "g2" ] }, { "cell_type": "markdown", "id": "77435398-e3eb-424a-b4dd-2543d6845ffa", "metadata": {}, "source": [ "Why `#3` was a trap is now explained: from the initial state, we can reach `#5` then `#1` and obtain `phi`.\n", "But from `#5` and `#1`, the initial state and other states, forming `#6`, cannot be reached back.\n", "This initial part `#6` even contains a SCC, which means that reaching `phi` can be delayed forever.\n", "This is also the case with `#5` and there is only one difference between `#5` and `#6`: the former can be reached from states where `phi` holds while the latter cannot, but both allow to reach `phi` while this may be delayed forever.\n", "\n", "We may wan to separate in `#6` the states that allow this delay from the others using functional property `hull()`." ] }, { "cell_type": "code", "execution_count": 6, "id": "1dfe7364-0285-46f2-bec4-3a38155536c6", "metadata": {}, "outputs": [ { "data": { "application/vnd.jupyter.widget-view+json": { "model_id": "7443dbda0b0b4f38a4621e2ce68b1fdd", "version_major": 2, "version_minor": 0 }, "text/plain": [ "VBox(children=(Accordion(children=(VBox(children=(HBox(children=(Dropdown(description='layout', index=3, optio…" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "g3 = g2.split(\"hull()\", 6)\n", "g3" ] }, { "cell_type": "markdown", "id": "8b7b9f57-34a6-4111-995d-259c938f878c", "metadata": {}, "source": [ "Now we can see that the system needs to execute `R4` before it has a chance to reach `phi`.\n", "Then, at any stage, executing `R11` or `R12` is the cause of loosing the reachability of `phi`.\n", "We could further analyse what these transitions are and why `#1` and `#5` are not SCC, but this is not the purpose of this notebokk that just shows how generic splits can provide a reach overview of the macro-dynamics of a system with respect to a property of interest." ] }, { "cell_type": "code", "execution_count": null, "id": "ac06685e-b828-4d50-a774-c975636763c7", "metadata": {}, "outputs": [], "source": [] } ], "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.1" } }, "nbformat": 4, "nbformat_minor": 5 }