Commit 701a3b1c authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

contains: fix the semantics

spot::contains(a, b) should test a⊇b.  It was testing a⊆b instead.

* NEWS: Mention the bug.
* spot/twaalgos/contains.cc, spot/twaalgos/contains.hh: Fix the
code and documentation.
* tests/python/contains.ipynb: Adjust description and expected
results.
* python/spot/__init__.py: Also swap the argument of
language_containment_checker.contains()
* bin/autfilt.cc: Adjust usage.
parent 126d3923
Pipeline #3187 passed with stage
in 54 minutes and 43 seconds
......@@ -16,6 +16,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)
......
......@@ -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)
......
......@@ -1039,7 +1039,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)
......
......@@ -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)
......
......@@ -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).
/// @{
......
......@@ -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<ipython-input-36-d7d1b4bd9ffe>\u001b[0m in \u001b[0;36m<module>\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": {
......
%% Cell type:code id: tags:
``` python
import spot
from spot.jupyter import display_inline
spot.setup(show_default='.a')
```
%% Cell type:markdown id: tags:
# Containement checks
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.
%% Cell type:code id: tags:
``` python
f = spot.formula('GFa'); aut_f = f.translate()
g = spot.formula('FGa'); aut_g = g.translate()
```
%% Cell type:code id: tags:
``` python
spot.contains(f, g), spot.contains(g, f)
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains(aut_f, aut_g), spot.contains(aut_g, aut_f)
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains(aut_f, g), spot.contains(aut_g, f)
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains(f, aut_g), spot.contains(g, aut_f)
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:code id: tags:
``` python
spot.contains("GFa", aut_g), spot.contains("FGa", aut_f)
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:markdown id: tags:
Those functions are also usable as methods:
%% Cell type:code id: tags:
``` python
f.contains(aut_g), g.contains(aut_f)
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:code id: tags:
``` python
aut_f.contains("FGa"), aut_g.contains("GFa")
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:markdown id: tags:
# Equivalence checks
The `spot.are_equivalent()` tests the equivalence of the languages of its two arguments. Note that the corresponding method is called `equivalent_to()`.
%% Cell type:code id: tags:
``` python
spot.are_equivalent(f, g), spot.are_equivalent(aut_f, aut_g)
```
%%%% Output: execute_result
(False, False)
%% Cell type:code id: tags:
``` python
f.equivalent_to(aut_g), aut_f.equivalent_to(g)
```
%%%% Output: execute_result
(False, False)
%% Cell type:code id: tags:
``` python
aut_f.equivalent_to('XXXGFa')
```
%%%% Output: execute_result
True
%% Cell type:markdown id: tags:
# Containement checks between formulas with cache
In the case of containement checks between formulas, `language_containement_checker` instances provide similar services, but they cache automata representing the formulas checked. This should be prefered when performing several containement checks using the same formulas.
%% Cell type:code id: tags:
``` python
lcc = spot.language_containment_checker()
```
%% Cell type:code id: tags:
``` python
lcc.contains(f, g), lcc.contains(g, f)
```
%%%% Output: execute_result
(False, True)
(True, False)
%% Cell type:code id: tags:
``` python
lcc.are_equivalent(f, g)
```
%%%% Output: execute_result
False
%% Cell type:markdown id: tags:
# Help for distinguishing languages
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.
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 id: tags:
``` python
aut_f.exclusive_word(aut_g)
```
%%%% Output: execute_result
cycle{a; !a}
%% Cell type:markdown id: tags:
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 id: tags:
``` python
def show_one_difference(left, right):
run = left.exclusive_run(right)
if not run:
print("The two automata are equivalent.")
else:
print("The following word is only accepted by one automaton:", spot.make_twa_word(run))
run.highlight(5)
display_inline(left, right)
```
%% Cell type:code id: tags:
``` python
show_one_difference(aut_f, aut_g)
```
%%%% Output: stream
The following word is only accepted by one automaton: cycle{!a; a; !a}
%%%% Output: display_data
%% Cell type:code id: tags:
``` python
run.get_aut()
```
%%%% Output: error
---------------------------------------------------------------------------
NameError Traceback (most recent call last)
<ipython-input-36-d7d1b4bd9ffe> in <module>()
----> 1 run.get_aut()
NameError: name 'run' is not defined
%% Cell type:code id: tags:
``` python
```
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment