diff --git a/spot/twaalgos/mealy_machine.cc b/spot/twaalgos/mealy_machine.cc index aa7821213..99b762f16 100644 --- a/spot/twaalgos/mealy_machine.cc +++ b/spot/twaalgos/mealy_machine.cc @@ -2951,6 +2951,19 @@ namespace decltype(iaj_eq)>& used_ziaj_map) { const unsigned n_env_states = minmach->num_states(); + // Looping over unordered is different on arm vs intel + // todo better way to do this? + // We could move it I guess, but the elements are fairly cheap to copy + auto used_ziaj_ordered = std::vector>(); + used_ziaj_ordered.reserve(used_ziaj_map.size()); + + for (const auto& e : used_ziaj_map) + used_ziaj_ordered.push_back(e); + + std::sort(used_ziaj_ordered.begin(), used_ziaj_ordered.end(), + [](const auto& pl, const auto& pr) + {return pl.first < pr.first; }); + // For each minimal letter, create the (input) condition that it represents // This has to be created for each minimal letters // and might be shared between alphabets @@ -2958,7 +2971,7 @@ namespace = comp_represented_cond(red); #ifdef TRACE - for (const auto& el : used_ziaj_map) + for (const auto& el : used_ziaj_ordered) { const unsigned group = x_in_class[el.first.i].first; const bdd& incond = gmm2cond[group][el.first.a]; @@ -3014,7 +3027,7 @@ namespace minmach->edge_storage(it->second).cond |= incond; }; - for (const auto& [iaj, outcond] : used_ziaj_map) + for (const auto& [iaj, outcond] : used_ziaj_ordered) { // The group determines the incond const unsigned group = x_in_class[iaj.i].first; @@ -3232,8 +3245,10 @@ namespace incomp_cubes_list.end(), incomp_cubes_list.begin(), [&](auto& el) -> std::pair - {return {repl1(el.first), - repl2(el.second)}; }); + { + auto r1 = repl1(el.first); + auto r2 = repl2(el.second); + return {r1, r2}; }); }; std::vector> incomp_cubes_list; diff --git a/tests/python/_synthesis.ipynb b/tests/python/_synthesis.ipynb index ee7cd9c1f..1ed59760d 100644 --- a/tests/python/_synthesis.ipynb +++ b/tests/python/_synthesis.ipynb @@ -275,17 +275,17 @@ "spot-state-player: 0 0 1 1 1 1\n", "--BODY--\n", "State: 0\n", - "[0] 3\n", - "[!0] 4\n", - "State: 1\n", "[0] 2\n", + "[!0] 3\n", + "State: 1\n", + "[0] 4\n", "[!0] 5\n", "State: 2\n", - "[2] 1\n", - "State: 3\n", "[!2] 1\n", - "State: 4\n", + "State: 3\n", "[!2] 0\n", + "State: 4\n", + "[2] 1\n", "State: 5\n", "[2] 0\n", "--END--\n", @@ -314,17 +314,17 @@ "spot-state-player: 0 0 1 1 1 1\n", "--BODY--\n", "State: 0\n", - "[0] 3\n", - "[!0] 4\n", - "State: 1\n", "[0] 2\n", + "[!0] 3\n", + "State: 1\n", + "[0] 4\n", "[!0] 5\n", "State: 2\n", - "[2] 1\n", - "State: 3\n", "[!2] 1\n", - "State: 4\n", + "State: 3\n", "[!2] 0\n", + "State: 4\n", + "[2] 1\n", "State: 5\n", "[2] 0\n", "--END--\n"