diff --git a/NEWS b/NEWS index 09a68eb6e..b06ef4ab2 100644 --- a/NEWS +++ b/NEWS @@ -192,7 +192,14 @@ New in spot 2.5.3.dev (not yet released) - spot::contains() and spot::are_equivalent() can be used to check language containement between two automata or formulas. They are most welcome in Python, since we used to redefine - them every now and them. + them every now and them. Some examples are shown in + https://spot.lrde.epita.fr/ipynb/contains.html + + - aut1->exclusive_word(aut2) is a new method that returns a word + accepted by aut1 or aut2 but not both. The exclusive_run() + variant will return. This is useful when comparing automata and + looking for differences. See also + https://spot.lrde.epita.fr/ipynb/contains.html - spot::remove_alternation() was slightly improved on very-weak alternating automata: the labeling of the outgoing transitions in diff --git a/spot/twa/twa.cc b/spot/twa/twa.cc index 19fd494a0..7633a8b0f 100644 --- a/spot/twa/twa.cc +++ b/spot/twa/twa.cc @@ -28,6 +28,9 @@ #include #include #include +#include +#include +#include #include namespace spot @@ -117,7 +120,7 @@ namespace spot twa::intersecting_run(const_twa_ptr other, bool from_other) const { auto a = shared_from_this(); - if (from_other) + if (!from_other) other = remove_fin_maybe(other); else a = remove_fin_maybe(a); @@ -135,6 +138,57 @@ namespace spot return otf_product(a1, a2)->accepting_word(); } + namespace + { + static const_twa_graph_ptr + ensure_deterministic(const const_twa_ptr& aut_in) + { + const_twa_graph_ptr aut = + std::dynamic_pointer_cast(aut_in); + if (!aut) + aut = make_twa_graph(aut_in, twa::prop_set::all()); + + if (is_deterministic(aut)) + return aut; + postprocessor p; + p.set_type(postprocessor::Generic); + p.set_pref(postprocessor::Deterministic); + p.set_level(postprocessor::Low); + return p.run(std::const_pointer_cast(aut)); + } + } + twa_run_ptr + twa::exclusive_run(const_twa_ptr other) const + { + const_twa_ptr a = shared_from_this(); + const_twa_ptr b = other; + + // We have to find a run in A\B or in B\A. When possible, let's + // make sure the first automaton we complement is deterministic. + if (auto aa = std::dynamic_pointer_cast(a)) + if (is_deterministic(aa)) + std::swap(a, b); + if (auto run = a->intersecting_run(dualize(ensure_deterministic(b)))) + return run; + return b->intersecting_run(dualize(ensure_deterministic(a))); + } + + twa_word_ptr + twa::exclusive_word(const_twa_ptr other) const + { + const_twa_ptr a = shared_from_this(); + const_twa_ptr b = other; + + // We have to find a word in A\B or in B\A. When possible, let's + // make sure the first automaton we complement is deterministic. + if (auto aa = std::dynamic_pointer_cast(a)) + if (is_deterministic(aa)) + std::swap(a, b); + if (auto word = a->intersecting_word(dualize(ensure_deterministic(b)))) + return word; + return b->intersecting_word(dualize(ensure_deterministic(a))); + } + void twa::set_named_prop(std::string s, std::nullptr_t) { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 1b2468601..6b29bc142 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -888,6 +888,30 @@ namespace spot /// Return nullptr if no accepting word were found. virtual twa_word_ptr intersecting_word(const_twa_ptr other) const; + /// \brief Return an accepting run recognizing a word accepted by + /// exactly one of the two automata. + /// + /// If \a from_other is true, the returned run will be over the + /// \a other automaton. Otherwise, the run will be over this + /// automaton. + /// + /// Note that this method currently only works if the automaton + /// from which the accepting run is extracted uses Fin-less acceptance. + /// (The other automaton can have any acceptance condition.) + /// + /// Return nullptr iff the two automata recognize the same + /// language. + virtual twa_run_ptr exclusive_run(const_twa_ptr other) const; + + /// \brief Return a word accepted by exactly one of the two + /// automata. + /// + /// Note that this method DOES works with Fin acceptance. + /// + /// Return nullptr iff the two automata recognize the same + /// language. + virtual twa_word_ptr exclusive_word(const_twa_ptr other) const; + private: acc_cond acc_; diff --git a/tests/python/contains.ipynb b/tests/python/contains.ipynb index bddf18b50..5e15a0ba1 100644 --- a/tests/python/contains.ipynb +++ b/tests/python/contains.ipynb @@ -7,6 +7,7 @@ "outputs": [], "source": [ "import spot\n", + "from spot.jupyter import display_inline\n", "spot.setup(show_default='.a')" ] }, @@ -302,6 +303,215 @@ "source": [ "lcc.are_equivalent(f, g)" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "# Help for distinguishing languages\n", + "\n", + "Assume you have computed two automata, that `are_equivalent(a1, a2)` returns `False`, and you want to know why. (This often occur when debugging some algorithm that produce an automaton that is not equivalent to which it should.) The automaton class has a method called `a1.exclusive_run(a2)` that can help with this task: it returns a run that recognizes a word is is accepted by one of the two automata but not by both. The method `a1.exclusive_run(a2)` will return just a word.\n", + "\n", + "For instance let's find a word that is exclusive between `aut_f` and `aut_g`. (The adjective *exlusive* is a reference to the *exclusive or* operator: the word belongs to L(aut_f) \"xor\" it belongs to L(aut_g).)" + ] + }, + { + "cell_type": "code", + "execution_count": 16, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "cycle{a; !a}" + ] + }, + "execution_count": 16, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "aut_f.exclusive_word(aut_g)" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "We can even write a small function that highlights one difference between two automata. Note that the `run` returned will belong to either `left` or `right`, so calling the `highlight()` method will colorize one of those two automata." + ] + }, + { + "cell_type": "code", + "execution_count": 34, + "metadata": {}, + "outputs": [], + "source": [ + "def show_one_difference(left, right):\n", + " run = left.exclusive_run(right)\n", + " if not run:\n", + " print(\"The two automata are equivalent.\")\n", + " else:\n", + " print(\"The following word is only accepted by one automaton:\", spot.make_twa_word(run))\n", + " run.highlight(5)\n", + " display_inline(left, right)" + ] + }, + { + "cell_type": "code", + "execution_count": 35, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "The following word is only accepted by one automaton: cycle{!a; a; !a}\n" + ] + }, + { + "data": { + "text/html": [ + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "!a\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "a\n", + "⓿\n", + "\n", + "\n", + "\n", + "
\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "[Büchi]\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "I->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0->0\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "0->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "a\n", + "\n", + "\n", + "\n", + "
" + ], + "text/plain": [ + "" + ] + }, + "metadata": {}, + "output_type": "display_data" + } + ], + "source": [ + "show_one_difference(aut_f, aut_g)" + ] + }, + { + "cell_type": "code", + "execution_count": 36, + "metadata": {}, + "outputs": [ + { + "ename": "NameError", + "evalue": "name 'run' is not defined", + "output_type": "error", + "traceback": [ + "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m", + "\u001b[0;31mNameError\u001b[0m Traceback (most recent call last)", + "\u001b[0;32m\u001b[0m in \u001b[0;36m\u001b[0;34m()\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mrun\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mget_aut\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m", + "\u001b[0;31mNameError\u001b[0m: name 'run' is not defined" + ] + } + ], + "source": [ + "run.get_aut()" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -320,7 +530,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.6.5" + "version": "3.6.6" } }, "nbformat": 4,