diff --git a/doc/org/autfilt.org b/doc/org/autfilt.org index 5a2e8438d..22d0eec0b 100644 --- a/doc/org/autfilt.org +++ b/doc/org/autfilt.org @@ -335,11 +335,11 @@ $txt #+RESULTS: [[file:autfilt-ex1.png]] -Using =--sba= will "push" the acceptance membership of the transitions to the states: +Using =--sbacc= will "push" the acceptance membership of the transitions to the states: #+NAME: autfilt-ex2 #+BEGIN_SRC sh :results verbatim :export code -autfilt --sba aut-ex1.hoa --dot=.a +autfilt --sbacc aut-ex1.hoa --dot=.a #+END_SRC #+RESULTS: autfilt-ex2 @@ -430,15 +430,9 @@ digraph G { 2 -> 0 [label=] 2 -> 1 [label=⓿>] 2 -> 2 [label=⓿>] - 2 -> 3 [label=] - 2 -> 4 [label=⓿>] - 2 -> 5 [label=⓿>] + 2 -> 3 [label=⓿>] 3 [label="3"] - 4 [label="4"] - 5 [label="5"] - 5 -> 3 [label=❶❹>] - 5 -> 4 [label=⓿❶❹>] - 5 -> 5 [label=⓿❶❹>] + 3 -> 3 [label=⓿❶❹>] } #+end_example diff --git a/src/tgba/tgbagraph.cc b/src/tgba/tgbagraph.cc index ac6535089..8c5900a14 100644 --- a/src/tgba/tgbagraph.cc +++ b/src/tgba/tgbagraph.cc @@ -178,52 +178,74 @@ namespace spot unsigned num_states = g_.num_states(); if (num_states == 0) return; - std::vector info(num_states, 0); - // In this loop, info[s] means that the state is useless. - bool untouched; + + std::vector useful(num_states, 0); + + // Make a DFS to compute a topological order. + std::vector order; + order.reserve(num_states); + std::vector> todo; // state, trans + useful[init_number_] = 1; + todo.emplace_back(init_number_, g_.state_storage(init_number_).succ); do { - untouched = true; - for (unsigned s = 0; s < num_states; ++s) + unsigned src; + unsigned tid; + std::tie(src, tid) = todo.back(); + if (tid == 0U) { - if (info[s]) - continue; - bool useless = true; - auto t = g_.out_iteraser(s); - while (t) - { - // Erase any transition to a unused state. - if (info[t->dst]) - { - t.erase(); - continue; - } - // if we have a transition, to a used state, - // then the state is useful. - useless = false; - ++t; - } - if (useless) - { - info[s] = true; - untouched = false; - } + todo.pop_back(); + order.push_back(src); + continue; + } + auto& t = g_.trans_storage(tid); + todo.back().second = t.next_succ; + unsigned dst = t.dst; + if (useful[dst] != 1) + { + todo.emplace_back(dst, g_.state_storage(dst).succ); + useful[dst] = 1; } } - while (!untouched); + while (!todo.empty()); + + // Process states in topological order + for (auto s: order) + { + auto t = g_.out_iteraser(s); + bool useless = true; + while (t) + { + // Erase any transition to a useless state. + if (!useful[t->dst]) + { + t.erase(); + continue; + } + // if we have a transition to a useful state, then the + // state is useful. + useless = false; + ++t; + } + if (useless) + useful[s] = 0; + } + + // Make sure the initial state is useful (even if it has been + // marked as useless by the previous loop because it has no + // successor). + useful[init_number_] = 1; - // Assume that the initial state is useful. - info[init_number_] = false; // Now renumber each used state. unsigned current = 0; - for (auto& v: info) - if (v) - v = -1U; + for (unsigned s = 0; s < num_states; ++s) + if (useful[s]) + useful[s] = current++; else - v = current++; - if (current == info.size()) + useful[s] = -1U; + if (current == num_states) return; // No useless state. - init_number_ = info[init_number_]; - g_.defrag_states(std::move(info), current); + init_number_ = useful[init_number_]; + g_.defrag_states(std::move(useful), current); } } diff --git a/src/tgbaalgos/remfin.cc b/src/tgbaalgos/remfin.cc index 63edcd59e..7619f16fa 100644 --- a/src/tgbaalgos/remfin.cc +++ b/src/tgbaalgos/remfin.cc @@ -331,7 +331,7 @@ namespace spot } - res->purge_unreachable_states(); + res->purge_dead_states(); trace << "before cleanup: " << res->get_acceptance() << '\n'; cleanup_acceptance(res); trace << "after cleanup: " << res->get_acceptance() << '\n'; diff --git a/src/tgbatest/det.test b/src/tgbatest/det.test index 5d98c5b9d..336e549f0 100755 --- a/src/tgbatest/det.test +++ b/src/tgbatest/det.test @@ -80,15 +80,14 @@ State: 2 --END-- EOF -# FIXME: we should improve this output cat >ex.hoa <<'EOF' HOA: v1 -States: 7 +States: 5 Start: 0 AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) -properties: trans-labels explicit-labels state-acc +properties: trans-labels explicit-labels state-acc inherently-weak --BODY-- State: 0 [!0] 0 @@ -102,16 +101,12 @@ State: 2 [!0] 0 [0] 2 [!0] 3 -[0] 5 +[0] 4 State: 3 {0} [!0] 3 State: 4 {0} [!0] 3 -State: 5 {0} -[!0] 3 -[0] 5 -State: 6 {0} -[t] 6 +[0] 4 --END-- EOF @@ -119,8 +114,6 @@ run 0 ../ltl2tgba -H -DC -XH in.hoa > out.hoa run 1 ../../bin/autfilt -q --are-isomorph in.hoa out.hoa run 0 ../../bin/autfilt -q --are-isomorph ex.hoa out.hoa -# FIXME: State 2 and 5 are unreachable and I'd rather -# not show them. run 0 ../ltl2tgba -x -DC 'GFa & XGFb' > out.tgba cat >ex.tgba < 1 [label="1"] 1 [label="1"] 1 -> 1 [label="1"] - 1 -> 3 [label="!a"] - 1 -> 4 [label="!b"] + 1 -> 2 [label="!a"] + 1 -> 3 [label="!b"] 2 [label="2", peripheries=2] - 2 -> 3 [label="!a"] + 2 -> 2 [label="!a"] 3 [label="3", peripheries=2] - 3 -> 3 [label="!a"] - 4 [label="4", peripheries=2] - 4 -> 4 [label="!b"] - 5 [label="5", peripheries=2] - 5 -> 5 [label="1"] + 3 -> 3 [label="!b"] } EOF diff out.tgba ex.tgba diff --git a/src/tgbatest/remfin.test b/src/tgbatest/remfin.test index 12aa8bb38..0c6d68a02 100755 --- a/src/tgbatest/remfin.test +++ b/src/tgbatest/remfin.test @@ -186,7 +186,7 @@ State: 2 {0} [0&!1] 2 --END-- HOA: v1 -States: 6 +States: 4 Start: 0 AP: 2 "a" "b" Acceptance: 4 Inf(0) | Inf(3) | (Inf(1)&Inf(2)) @@ -204,18 +204,12 @@ State: 2 [!1] 0 [0&!1] 1 [!0&!1] 2 -[!1] 3 -[0&!1] 4 -[!0&!1] 5 +[!0&!1] 3 State: 3 -State: 4 -State: 5 -[!1] 3 -[0&!1] 4 {0} -[!0&!1] 5 {0} +[!0&!1] 3 {0} --END-- HOA: v1 -States: 6 +States: 4 Start: 0 AP: 2 "a" "b" Acceptance: 5 (Inf(0)&Inf(1)&Inf(4)) | Inf(0) | (Inf(2)&Inf(3)) @@ -233,15 +227,9 @@ State: 2 [!1] 0 [0&!1] 1 {0} [!0&!1] 2 {0} -[!1] 3 -[0&!1] 4 {0} -[!0&!1] 5 {0} +[!0&!1] 3 {0} State: 3 -State: 4 -State: 5 -[!1] 3 {1 4} -[0&!1] 4 {0 1 4} -[!0&!1] 5 {0 1 4} +[!0&!1] 3 {0 1 4} --END-- HOA: v1 States: 1 @@ -281,7 +269,7 @@ State: 1 {0} [0] 1 --END-- HOA: v1 -States: 12 +States: 10 Start: 2 AP: 1 "p1" Acceptance: 2 Inf(1) | Inf(0) @@ -290,8 +278,8 @@ properties: trans-labels explicit-labels state-acc State: 0 [!0] 6 [0] 0 +[0] 8 [0] 9 -[0] 11 State: 1 {0 1} [!0] 3 [0] 3 @@ -314,13 +302,9 @@ State: 7 {1} [!0] 6 [0] 4 State: 8 -State: 9 -[!0] 8 +[0] 8 +State: 9 {1} [0] 9 -State: 10 -State: 11 {1} -[!0] 10 -[0] 11 --END-- EOF