diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 80e581a50..1c4dcbacb 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1357,10 +1357,10 @@ namespace spot { std::sort(disj.begin(), disj.end(), [](acc_code c1, acc_code c2) - { - (void) c2; - return c1.back().sub.op == acc_cond::acc_op::Inf; - }); + { + return (c1 != c2) && + c1.back().sub.op == acc_cond::acc_op::Inf; + }); unsigned i = 0; for (; i < disj.size() - 1; ++i) { @@ -1394,10 +1394,10 @@ namespace spot else { std::sort(conj.begin(), conj.end(), [](acc_code c1, acc_code c2) - { - (void) c2; - return c1.back().sub.op == acc_cond::acc_op::Fin; - }); + { + return (c1 != c2) + && c1.back().sub.op == acc_cond::acc_op::Fin; + }); unsigned i = 0; for (; i < conj.size() - 1; i++) { diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index bb4db11aa..8854e6887 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -689,13 +689,20 @@ get_inputs_iar(const twa_graph_ptr& aut, algorithm algo, std::vector group_to_vector(const std::set& group) { + // In this function, we have for example the marks {1, 2}, {1, 2, 3}, {2} + // A compatible order is [2, 1, 3] std::vector group_vect(group.begin(), group.end()); + // We sort the elements by inclusion. This function is called on a + // set of marks such that each mark is included or includes the others. std::sort(group_vect.begin(), group_vect.end(), [](const acc_cond::mark_t left, const acc_cond::mark_t right) { - return (left & right) == left; + return (left != right) && ((left & right) == left); }); + // At this moment, we have the vector [{2}, {1, 2}, {1, 2, 3}]. + // In order to create the order, we add the elements of the first element. + // Then we add the elements of the second mark (without duplication), etc. std::vector result; for (auto mark : group_vect) { @@ -717,8 +724,9 @@ group_to_vector_iar(const std::set>& group) [](const std::vector left, const std::vector right) { - return std::includes(right.begin(), right.end(), - left.begin(), left.end()); + return (right != left) + && std::includes(right.begin(), right.end(), + left.begin(), left.end()); }); std::vector result; for (auto vec : group_vect)