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

translate: fix #551

Browse source 
Reported by Yann Thierry-Mieg.

* spot/twaalgos/translate.cc: Run scc_filter if relabel_here reduced
the number of edges, because maybe we have more to remove.
* tests/core/ltl2tgba2.test: Add test case.
This commit is contained in:
Alexandre Duret-Lutz 2023-11-17 14:04:22 +01:00
parent f0928f2b52
commit 313e43c84b
2 changed files with 19 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

7
spot/twaalgos/translate.cc
View file

@ -576,7 +576,12 @@ namespace spot
auto aut = run_aux(r);
if (!m.empty())
relabel_here(aut, &m);
{
unsigned ne = aut->num_edges();
relabel_here(aut, &m);
if (aut->num_edges() < ne)
return finalize(do_scc_filter(aut));
}
return aut;
}

13
tests/core/ltl2tgba2.test
View file

@ -527,3 +527,16 @@ v29)))& (G F (v11 -> (v46 & v29)))& (G F (v13 -> (v47 & v29)))&
(v11 | (v13 | (v15 | (v17 | v19))))))))))))'
ltl2tgba -p'min even' -D -C "$f" --stats='%s %e'>out
test '22 288' = "`cat out`"
# Make sure relabel-overlap still reduce empty automata. Issue #551.
f='(G(!(G(p16) U G(p5))))&&((p5&&!p3&&p4&&!p2)) &&
((p16&&!p14&&p5&&p15)) && (p5) && (p16) && (X(p5)) &&
(X(!(p2&&!p3&&p4&&!p5))) && (X(!(p3&&p4&&!p5))) && (X(X(!(p3&&!p5))))
&& (X(X(!(p2&&!p3&&!p5)))) && (X(X(p5))) && (X((!p14&&p5))) &&
(X(X((!p14&&p5)))) && (F(G(p5))) && (F(G(!p16))) && (G((!p2||p3||p5))) &&
(G((!p3||p5))) && (G((!p2||p3||!p4||p5))) && (G((!p3||!p4||p5)))'
s8=`ltl2tgba -x relabel-overlap=8 -f "$f" --stats=%g,%s,%e`
test "$s8" = "t,1,0"
s7=`ltl2tgba -x relabel-overlap=7 -f "$f" --stats=%g,%s,%e`
test "$s7" = "t,1,0"