Commit 020bbd44 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

remove_fin: remove useless states

* src/tgba/tgbagraph.cc (purge_dead_states): Using a DFS to compute a
topological order, allowing to remove useless using a second
pass (instead of iterating the passes until there is nothing to remove).
* src/tgbaalgos/remfin.cc: Call purge_dead_states().
* src/tgbatest/remfin.test, src/tgbatest/det.test: Adjust expected
output.
* doc/org/autfilt.org: Update example.
parent b4e22a3c
......@@ -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=<!b>]
2 -> 1 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
2 -> 2 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
2 -> 3 [label=<!b>]
2 -> 4 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
2 -> 5 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
2 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font>>]
3 [label="3"]
4 [label="4"]
5 [label="5"]
5 -> 3 [label=<!b<br/><font color="#F17CB0">❶</font><font color="#60BD68">❹</font>>]
5 -> 4 [label=<a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font><font color="#60BD68">❹</font>>]
5 -> 5 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font><font color="#60BD68">❹</font>>]
3 -> 3 [label=<!a &amp; !b<br/><font color="#5DA5DA">⓿</font><font color="#F17CB0">❶</font><font color="#60BD68">❹</font>>]
}
#+end_example
......
......@@ -178,52 +178,74 @@ namespace spot
unsigned num_states = g_.num_states();
if (num_states == 0)
return;
std::vector<unsigned> info(num_states, 0);
// In this loop, info[s] means that the state is useless.
bool untouched;
std::vector<unsigned> useful(num_states, 0);
// Make a DFS to compute a topological order.
std::vector<unsigned> order;
order.reserve(num_states);
std::vector<std::pair<unsigned, unsigned>> 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)
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 (!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])
{
info[s] = true;
untouched = false;
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;
}
while (!untouched);
// Assume that the initial state is useful.
info[init_number_] = false;
// 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;
// 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);
}
}
......@@ -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';
......
......@@ -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 <<EOF
digraph G {
......@@ -131,16 +124,12 @@ digraph G {
0 -> 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
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment