6

{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# SAT-based minimization of deterministic ω-automata\n", "\n", "The `spot.sat_minimize()` Python function is the main entry point for minimizing any **deterministic** ω-automaton. This notebook demonstrates how to use that function.\n", "\n", "**Warning:** while the automata used in this notebook are quite small, working with large automata can require a lot of RAM and take huge amount of time. In its most straightforward variant, `sat_minimize()` takes a input automaton (called *reference*) and then makes a loop to ask a SAT-solver for an equivalent automaton (called *candidate*) with 1 fewer state at each iteration. If the reference has size ($n_i$, $s_i$), i.e. $n_i$ states, $s_i$ acceptance sets, and the candidate has size $(n_o, s_o)$, the SAT encoding uses $\\mathrm{O}(n_i^2\\times n_o^2\\times 2^{s_i+s_o})$ variables and $\\mathrm{O}(n_i^2 \\times n_o^3\\times 2^{s_i+2s_o}\\times |\\Sigma|)$ clauses. Reducing the number of acceptance set the therefore the most important way to simplify a problem." ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [], "source": [ "import spot\n", "spot.setup(show_default='.b')\n", "from IPython.display import display" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Minimizing DBA\n", "\n", "Let's take a simple formula and translate it into a DBA:" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "data": { "text/latex": [ "$\\mathsf{G} \\mathsf{F} (a \\leftrightarrow \\mathsf{X} \\mathsf{X} b)$" ], "text/plain": [ "spot.formula(\"GF(a <-> XXb)\")" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "f = spot.formula('GF(a <-> XXb)'); f" ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1ce910> >" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "aut = f.translate('det', 'Buchi', 'SBAcc'); aut" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The above automaton is not minimal and is easily reduced by `sat_minimize()`:" ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1ce430> >" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(aut)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Note that by default SAT-minimize produces a transition-based automaton with the same acceptance condition. State-based acceptance can be requested with the `state_based` option:" ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1ce940> >" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(aut, state_based=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Minimizing deterministic ω-automata with arbitrary acceptance condition\n", "\n", "Now let's look at examples with more complicated acceptance conditions. \n", "The following Rabin automaton was produced using ltl2dstar 0.5.4 and spot 2.5.2 with\n", "```\n", "ltlfilt --lbt -f '(FGa | Fb) & FGc' | ltl2dstar -H --ltl2nba=spin:ltl2tgba@-Ds - -\n", "```\n", "however we hardcode it so that the notebook can be used even with `ltl2dstar` installed." ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cefa0> >" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "large = spot.automaton('''\n", "HOA: v1 States: 6 properties: implicit-labels trans-labels no-univ-branch\n", "deterministic complete stutter-invariant tool: \"ltl2dstar\" \"0.5.4\"\n", "name: \"& | F G a F b F G c\" comment: \"Safra[NBA=4]\" acc-name: Rabin 2\n", "Acceptance: 4 (Fin(0)&Inf(1))|(Fin(2)&Inf(3)) Start: 5 AP: 3 \"a\" \"b\"\n", "\"c\" --BODY-- State: 0 {1 3} 4 4 4 4 1 0 1 0 State: 1 {0 3} 4 4 4 4 1 1\n", "1 1 State: 2 {1 2} 4 4 4 4 2 2 2 2 State: 3 {1 2} 5 5 4 4 5 3 4 0 State:\n", "4 {0 2} 4 4 4 4 2 2 2 2 State: 5 {0 2} 5 5 4 4 5 3 2 2 --END--''')\n", "large.merge_edges()\n", "large" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "It can be minimized as a 2-state transition-based Rabin automaton:" ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cee80> >" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "small = spot.sat_minimize(large); small" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Or as a 4-state state-based Rabin automaton:" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cec40> >" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(large, state_based=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "But do we really need 2 Rabin pairs? Let's ask if we can get an equivalent with only one pair. (Note that reducing the number of pairs might require more state, but the `sat_minimize()` function will never attempt to add state unless explicitly instructed to do so. In this case we are therefore looking for a state-based Rabin-1 automaton with at most 4 states.)" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cebb0> >" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(large, state_based=True, acc='Rabin 1')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Using the `display_log` option, we can have a hint of what is going on under the hood. Each line in the table shows one call to the SAT solver. The column labeled `target.states` gives the size of the equivalent automaton we ask the SAT-solver to produce, but some of these states may actually be unreachable in the result. The `variables` and `clauses` columns give an indication of the size of the SAT problem. The `enc.*` and `sat.*` columns give the user and system time taken to encode and solve the SAT problem (the unit is \"ticks\", which usually is 1/100 of seconds).\n", "\n", "Below we see that the minimization procedure first tried to squeeze the 6-state input into a 3-state automaton, which failed, and then into a 5-state automaton, which was successful. This 5-state automaton was used as input to produce a smaller 4-state automaton.. Essentially this procedure is doing a binary search towards the minimal size. \n", "\n", "(In this case it does not matter, but be aware that the number of states displayed in the log table are those of complete automata, while the output of `sat_minimize()` is trimmed by default.)" ] }, { "cell_type": "code", "execution_count": 10, "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", " \n", "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user
0	6	3	NaN	NaN	NaN	996	48806	2	0
1	6	5	5	16	40	2760	224707	5	5
2	5	4	4	11	32	2008	155020	3	3

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 6 3 NaN NaN NaN 996 \n", "1 6 5 5 16 40 2760 \n", "2 5 4 4 11 32 2008 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 48806 2 0 0 0 \n", "1 224707 5 0 5 0 \n", "2 155020 3 0 3 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f611de5a370> >" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(large, state_based=True, acc='Rabin 1', display_log=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Note that we already had a smaller transition-based automaton for this language (in the `small` variable), and that it actually is more efficient to work from that, as seen in problem sizes displayed in the following log." ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user
0	2	3	NaN	NaN	NaN	348	15974	0	1
1	2	5	5	17	40	960	73187	2	1
2	2	4	4	11	32	616	37620	1	0

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 2 3 NaN NaN NaN 348 \n", "1 2 5 5 17 40 960 \n", "2 2 4 4 11 32 616 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 15974 0 0 1 0 \n", "1 73187 2 0 1 0 \n", "2 37620 1 0 0 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cf870> >" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(small, state_based=True, acc='Rabin 1', display_log=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "How did the procedure look for a complete automaton of size 5 when the input had only 2 states? It's because the input uses transition-based acceptance: to estimate an upper bound of the size of the state-based output, the `sat_minimize()` procedure converted its transition-based input to state-based acceptance (using the `spot.sbacc()` function) and counted the number of states in the result.\n", "\n", "Such an estimate is not necessarily correct if we request a different acceptance condition. In that case we can actually change the upper-bound using `max_states`. Below we additionally demonstrate the use of the `colored` option, to request all transitions to belong to exactly one set, as customary in parity automata." ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user
0	2	5	5	19	40	2300	288887	8	12
1	2	2	2	6	16	368	18569	1	0
2	2	1	NaN	NaN	NaN	92	2337	0	0

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 2 5 5 19 40 2300 \n", "1 2 2 2 6 16 368 \n", "2 2 1 NaN NaN NaN 92 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 288887 8 0 12 0 \n", "1 18569 1 0 0 0 \n", "2 2337 0 0 0 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cf960> >" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(small, max_states=9, acc='parity min odd 3', colored=True, display_log=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "There are a couple of ways in which we can influence the search for the minimum automaton. We can disable the binary search with `sat_naive`. In this case, the procedure will try to remove one state at a time. This is not necessary slower than the default binary search, because satisfiable problems are often solved more quickly than unsatisfiable ones." ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user
0	6	6	5	13	40	2742	173183	4	2
1	5	4	4	11	32	964	45412	1	0
2	4	3	NaN	NaN	NaN	363	10496	1	0

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 6 6 5 13 40 2742 \n", "1 5 4 4 11 32 964 \n", "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 173183 4 0 2 0 \n", "1 45412 1 0 0 0 \n", "2 10496 1 0 0 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f611de5b3c0> >" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(large, acc='co-Buchi', sat_naive=True, state_based=True, display_log=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Variant for incremental SAT solving\n", "\n", "Using `sat_incr=1`, we encode the problem of finding an equivalent automaton with $n$ states, and add 6 additional variables and some additional constraints to the problem:\n", "\n", "| variable | implied constraints |\n", "| :--- | ---: |\n", "| $v_1$ | transitions to state $(n-1)$ must not be used | \n", "| $v_2$ | $v_1\\land{}$ transitions to state $(n-2)$ must not be used |\n", "| ... | |\n", "| $v_6$ | $v_5\\land{}$ transitions to state $(n-5)$ must not be used |\n", "\n", "Now using `assume` directives on variable $v_i$ amounts to testing whether the problem is solved with $n-i$ states, but we do not have to reencode the problem for each test, and the solver can (probably) reuse some of the knowledge it gathered during a previous attempt. We do a binary search on these 6 assumptions, to find some $i$ such that the problem is satisfiable with assumption $v_i$ but not with $v_{i+1}$. If such cast exists, we have found the minimal automaton. If assumption $v_6$ is satisfiable, we re-encode the problem with $n-7$ states and start over. Watch how the number of variables and clauses do not change in the following log.\n", "\n", "The number of assumption variables to use in a one encoding can be set with the `sat_incr_steps` argument. Its default value of 6 was chosen empirically by benchmarking different values." ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user
0	6	1	NaN	NaN	NaN	2747	173427	3	2
1	6	3	NaN	NaN	NaN	2747	173427	0	0
2	6	4	4	12	32	2747	173427	0	1

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 6 1 NaN NaN NaN 2747 \n", "1 6 3 NaN NaN NaN 2747 \n", "2 6 4 4 12 32 2747 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 173427 3 0 2 0 \n", "1 173427 0 0 0 0 \n", "2 173427 0 0 1 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f611de5b600> >" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(large, acc='co-Buchi', sat_incr=1, state_based=True, display_log=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Another incremental variant consists is the equivalent of forcing $v_1$, $v_2$, ... in order. But to do that we do not need to use any assumption. We just add the constraints that transitions going to state $n-i$ are forbidden. This variant is enabled by option `sat_incr=2`. As in the previous case, we do a few of those incremental steps (2 by default, but that can be changed with the `sat_incr_steps` parameter) and then we reencode the problem to reduce its size.\n", "\n", "In the log below, line 0 corresponds to the search of an equivalent automaton with the same size, but the simpler co-Büchi acceptance. It works, and most of the time was spent encoding the problem. Then for the next two lines, the minimization function looks for automata of size 5 and 4 without reencoding the problem but simply adding a few constraints to disable the relevant transitions." ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user
0	6	6	5	13	40	2742	173183	4	2
1	5	4	4	12	32	2742	173279	0	0
2	4	3	NaN	NaN	NaN	2742	173327	0	0

\n", "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user	automaton
0	6	6	5	13	40	2742	173183	4	2	HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...
1	5	4	4	12	32	2742	173279	0	0	HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a...
2	4	3	NaN	NaN	NaN	2742	173327	0	0	NaN

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 6 6 5 13 40 2742 \n", "1 5 4 4 12 32 2742 \n", "2 4 3 NaN NaN NaN 2742 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \\\n", "0 173183 4 0 2 0 \n", "1 173279 0 0 0 0 \n", "2 173327 0 0 0 0 \n", "\n", " automaton \n", "0 HOA: v1 States: 5 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", "1 HOA: v1 States: 4 Start: 0 AP: 3 \"a\" \"c\" \"b\" a... \n", "2 NaN " ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "aut, log = spot.sat_minimize(large, acc='co-Buchi', sat_incr=2, state_based=True, return_log=True)\n", "display(aut)\n", "display(log)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Here is how we can extract the automata from that log:" ] }, { "cell_type": "code", "execution_count": 17, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "automaton from line 0:\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f611de94660> >" ] }, "metadata": {}, "output_type": "display_data" }, { "name": "stdout", "output_type": "stream", "text": [ "automaton from line 1:\n" ] }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f611de946f0> >" ] }, "metadata": {}, "output_type": "display_data" } ], "source": [ "for line, data in log.iterrows():\n", " if type(data.automaton) is str:\n", " print(\"automaton from line {}:\".format(line))\n", " display(spot.automaton(data.automaton + \"\\n\"))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## `sat_langmap`\n", "\n", "When using the default binary search approach, the `sat_langmap=True` can help refine the lower bound by first testing the language-equivalence of all states in the automaton. This allows to form equivalence classes of states, and clearly the minimal automaton needs at least as many states as the number of equivalence states.\n", "\n", "For instance in the `large` automaton we use as example, the 6 states correspond to only two different languages. This can be seen with the `highlight_language()` function, which colors states with identical languages. This information can be used by the minimization function to search a minimal automaton between 2 and 6 states." ] }, { "cell_type": "code", "execution_count": 18, "metadata": {}, "outputs": [ { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cefa0> >" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.highlight_languages(large); large" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Compare the next two logs, with and without `sat_langmap`." ] }, { "cell_type": "code", "execution_count": 19, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	enc.sys	sat.user	sat.sys
0	6	3	NaN	NaN	NaN	687	21896	1	0	0	0
1	6	5	4	12	32	1905	100457	2	0	2	0

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 6 3 NaN NaN NaN 687 \n", "1 6 5 4 12 32 1905 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 21896 1 0 0 0 \n", "1 100457 2 0 2 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f61ac1cf6c0> >" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# Binary search between 1 and 6\n", "spot.sat_minimize(large, acc='co-Buchi', state_based=True, display_log=True)" ] }, { "cell_type": "code", "execution_count": 20, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	sat.user
0	6	4	4	12	32	1220	51612	1	1
1	4	2	NaN	NaN	NaN	162	3129	0	0
2	4	3	NaN	NaN	NaN	363	10496	0	0

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 6 4 4 12 32 1220 \n", "1 4 2 NaN NaN NaN 162 \n", "2 4 3 NaN NaN NaN 363 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 51612 1 0 1 0 \n", "1 3129 0 0 0 0 \n", "2 10496 0 0 0 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f611de5b960> >" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "# Binary search between 2 and 6 thanks to sat_langmap\n", "spot.sat_minimize(large, acc='co-Buchi', sat_langmap=True, state_based=True, display_log=True)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### `states`\n", "\n", "Sometimes we do not want a minimization loop, we just want to generate an equivalent automaton with a given number of states. In that case, we use the `states` option. However there is no constraint that all states should be reachable, so in the end, you could end with an automaton with fewer states than requested." ] }, { "cell_type": "code", "execution_count": 21, "metadata": {}, "outputs": [ { "data": { "text/html": [ "

	input.states	target.states	reachable.states	edges	transitions	variables	clauses	enc.user	enc.sys	sat.user	sat.sys
0	2	7	7	23	56	1379	89168	2	0	1	0

\n", "

" ], "text/plain": [ " input.states target.states reachable.states edges transitions variables \\\n", "0 2 7 7 23 56 1379 \n", "\n", " clauses enc.user enc.sys sat.user sat.sys \n", "0 89168 2 0 1 0 " ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "image/svg+xml": [ "\n", "\n", "\n", "\n", "\n" ], "text/html": [ "\n", "\n", "\n", "\n", "\n" ], "text/plain": [ " *' at 0x7f611de5b570> >" ] }, "execution_count": 21, "metadata": {}, "output_type": "execute_result" } ], "source": [ "spot.sat_minimize(small, acc=\"co-Buchi\", states=7, state_based=True, display_log=True)" ] } ], "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.11.7" } }, "nbformat": 4, "nbformat_minor": 2 }