"This notebook demonstrates how to use the `strength_decompose()` function to split an automaton in up to three automata capturing different behaviors. This is based on the paper [Strength-based decomposition of the property B\u00fcchi automaton for faster model checking](https://www.lrde.epita.fr/~adl/dl/adl/renault.13.tacas.pdf) (TACAS'13).\n",
"This notebook demonstrates how to use the `decompose_strength()` function to split an automaton in up to three automata capturing different behaviors. This is based on the paper [Strength-based decomposition of the property B\u00fcchi automaton for faster model checking](https://www.lrde.epita.fr/~adl/dl/adl/renault.13.tacas.pdf) (TACAS'13).\n",
"\n",
"This page uses the Python bindings, but the same decompositions can be performed from the shell using [`autfilt`](https://spot.lrde.epita.fr/autfilt.html) and its `--decompose-strength` option.\n",
"\n",
"# Basics\n",
"\n",
"Let's define the following strengths of SCCs:\n",
"\n",
"- an accepting SCC is **weak** if all its transitions belong to the same acceptance sets\n",
"- an accepting SCC is **terminal** if it is *weak* and complete (i.e. from any state, you can stay in the SCC by reading any word)\n",
"- an accepting SCC is **strictly weak** if it is *weak* and not complete (in other words: *weak* but not *terminal*)\n",
...
...
@@ -199,7 +203,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG object>"
"<IPython.core.display.SVG at 0x7fd4fcc39198>"
]
}
],
...
...
@@ -209,9 +213,10 @@
"cell_type": "markdown",
"metadata": {},
"source": [
"The `strength_decompose()` function takes an automaton, and a string specifying which strength to preserve. \n",
"The `decompose_strength()` function takes an automaton, and a string specifying which strength to preserve. \n",
"\n",
"The letters used for this specification are as follows:\n",
"\n",
"- `t`: terminal\n",
"- `w`: strictly weak\n",
"- `s`: strong\n",
...
...
@@ -309,7 +314,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG object>"
"<IPython.core.display.SVG at 0x7fd505085f60>"
]
}
],
...
...
@@ -444,7 +449,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG object>"
"<IPython.core.display.SVG at 0x7fd4fc0f2978>"
]
}
],
...
...
@@ -528,7 +533,7 @@
"</svg>"
],
"text": [
"<IPython.core.display.SVG object>"
"<IPython.core.display.SVG at 0x7fd4fc1329b0>"
]
}
],
...
...
@@ -599,7 +604,7 @@
"</svg>\n"
],
"text": [
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fe318ffbf00> >"
"<spot_impl.twa_graph; proxy of <Swig Object of type 'std::shared_ptr< spot::twa_graph > *' at 0x7fd4fcbe7720> >"
