diff --git a/NEWS b/NEWS index 3ad57d31d..d8fd0ab70 100644 --- a/NEWS +++ b/NEWS @@ -1,5 +1,11 @@ New in spot 2.11.1.dev (not yet released) + Library: + + - spot::reduce_parity() now has a "layered" option to force all + transition in the same parity layer to receive the same color; + like acd_transform() would do. + Bugs fixed: - Fix pkg-config files containing @LIBSPOT_PTHREAD@ (issue #520) diff --git a/spot/twaalgos/parity.cc b/spot/twaalgos/parity.cc index 94c7bd922..9428d7bb5 100644 --- a/spot/twaalgos/parity.cc +++ b/spot/twaalgos/parity.cc @@ -388,14 +388,14 @@ namespace spot } twa_graph_ptr - reduce_parity(const const_twa_graph_ptr& aut, bool colored) + reduce_parity(const const_twa_graph_ptr& aut, bool colored, bool layered) { return reduce_parity_here(make_twa_graph(aut, twa::prop_set::all()), - colored); + colored, layered); } twa_graph_ptr - reduce_parity_here(twa_graph_ptr aut, bool colored) + reduce_parity_here(twa_graph_ptr aut, bool colored, bool layered) { unsigned num_sets = aut->num_sets(); if (!colored && num_sets == 0) @@ -507,15 +507,30 @@ namespace spot m.first += (piri - m.first) & 1; m.second += (piri - m.second) & 1; } - for (unsigned state: si.states_of(scc)) - for (auto& e: aut->out(state)) - if ((sba || si.scc_of(e.dst) == scc) && - ((piri >= 0 && e.acc.has(color)) || (piri < 0 && !e.acc))) - { - unsigned en = aut->edge_number(e); - piprime1[en] = m.first; - piprime2[en] = m.second; - } + // Recolor edges. Depending on LAYERED we want to + // either recolor all edges for which piprime1 is -2 + // (uncolored), or only the edges that we were removed + // by the previous filter. + auto coloredge = [&](auto& e) { + unsigned en = aut->edge_number(e); + bool recolor = layered + ? piprime1[en] == -2 + : (piri >= 0 && e.acc.has(color)) || (piri < 0 && !e.acc); + if (recolor) + { + piprime1[en] = m.first; + piprime2[en] = m.second; + } + }; + if (sba) + // si.edges_of(scc) would be wrong as it can ignore + // outgoing edges removed from a previous level. + for (unsigned s: si.states_of(scc)) + for (auto& e: aut->out(s)) + coloredge(e); + else + for (auto& e: si.inner_edges_of(scc)) + coloredge(e); res.first = std::max(res.first, m.first); res.second = std::max(res.second, m.second); } diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index 167c6b2d8..44d7cca7e 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2016-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2016-2019, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -134,7 +134,6 @@ namespace spot colorize_parity_here(twa_graph_ptr aut, bool keep_style = false); /// @} - /// \brief Reduce the parity acceptance condition to use a minimal /// number of colors. /// @@ -149,11 +148,51 @@ namespace spot /// the above paper assumes). Otherwise, the smallest or highest /// colors (depending on the parity kind) is removed to simplify the /// acceptance condition. + /// + /// If the input uses state-based acceptance, the output will use + /// state-based acceptance as well. + /// + /// A parity automaton, sometimes called a chain automaton, can be + /// seen as a stack of layers that are alternatively rejecting and + /// accepting. For instance imagine a parity max automaton that is + /// strongly connected. Removing the transitions with the maximal + /// color might leave a few transitions that were not labeled by + /// this maximal color, but that are part of any cycle anymore: + /// those transition could have been colored with the maximal color, + /// since any cycle going through them would have seen the maximal + /// color. (Once your remove this maximal layer, + /// your can define the next layer similarly.) + /// + /// When \a layered is true all transition that belong to the same + /// layer receive the same color. When layer is `false`, only the + /// transition that where used initially to define the layers (i.e, + /// the transition with the maximal color in the previous exemple), + /// get their color adjusted. The other will receive either no + /// color (if \a colored is false), or a useless color (if \a colored + /// is true). Here "useless color" means the smallest color + /// for parity max, and the largest color for parity min. + /// + /// When \a layered is true, the output of this function is + /// comparable to what acd_transform() would produce. The + /// difference is that this function preserve the kind (min/max) of + /// parity input, while acd_transform() always output a parity min + /// automaton. Additionally, this function needs fewer resources + /// than acd_transform() because it is already known that the input + /// is a parity automaton. In some (historically inaccurate) way, + /// reduce_parity() can be seen as a specialized version of + /// acd_transform(). + /// + /// The reason layered is false by default, is that not introducing + /// colors in place where there where none occasionally help with + /// simulation-based reductions. + /// /// @{ SPOT_API twa_graph_ptr - reduce_parity(const const_twa_graph_ptr& aut, bool colored = false); + reduce_parity(const const_twa_graph_ptr& aut, + bool colored = false, bool layered = false); SPOT_API twa_graph_ptr - reduce_parity_here(twa_graph_ptr aut, bool colored = false); + reduce_parity_here(twa_graph_ptr aut, + bool colored = false, bool layered = false); /// @} } diff --git a/tests/python/parity.ipynb b/tests/python/parity.ipynb index 7323717da..56d6af350 100644 --- a/tests/python/parity.ipynb +++ b/tests/python/parity.ipynb @@ -72,9 +72,9 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "Of course the case of parity automata with a single color is a bit degenerate, as the same formula correspond to two parity conditions with different kinds. \n", + "Of course the case of parity automata with a single color is a bit degenerate, as the same formula corresponds to two parity conditions of different kinds. \n", "\n", - "In addition the the above, an automaton is said to be **colored** if each of its edges (or states) has exactly one color. Automata that people usually call *parity automata* correspond in Spot to *colored* automata with *parity acceptance*. For this reason try to use the term *automata with parity acceptance* rather than *parity automata* for automata that are not *colored*." + "In addition to the above, an automaton is said to be **colored** if each of its edges (or states) has exactly one color. Automata that people usually call *parity automata* correspond in Spot to *colored* automata with *parity acceptance*. For this reason try to use the term *automata with parity acceptance* rather than *parity automata* for automata that are not *colored*." ] }, { @@ -3009,11 +3009,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[co-Büchi]\n", + "\n", + "\n", + "\n", + "[co-Büchi]\n", "\n", "\n", "\n", @@ -3237,11 +3237,11 @@ "\n", "\n", - "\n", - "\n", - "\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "[Büchi]\n", "\n", "\n", "\n", @@ -4223,14 +4223,15 @@ "\n", "# Reduce parity\n", "\n", - "The `reduce_parity()` function is a more elaborate version of `cleanup_parity()`. It implements an algorithm by Carton and Maceiras (*Computing the Rabin index of a parity automaton*, Informatique théorique et applications, 1999), to obtain the minimal parity acceptance condition for a given automaton. Why the original algorithm assume *max odd* parity, this version with work with the four types of parity acceptance. It will only try to preserve the kind (max/min) and may change the style if it allows saving one color. Furthermore, it can colorize (or uncolorize) automata at the same time,\n", + "The `reduce_parity()` function is a more elaborate version of `cleanup_parity()`. It implements an algorithm by Carton and Maceiras (*Computing the Rabin index of a parity automaton*, Informatique théorique et applications, 1999), to obtain the minimal parity acceptance condition for a given automaton. While the original algorithm assumes *max odd* parity, this version works with the four types of parity acceptance. It will only try to preserve the kind (max/min) and may change the style if it allows saving one color. Furthermore, it can colorize (or uncolorize) automata at the same time,\n", "making it a very nice replacement for both `cleanup_parity()` and `colorize_parity()`.\n", "\n", - "It takes two arguments:\n", + "It takes three arguments:\n", "1. the automaton whose parity acceptance condition should be reduced\n", "2. a Boolean indicating whether the output should be colored (`True`), or if transition with no color can be used (`False`).\n", + "3. a Boolean indicating whether the output should be layered, i.e., in a max parity automaton, that means the color of a transition should be the maximal color visited by all cycles going through it.\n", "\n", - "By default, the second argument is `False`, because acceptance sets is a scarse ressource in Spot." + "By default, the second argument is `False`, because acceptance sets is a scarse ressource in Spot. The third argument also defaults to `False`, but for empircal reason: adding more colors like this tends to hinder simulation-based reductions." ] }, { @@ -4715,8 +4716,8 @@ "outputs": [ { "data": { - "text/html": [ - "
\n", + "image/svg+xml": [ + "\n", "\n", "\n", - "\n", - "\n", - "\n", - "\n", - "Fin(\n", - "❸\n", - ") & (Inf(\n", - "❷\n", - ") | (Fin(\n", - "❶\n", - ") & Inf(\n", - "⓿\n", - ")))\n", - "[parity max even 4]\n", - "\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!p0 & p1\n", - "\n", - "\n", - "\n", - "3->0\n", - "\n", - "\n", - "p0 & !p1\n", - "❷\n", - "\n", - "\n", - "\n", - "3->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "❸\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!p0 & p1\n", - "❷\n", - "\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!p0 & p1\n", - "⓿\n", - "❷\n", - "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!p0 & !p1\n", - "\n", - "\n", - "\n", "
\n", "\n", @@ -5188,17 +5074,263 @@ }, "metadata": {}, "output_type": "display_data" + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "❶\n", + ") & Inf(\n", + "⓿\n", + ")\n", + "[parity max even 2]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Fin(\n", + "❷\n", + ") & (Inf(\n", + "❶\n", + ") | Fin(\n", + "⓿\n", + "))\n", + "[parity max odd 3]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "2\n", + "\n", + "2\n", + "\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "\n", + "0->3\n", + "\n", + "\n", + "!p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "2->1\n", + "\n", + "\n", + "!p0 & p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", + "p0 & !p1\n", + "❶\n", + "\n", + "\n", + "\n", + "3->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "❷\n", + "\n", + "\n", + "\n", + "3->3\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "1->0\n", + "\n", + "\n", + "!p0 & p1\n", + "❶\n", + "\n", + "\n", + "\n", + "1->2\n", + "\n", + "\n", + "!p0 & !p1\n", + "⓿\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" } ], "source": [ - "display2(maxeven4, spot.reduce_parity(maxeven4))\n", - "display2(maxeven4, spot.reduce_parity(maxeven4, True))" + "display(maxeven4)\n", + "display2(spot.reduce_parity(maxeven4), spot.reduce_parity(maxeven4, True))\n", + "display2(spot.reduce_parity(maxeven4, False, True), spot.reduce_parity(maxeven4, True, True))" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -5212,7 +5344,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.10.7" } }, "nbformat": 4,