alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

contains: fix the semantics

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2018-08-01 17:17:25 +02:00
parent 4ce0d92896
commit 23722c031f
6 changed files with 27 additions and 50 deletions
Download patch file Download diff file Expand all files Collapse all files

12
spot/twaalgos/contains.cc
View file

@ -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)

6
spot/twaalgos/contains.hh
View file

@ -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).
/// @{