From 4711dcd74fb9a48aa9f246c25bb2d66694c9edde Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 3 Nov 2017 17:01:05 +0100 Subject: [PATCH] introduce stutter_invariant_letters() * spot/twaalgos/stutter.cc, spot/twaalgos/stutter.hh (stutter_invariant_letters) (stutter_invariant_states): Get rid of the broken local variant. * tests/python/stutter-inv.ipynb, NEWS: Document. * python/spot/impl.i: Bind vector. --- NEWS | 3 +- python/spot/impl.i | 1 + spot/twaalgos/stutter.cc | 96 +++++- spot/twaalgos/stutter.hh | 32 +- tests/python/stutter-inv.ipynb | 602 ++++++++------------------------- 5 files changed, 254 insertions(+), 480 deletions(-) diff --git a/NEWS b/NEWS index 2532f5c4a..83b2f4882 100644 --- a/NEWS +++ b/NEWS @@ -133,8 +133,7 @@ New in spot 2.4.1.dev (not yet released) - In addition to detecting stutter-invariant formulas/automata, some can now study a stutter-sensitive automaton and detect the subset of states that are stutter-invariant. See - https://spot.lrde.epita.fr/ipynb/stutter-inv-states.html for - examples. + https://spot.lrde.epita.fr/ipynb/stutter-inv.html for examples. - Determinization has been heavily rewritten and optimized. The algorithm has (almost) not changed, but it runs muuuch faster now. It also features an diff --git a/python/spot/impl.i b/python/spot/impl.i index 32dec7582..76df4800d 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -431,6 +431,7 @@ namespace std { %template(vectorformula) vector; %template(vectorunsigned) vector; %template(vectorbool) vector; + %template(vectorbdd) vector; %template(vectorstring) vector; %template(atomic_prop_set) set; %template(relabeling_map) map; diff --git a/spot/twaalgos/stutter.cc b/spot/twaalgos/stutter.cc index ec6f25a2d..579651738 100644 --- a/spot/twaalgos/stutter.cc +++ b/spot/twaalgos/stutter.cc @@ -686,21 +686,19 @@ namespace spot } std::vector - stutter_invariant_states(const_twa_graph_ptr pos, formula f, - bool local) + stutter_invariant_states(const_twa_graph_ptr pos, formula f) { if (f.is_syntactic_stutter_invariant() || pos->prop_stutter_invariant().is_true()) return std::vector(pos->num_states(), true); auto neg = translator(pos->get_dict()).run(formula::Not(f)); - return stutter_invariant_states(pos, neg, local); + return stutter_invariant_states(pos, neg); } // Based on an idea by Joachim Klein. std::vector stutter_invariant_states(const_twa_graph_ptr pos, - const_twa_graph_ptr neg, - bool local) + const_twa_graph_ptr neg) { std::vector res(pos->num_states(), true); if (pos->prop_stutter_invariant().is_true()) @@ -750,8 +748,83 @@ namespace spot continue; for (auto& e: prod->out(s)) if (si.is_useful_scc(si.scc_of(e.dst))) - if (!local || pairs.find((*prod_pairs)[e.dst]) == pairs.end()) - res[(*prod_pairs)[s].first] = sinv = false; + res[(*prod_pairs)[s].first] = sinv = false; + } + std::const_pointer_cast(pos)->prop_stutter_invariant(sinv); + std::const_pointer_cast(neg)->prop_stutter_invariant(sinv); + return res; + } + + std::vector + stutter_invariant_letters(const_twa_graph_ptr pos, formula f) + { + if (f.is_syntactic_stutter_invariant() + || pos->prop_stutter_invariant().is_true()) + { + std::const_pointer_cast(pos)->prop_stutter_invariant(true); + return stutter_invariant_letters(pos); + } + auto neg = translator(pos->get_dict()).run(formula::Not(f)); + return stutter_invariant_letters(pos, neg); + } + + std::vector + stutter_invariant_letters(const_twa_graph_ptr pos, + const_twa_graph_ptr neg) + { + unsigned ns = pos->num_states(); + std::vector res(ns, bddtrue); + if (pos->prop_stutter_invariant().is_true()) + return res; + + if (neg == nullptr) + { + spot::postprocessor p; + p.set_type(spot::postprocessor::Generic); + p.set_pref(spot::postprocessor::Deterministic); + p.set_level(spot::postprocessor::Low); + neg = dualize(p.run(std::const_pointer_cast(pos))); + } + + auto product_states = [](const const_twa_graph_ptr& a) + { + return (a->get_named_prop>> + ("product-states")); + }; + + // Get the set of states (x,y) that appear in the product P1=pos*neg. + std::set> pairs = [&]() + { + twa_graph_ptr prod = spot::product(pos, neg); + auto goodstates = product_states(prod); + std::set> pairs(goodstates->begin(), + goodstates->end()); + return pairs; + }(); + + // Compute P2=cl(pos)*cl(neg). A state x of pos is stutter-sensitive + // if there exists a state (x,y) in both P1 and P2 that as a successor + // in the useful part of P2 and that is not in P1. + twa_graph_ptr prod = spot::product(closure(pos), closure(neg)); + auto prod_pairs = product_states(prod); + scc_info si(prod, scc_info_options::TRACK_SUCCS + | scc_info_options::TRACK_STATES_IF_FIN_USED); + si.determine_unknown_acceptance(); + unsigned n = prod->num_states(); + bool sinv = true; + + for (unsigned s = 0; s < n; ++s) + { + if (!si.is_useful_scc(si.scc_of(s))) + continue; + if (pairs.find((*prod_pairs)[s]) == pairs.end()) + continue; + for (auto& e: prod->out(s)) + if (si.is_useful_scc(si.scc_of(e.dst))) + { + sinv = false; + res[(*prod_pairs)[s].first] -= e.cond; + } } std::const_pointer_cast(pos)->prop_stutter_invariant(sinv); std::const_pointer_cast(neg)->prop_stutter_invariant(sinv); @@ -784,17 +857,16 @@ namespace spot void highlight_stutter_invariant_states(twa_graph_ptr pos, - formula f, unsigned color, - bool local) + formula f, unsigned color) { - highlight_vector(pos, stutter_invariant_states(pos, f, local), color); + highlight_vector(pos, stutter_invariant_states(pos, f), color); } void highlight_stutter_invariant_states(twa_graph_ptr pos, const_twa_graph_ptr neg, - unsigned color, bool local) + unsigned color) { - highlight_vector(pos, stutter_invariant_states(pos, neg, local), color); + highlight_vector(pos, stutter_invariant_states(pos, neg), color); } } diff --git a/spot/twaalgos/stutter.hh b/spot/twaalgos/stutter.hh index bebb5910e..f8576ec9b 100644 --- a/spot/twaalgos/stutter.hh +++ b/spot/twaalgos/stutter.hh @@ -219,12 +219,10 @@ namespace spot /// automaton, or supplying a formula for the (positive) automaton. SPOT_API std::vector stutter_invariant_states(const_twa_graph_ptr pos, - const_twa_graph_ptr neg = nullptr, - bool local = false); + const_twa_graph_ptr neg = nullptr); SPOT_API std::vector - stutter_invariant_states(const_twa_graph_ptr pos, formula f_pos, - bool local = false); + stutter_invariant_states(const_twa_graph_ptr pos, formula f_pos); ///@} ///@{ @@ -246,12 +244,30 @@ namespace spot /// setup the "highlight-states" property of the automaton. SPOT_API void highlight_stutter_invariant_states(twa_graph_ptr pos, - formula f_pos, unsigned color = 0, - bool local = false); + formula f_pos, unsigned color = 0); SPOT_API void highlight_stutter_invariant_states(twa_graph_ptr pos, const_twa_graph_ptr neg = nullptr, - unsigned color = 0, - bool local = false); + unsigned color = 0); ///@} + + ///@{ + /// \ingroup stutter_inv + /// \brief Determinate the letters with which each state is + /// stutter-invariant. + /// + /// A state q is stutter-invariant for ℓ iff the membership to L(q) + /// of any word starting with ℓ is unchanged by duplicating any + /// letter, or removing a duplicate letter. + /// + /// The algorithm needs to compute the complement of \a pos. You can + /// avoid that costly operation by either supplying the complement + /// automaton, or supplying a formula for the (positive) automaton. + SPOT_API std::vector + stutter_invariant_letters(const_twa_graph_ptr pos, + const_twa_graph_ptr neg = nullptr); + + SPOT_API std::vector + stutter_invariant_letters(const_twa_graph_ptr pos, formula f_pos); + /// @} } diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index bb104dbad..a86cf9d79 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -354,7 +354,7 @@ "\n" ], "text": [ - " *' at 0x7f1c8045a660> >" + " *' at 0x7f71841135d0> >" ] }, { @@ -411,7 +411,7 @@ "language": "python", "metadata": {}, "outputs": [], - "prompt_number": 25 + "prompt_number": 11 }, { "cell_type": "code", @@ -432,7 +432,7 @@ ] } ], - "prompt_number": 26 + "prompt_number": 12 }, { "cell_type": "markdown", @@ -626,7 +626,7 @@ "\n" ], "text": [ - " *' at 0x7f1c803f4de0> >" + " *' at 0x7f71840b9b40> >" ] } ], @@ -816,7 +816,7 @@ "\n" ], "text": [ - " *' at 0x7f1c803f4de0> >" + " *' at 0x7f71840b9b40> >" ] } ], @@ -979,7 +979,7 @@ "\n" ], "text": [ - " *' at 0x7f1c80480540> >" + " *' at 0x7f7184113480> >" ] }, { @@ -1066,7 +1066,7 @@ "\n" ], "text": [ - " *' at 0x7f1c8045a6c0> >" + " *' at 0x7f71841135a0> >" ] } ], @@ -1259,7 +1259,7 @@ "\n" ], "text": [ - " *' at 0x7f1c80480660> >" + " *' at 0x7f71840b9a80> >" ] } ], @@ -1271,17 +1271,17 @@ "source": [ "### Third example\n", "\n", - "These procedures work regardless of the acceptance condition. Here is an example with state-based co-B\u00fcchi acceptance.\n", + "These procedures work regardless of the acceptance condition. Here is an example with co-B\u00fcchi acceptance.\n", "\n", - "In this case we do not even have a formula to pass as second argument, so the check will perform a costly complementation by determinization." + "In this case we do not even have a formula to pass as second argument, so the check will perform a complementation by determinization." ] }, { "cell_type": "code", "collapsed": false, "input": [ - "aut = spot.automaton('genaut --ks-nca=2 |')\n", - "spot.highlight_stutter_invariant_states(aut, None, 5, True)\n", + "aut = spot.automaton('randaut --seed=30 -Q4 -A\"Fin(0)\" a |')\n", + "spot.highlight_stutter_invariant_states(aut, None, 5)\n", "display(aut)" ], "language": "python", @@ -1297,140 +1297,87 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Fin(\n", - "\u24ff\n", - ")\n", - "[co-B\u00fcchi]\n", + "\n", + "Fin(\n", + "\u24ff\n", + ")\n", + "[co-B\u00fcchi]\n", "\n", "\n", "0\n", - "\n", - "0\n", - "\u24ff\n", + "\n", + "0\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "1\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", "\n", "\n", - "2\n", - "\n", - "2\n", + "2\n", + "\n", + "2\n", "\n", "\n", - "0->2\n", - "\n", - "\n", - "1\n", + "0->2\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "2->0\n", + "\n", + "\n", + "!a\n", "\n", "\n", "3\n", - "\n", - "3\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1->0\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "1->1\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "(!a & b) | (a & !b)\n", - "\n", - "\n", - "2->1\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "2->2\n", - "\n", - "\n", - "(!a & !b) | (a & b)\n", + "\n", + "3\n", "\n", "\n", - "2->3\n", - "\n", - "\n", - "a & !b\n", + "2->3\n", + "\n", + "\n", + "!a\n", "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a | b\n", + "\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a & !b\n", + "\n", + "1->3\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "4->1\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "!a | b\n", + "\n", + "3->1\n", + "\n", + "\n", + "!a\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f1c80370300> >" + " *' at 0x7f7184137690> >" ] } ], - "prompt_number": 27 + "prompt_number": 21 }, { "cell_type": "markdown", @@ -1443,19 +1390,27 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "## Global vs Local stuttering (experimental)\n", + "## Sutter-invariance at the letter level\n", "\n", - "Do not build anything on top of what follows, as it is likely to be removed." + "Instead of marking each state as stuttering or not, we can list the letters that we can stutter in each state.\n", + "More precisely, a state $q$ is _stutter-invariant for letter $a$_ if the membership to $L(q)$ of any word starting with $a$ is preserved by the operations that duplicate letters or remove duplicates. \n", + "\n", + "$(\\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_{i+1}\\ldots\\in L(q) \\land \\ell_0=a) \\iff (\\ell_0\\ldots\\ell_{i-1}\\ell_i\\ell_i\\ell_{i+1}\\ldots\\in L(q)\\land \\ell_0=a)$\n", + "\n", + "Under this definition, we can also say that $q$ is _stutter-invariant_ iff it is _stutter-invariant for any letter_.\n", + "\n", + "For instance consider the following automaton, for which all words that start with $b$ are stutter invariant.\n", + "The initial state may not be declared as stutter-invariant because of words that start with $\\lnot b$." ] }, { "cell_type": "code", "collapsed": false, "input": [ - "h = spot.formula('F(a & X(!a & X(b & Xb)))')\n", - "aut = spot.translate(h)\n", - "spot.highlight_stutter_invariant_states(aut, h, 5)\n", - "display(aut)" + "f = spot.formula('(!b&Xa) | Gb')\n", + "pos = spot.translate(f)\n", + "spot.highlight_stutter_invariant_states(pos, f, 5)\n", + "display(pos)" ], "language": "python", "metadata": {}, @@ -1470,88 +1425,78 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "[B\u00fcchi]\n", + "\n", + "Inf(\n", + "\u24ff\n", + ")\n", + "[B\u00fcchi]\n", "\n", + "\n", + "3\n", + "\n", + "3\n", + "\n", + "\n", + "I->3\n", + "\n", + "\n", + "\n", "\n", - "0\n", - "\n", - "0\n", + "0\n", + "\n", + "0\n", "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", + "\n", + "3->0\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "1\n", - "\n", - "1\n", + "1\n", + "\n", + "1\n", + "\u24ff\n", "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", + "\n", + "3->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "2\n", - "\n", - "2\n", + "\n", + "2\n", + "\u24ff\n", "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", "\n", - "\n", - "3\n", - "\n", - "3\n", + "\n", + "2->2\n", + "\n", + "\n", + "1\n", "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "1\n", - "\u24ff\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f1c8045a690> >" + " *' at 0x7f71840b9b70> >" ] } ], @@ -1561,293 +1506,34 @@ "cell_type": "markdown", "metadata": {}, "source": [ - "The above result uses a natural definition of \"stutter-invariant state\": a state is stutter-invariant if the language accepted from this state is.\n", + "The `stutter_invariant_letters()` functions returns a vector of BDDs indexed by state numbers. The BDD at index $q$ specifies all letters $\\ell$ for which state $q$ would be stuttering. Note that if $q$ is stutter-invariant or reachable from a stutter-invariant state, the associated BDD will be `bddtrue` (printed as `1` below).\n", "\n", - "We can also have a \"local\" variant of the stutter invariance check that considers the state as stutter invariant if you can stutter on (or remove duplicates of) the first letter read from that state, but not necessary do the same operations on a different letter that follows. \n", - "In other words, state $q$ is a local stutter-invariant state iff $\\ell_1\\ell_2\\ldots \\in L(q) \\iff \\ell_1\\ell_1\\ell_2\\ldots \\in L(q)$.\n", - "\n", - "Just pass `True` as the last optional parameter, as below." + "This interface is a bit inconveniant to use interactively, due to the fact that we need a `spot.bdd_dict` object to print a BDD." ] }, { "cell_type": "code", "collapsed": false, "input": [ - "spot.highlight_stutter_invariant_states(aut, h, 5, True)\n", - "display(aut)" + "sil_vec = spot.stutter_invariant_letters(pos, f)\n", + "for q in range(pos.num_states()):\n", + " print(\"sil_vec[{}] =\".format(q), spot.bdd_format_formula(pos.get_dict(), sil_vec[q]))" ], "language": "python", "metadata": {}, "outputs": [ { - "metadata": {}, - "output_type": "display_data", - "svg": [ - "\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "[B\u00fcchi]\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "I->0\n", - "\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "2->3\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "1\n", - "\u24ff\n", - "\n", - "\n", - "\n" - ], + "output_type": "stream", + "stream": "stdout", "text": [ - " *' at 0x7f1c8045a690> >" + "sil_vec[0] = 1\n", + "sil_vec[1] = 1\n", + "sil_vec[2] = 1\n", + "sil_vec[3] = b\n" ] } ], "prompt_number": 23 - }, - { - "cell_type": "markdown", - "metadata": {}, - "source": [ - "Note that an SCC can contain a mix of locally stutter-invariant and local stutter-sensitive states. Here is the deterministic version of the above automaton for example." - ] - }, - { - "cell_type": "code", - "collapsed": false, - "input": [ - "aut = spot.translate(h, 'deterministic')\n", - "spot.highlight_stutter_invariant_states(aut, h, 5, True)\n", - "display(aut.show('.abs'))" - ], - "language": "python", - "metadata": {}, - "outputs": [ - { - "metadata": {}, - "output_type": "display_data", - "svg": [ - "\n", - "\n", - "G\n", - "\n", - "Inf(\n", - "\u24ff\n", - ")\n", - "[B\u00fcchi]\n", - "cluster_0\n", - "\n", - "\n", - "cluster_1\n", - "\n", - "\n", - "\n", - "\n", - "3\n", - "\n", - "3\n", - "\n", - "\n", - "I->3\n", - "\n", - "\n", - "\n", - "\n", - "3->3\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "4\n", - "\n", - "4\n", - "\n", - "\n", - "3->4\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "5\n", - "\n", - "5\n", - "\u24ff\n", - "\n", - "\n", - "5->5\n", - "\n", - "\n", - "1\n", - "\n", - "\n", - "4->4\n", - "\n", - "\n", - "a\n", - "\n", - "\n", - "0\n", - "\n", - "0\n", - "\n", - "\n", - "4->0\n", - "\n", - "\n", - "!a\n", - "\n", - "\n", - "0->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "0->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "1\n", - "\n", - "1\n", - "\n", - "\n", - "0->1\n", - "\n", - "\n", - "!a & b\n", - "\n", - "\n", - "2\n", - "\n", - "2\n", - "\n", - "\n", - "0->2\n", - "\n", - "\n", - "a & b\n", - "\n", - "\n", - "1->3\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "1->5\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "1->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "2->5\n", - "\n", - "\n", - "b\n", - "\n", - "\n", - "2->4\n", - "\n", - "\n", - "a & !b\n", - "\n", - "\n", - "2->0\n", - "\n", - "\n", - "!a & !b\n", - "\n", - "\n", - "" - ], - "text": [ - "" - ] - } - ], - "prompt_number": 24 } ], "metadata": {}