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

tra_to_tba: remove more useless edges

Browse source 
* spot/twaalgos/remfin.cc (tra_to_tba): Implement the same
optimization has in the generic remove_fin transformation.
* tests/python/tra2tba.py: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2020-07-24 16:24:28 +02:00
parent 567a5439c5
commit 05e6e08859
3 changed files with 18 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -49,7 +49,8 @@ New in spot 2.9.3.dev (not yet released)
used to take ages are now instantaneous. (See issue #412.) used to take ages are now instantaneous. (See issue #412.)
- remove_fin() learned to remove more unnecessary edges by using - remove_fin() learned to remove more unnecessary edges by using
propagate_marks_vector(). propagate_marks_vector(), both in the general case and in the
Rabin-like case.
Bugs fixed: Bugs fixed:

17
spot/twaalgos/remfin.cc
View file

@ -210,9 +210,13 @@ namespace spot
std::vector<bool> scc_is_tba_type(si.scc_count(), false); std::vector<bool> scc_is_tba_type(si.scc_count(), false);
std::vector<bool> final(aut->edge_vector().size(), false); std::vector<bool> final(aut->edge_vector().size(), false);
bool tba_type = true;
for (unsigned scc = 0; scc < si.scc_count(); ++scc) for (unsigned scc = 0; scc < si.scc_count(); ++scc)
scc_is_tba_type[scc] = is_scc_tba_type(aut, si, scc, {
aut_pairs, final); bool res = is_scc_tba_type(aut, si, scc, aut_pairs, final);
scc_is_tba_type[scc] = res;
tba_type &= res;
}
auto res = make_twa_graph(aut->get_dict()); auto res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut); res->copy_ap_of(aut);
@ -223,6 +227,11 @@ namespace spot
trival deterministic = aut->prop_universal(); trival deterministic = aut->prop_universal();
trival complete = aut->prop_complete(); trival complete = aut->prop_complete();
std::vector<bool> accedge(aut->edge_vector().size(), false);
std::vector<acc_cond::mark_t> propmarks;
if (!tba_type)
propmarks = propagate_marks_vector(aut, &si);
std::vector<unsigned> state_map(aut->num_states()); std::vector<unsigned> state_map(aut->num_states());
for (unsigned scc = 0; scc < si.scc_count(); ++scc) for (unsigned scc = 0; scc < si.scc_count(); ++scc)
{ {
@ -250,6 +259,8 @@ namespace spot
{ {
bool acc = !!(e.acc & scc_infs_alone); bool acc = !!(e.acc & scc_infs_alone);
res->new_acc_edge(e.src, e.dst, e.cond, acc); res->new_acc_edge(e.src, e.dst, e.cond, acc);
if (acc)
accedge[aut->edge_number(e)] = true;
} }
auto fins_alone = aut_pairs.fins_alone(); auto fins_alone = aut_pairs.fins_alone();
@ -262,7 +273,7 @@ namespace spot
state_map[s] = base++; state_map[s] = base++;
for (const auto& e: si.inner_edges_of(scc)) for (const auto& e: si.inner_edges_of(scc))
{ {
if (e.acc.has(r)) if (e.acc.has(r) || accedge[aut->edge_number(e)])
continue; continue;
auto src = state_map[e.src]; auto src = state_map[e.src];
auto dst = state_map[e.dst]; auto dst = state_map[e.dst];

11
tests/python/tra2tba.py
View file

@ -232,7 +232,7 @@ State: 0 "F(Gp3|GFp2)"
""") """)
exp = """HOA: v1 exp = """HOA: v1
States: 4 States: 3
Start: 0 Start: 0
AP: 2 "p3" "p2" AP: 2 "p3" "p2"
acc-name: Buchi acc-name: Buchi
@ -246,14 +246,8 @@ State: 0
State: 1 {0} State: 1 {0}
[!1] 0 [!1] 0
[1] 1 [1] 1
[0&!1] 2
[0&1] 3
State: 2 {0} State: 2 {0}
[0&!1] 2 [0&!1] 2
[0&1] 3
State: 3 {0}
[0&!1] 2
[0&1] 3
--END--""" --END--"""
res = spot.remove_fin(aut) res = spot.remove_fin(aut)
@ -648,9 +642,8 @@ State: 0
[!0] 0 [!0] 0
[0] 0 {0} [0] 0 {0}
[!0&!1] 1 [!0&!1] 1
[0&!1] 1 {0}
State: 1 State: 1
[!1] 1 {0} [!0&!1] 1 {0}
--END--""" --END--"""
res = spot.remove_fin(aut) res = spot.remove_fin(aut)