From 313e43c84bc2b238b54dd4bd5fed8d773fd6ed9e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 17 Nov 2023 14:04:22 +0100 Subject: [PATCH] translate: fix #551 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. --- spot/twaalgos/translate.cc | 7 ++++++- tests/core/ltl2tgba2.test | 13 +++++++++++++ 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 1db1f1aa4..9bc6690d6 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -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; } diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 6e64e7081..370e744f9 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -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"