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

to_parity: Correct order function

Browse source 
* spot/twaalgos/toparity.cc: Use a strict
comparison in group_to_vector.
* spot/twa/acc.cc: Use a strict comparison
in is_parity_max_equiv.
This commit is contained in:
Florian Renkin 2020-04-15 15:25:53 +02:00 • committed by Alexandre Duret-Lutz
parent 533640fa74
commit ee3e09f8c9
2 changed files with 19 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

8
spot/twa/acc.cc
View file

@ -1358,8 +1358,8 @@ namespace spot
std::sort(disj.begin(), disj.end(), std::sort(disj.begin(), disj.end(),
[](acc_code c1, acc_code c2) [](acc_code c1, acc_code c2)
{ {
(void) c2; return (c1 != c2) &&
return c1.back().sub.op == acc_cond::acc_op::Inf; c1.back().sub.op == acc_cond::acc_op::Inf;
}); });
unsigned i = 0; unsigned i = 0;
for (; i < disj.size() - 1; ++i) for (; i < disj.size() - 1; ++i)
@ -1395,8 +1395,8 @@ namespace spot
{ std::sort(conj.begin(), conj.end(), { std::sort(conj.begin(), conj.end(),
[](acc_code c1, acc_code c2) [](acc_code c1, acc_code c2)
{ {
(void) c2; return (c1 != c2)
return c1.back().sub.op == acc_cond::acc_op::Fin; && c1.back().sub.op == acc_cond::acc_op::Fin;
}); });
unsigned i = 0; unsigned i = 0;
for (; i < conj.size() - 1; i++) for (; i < conj.size() - 1; i++)

12
spot/twaalgos/toparity.cc
View file

@ -689,13 +689,20 @@ get_inputs_iar(const twa_graph_ptr& aut, algorithm algo,
std::vector<unsigned> std::vector<unsigned>
group_to_vector(const std::set<acc_cond::mark_t>& group) group_to_vector(const std::set<acc_cond::mark_t>& 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<acc_cond::mark_t> group_vect(group.begin(), group.end()); std::vector<acc_cond::mark_t> 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(), std::sort(group_vect.begin(), group_vect.end(),
[](const acc_cond::mark_t left, const acc_cond::mark_t right) [](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<unsigned> result; std::vector<unsigned> result;
for (auto mark : group_vect) for (auto mark : group_vect)
{ {
@ -717,7 +724,8 @@ group_to_vector_iar(const std::set<std::vector<unsigned>>& group)
[](const std::vector<unsigned> left, [](const std::vector<unsigned> left,
const std::vector<unsigned> right) const std::vector<unsigned> right)
{ {
return std::includes(right.begin(), right.end(), return (right != left)
&& std::includes(right.begin(), right.end(),
left.begin(), left.end()); left.begin(), left.end());
}); });
std::vector<unsigned> result; std::vector<unsigned> result;