diff --git a/NEWS b/NEWS index e5dac4e3f..c7aba77a9 100644 --- a/NEWS +++ b/NEWS @@ -58,6 +58,11 @@ New in spot 2.6.0.dev (not yet released) set. (This combinations of options is not available from command-line tools.) + - The spot::contains(a, b) function introduced in 2.6 was testing + a⊆b instead of a⊇b as one would expect. Infortunately the + documentation was also matching the code, so this is a backward + incompatible change. + New in spot 2.6 (2018-07-04) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 018086289..71ba08ffc 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1411,7 +1411,7 @@ namespace matched &= !aut->intersects(opt->included_in); if (opt->equivalent_pos) matched &= !aut->intersects(opt->equivalent_neg) - && spot::contains(opt->equivalent_pos, aut); + && spot::contains(aut, opt->equivalent_pos); if (matched && !opt->acc_words.empty()) for (auto& word_aut: opt->acc_words) diff --git a/python/spot/__init__.py b/python/spot/__init__.py index b01c21cc8..4980cad3e 100644 --- a/python/spot/__init__.py +++ b/python/spot/__init__.py @@ -1047,7 +1047,7 @@ def bdd_to_formula(b, dic=_bdd_dict): def language_containment_checker(dic=_bdd_dict): from spot.impl import language_containment_checker as c - c.contains = c.contained + c.contains = lambda this, a, b: c.contained(this, b, a) c.are_equivalent = c.equal return c(dic) diff --git a/spot/twaalgos/contains.cc b/spot/twaalgos/contains.cc index 957aa41b5..a94b3ac40 100644 --- a/spot/twaalgos/contains.cc +++ b/spot/twaalgos/contains.cc @@ -49,25 +49,25 @@ namespace spot bool contains(const_twa_graph_ptr left, const_twa_graph_ptr right) { - return !left->intersects(dualize(ensure_deterministic(right))); + return !right->intersects(dualize(ensure_deterministic(left))); } bool contains(const_twa_graph_ptr left, formula right) { - return !left->intersects(translate(formula::Not(right), left->get_dict())); + auto right_aut = translate(right, left->get_dict()); + return !right_aut->intersects(dualize(ensure_deterministic(left))); } bool contains(formula left, const_twa_graph_ptr right) { - auto left_aut = translate(left, right->get_dict()); - return !left_aut->intersects(dualize(ensure_deterministic(right))); + return !right->intersects(translate(formula::Not(left), right->get_dict())); } bool contains(formula left, formula right) { auto dict = make_bdd_dict(); - auto left_aut = translate(left, dict); - return !left_aut->intersects(translate(formula::Not(right), dict)); + auto right_aut = translate(right, dict); + return !right_aut->intersects(translate(formula::Not(left), dict)); } bool are_equivalent(const_twa_graph_ptr left, const_twa_graph_ptr right) diff --git a/spot/twaalgos/contains.hh b/spot/twaalgos/contains.hh index 758339c73..61c53076a 100644 --- a/spot/twaalgos/contains.hh +++ b/spot/twaalgos/contains.hh @@ -28,14 +28,14 @@ namespace spot { /// \ingroup containment - /// \brief Test if the language of \a left is included in that of \a right. + /// \brief Test if the language of \a right is included in that of \a left. /// /// Both arguments can be either formulas or automata. Formulas /// will be converted into automata. /// /// The inclusion check if performed by ensuring that the automaton - /// associated to \a left does not intersect the automaton - /// associated to the complement of \a right. It helps if \a right + /// associated to \a right does not intersect the automaton + /// associated to the complement of \a left. It helps if \a left /// is a deterministic automaton or a formula (because in both cases /// complementation is easier). /// @{ diff --git a/tests/python/contains.ipynb b/tests/python/contains.ipynb index 5e15a0ba1..0e0022b0f 100644 --- a/tests/python/contains.ipynb +++ b/tests/python/contains.ipynb @@ -17,7 +17,7 @@ "source": [ "# Containement checks\n", "\n", - "The `spot.contains()` function checks whether the language of its left argument is included in the language of its right argument. The arguments may mix automata and formulas; the latter can be given as strings." + "The `spot.contains()` function checks whether the language of its right argument is included in the language of its left argument. The arguments may mix automata and formulas; the latter can be given as strings." ] }, { @@ -38,7 +38,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 3, @@ -58,7 +58,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 4, @@ -78,7 +78,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 5, @@ -98,7 +98,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 6, @@ -118,7 +118,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 7, @@ -145,7 +145,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 8, @@ -165,7 +165,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 9, @@ -272,7 +272,7 @@ { "data": { "text/plain": [ - "(False, True)" + "(True, False)" ] }, "execution_count": 14, @@ -344,7 +344,7 @@ }, { "cell_type": "code", - "execution_count": 34, + "execution_count": 17, "metadata": {}, "outputs": [], "source": [ @@ -360,7 +360,7 @@ }, { "cell_type": "code", - "execution_count": 35, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -484,34 +484,6 @@ "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": {