diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index b4ab6987b..f612e4ca1 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -19,10 +19,11 @@ #include "config.h" #include +#include #include #include - +#include #include namespace spot @@ -88,15 +89,14 @@ namespace spot return it.first->second; }; + std::vector initial_perm(aut_->num_sets()); + std::iota(initial_perm.begin(), initial_perm.end(), 0); { - std::vector p0; - for (unsigned k : aut_->acc().all_sets().sets()) - p0.push_back(k); - lar_state s0{aut_->get_init_state_number(), p0}; - unsigned init = get_state(s0); // put s0 in todo - res_->set_init_state(init); + lar_state s0{aut_->get_init_state_number(), initial_perm}; + res_->set_init_state(get_state(s0)); } + scc_info si(aut_, scc_info_options::NONE); // main loop while (!todo.empty()) { @@ -106,6 +106,7 @@ namespace spot // TODO todo could store this number to avoid one lookup unsigned src_num = get_state(current); + unsigned source_scc = si.scc_of(current.state); for (const auto& e : aut_->out(current.state)) { // find the new permutation @@ -118,6 +119,12 @@ namespace spot std::rotate(it, it+1, new_perm.end()); } + if (source_scc != si.scc_of(e.dst)) + { + new_perm = initial_perm; + h = 0; + } + lar_state dst{e.dst, new_perm}; unsigned dst_num = get_state(dst); diff --git a/tests/python/toparity.py b/tests/python/toparity.py index e714a72d7..b0bffbe23 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -35,6 +35,18 @@ State: 0 p = spot.to_parity(a) assert spot.are_equivalent(a, p) +a = spot.automaton(""" +HOA: v1 States: 6 Start: 0 AP: 2 "p0" "p1" Acceptance: 6 Inf(5) | +Fin(2) | Inf(1) | (Inf(0) & Fin(3)) | Inf(4) properties: trans-labels +explicit-labels trans-acc --BODY-- State: 0 [0&1] 2 {4 5} [0&1] 4 {0 4} +[!0&!1] 3 {3 5} State: 1 [0&!1] 3 {1 5} [!0&!1] 5 {0 1} State: 2 [!0&!1] +0 {0 3} [0&!1] 1 {0} State: 3 [!0&1] 4 {1 2 3} [0&1] 3 {3 4 5} State: +4 [!0&!1] 1 {2 4} State: 5 [!0&1] 4 --END-- +""") +p = spot.to_parity(a) +assert p.num_states() == 22 +assert spot.are_equivalent(a, p) + for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") p = spot.to_parity(d)