From 396024143c9c5c505048d7b2b893794f2ccfa343 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Dec 2017 17:53:30 +0100 Subject: [PATCH 1/5] to_tgba: fix handling of CNF with multiple unit clauses MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #313, reported by František Blahoudek. * spot/twaalgos/totgba.cc (to_generalized_buchi): Fix it. * tests/core/remfin.test: Test it. * NEWS: Mention it. --- NEWS | 6 ++- spot/twaalgos/totgba.cc | 9 ++++- tests/core/remfin.test | 86 +++++++++++++++++++++++++++++++++++++++++ 3 files changed, 98 insertions(+), 3 deletions(-) diff --git a/NEWS b/NEWS index 497965b7f..be9acef7a 100644 --- a/NEWS +++ b/NEWS @@ -1,6 +1,10 @@ New in spot 2.4.3.dev (not yet released) - Nothing yet. + Bugs fixed: + + - The generic to_generalized_buchi() function would fail if the + Fin-less & CNF version of the acceptance condition had several + unit clauses. New in spot 2.4.3 (2017-12-19) diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index 6f3081265..a7bba102b 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -75,7 +75,8 @@ namespace spot while (pos >= end) { auto term_end = pos - 1 - pos->sub.size; - if (pos->sub.op == acc_cond::acc_op::Or) + bool inor = pos->sub.op == acc_cond::acc_op::Or; + if (inor) --pos; acc_cond::mark_t m = 0U; while (pos > term_end) @@ -84,7 +85,11 @@ namespace spot m |= pos[-1].mark; pos -= 2; } - res.emplace_back(m); + if (inor) + res.emplace_back(m); + else + for (unsigned i: m.sets()) + res.emplace_back(acc_cond::mark_t({i})); } return res; } diff --git a/tests/core/remfin.test b/tests/core/remfin.test index aa6074496..88908c445 100755 --- a/tests/core/remfin.test +++ b/tests/core/remfin.test @@ -270,6 +270,29 @@ HOA: v1 States: 3 Start: 0 AP: 2 "b" "c" Acceptance: 3 Fin(0) & complete --BODY-- State: 0 [!0] 0 {1 2} [0] 0 {0 1 2} [0&!1] 1 [0&1] 2 State: 1 [!0 | !1] 1 {1 2} [0&1] 2 {1} State: 2 [!1] 1 {1 2} [1] 2 {1} --END-- +/* +** Issue #313. The TGBA conversion of this automaton was wrong. +*/ +HOA: v1 +States: 2 +Start: 0 +AP: 3 "a" "b" "c" +Acceptance: 4 (Fin(1)|Fin(2)) & Fin(0) & Inf(3) +properties: trans-labels explicit-labels trans-acc complete +--BODY-- +State: 0 +[t] 0 {0 3} +[1 | 2] 0 {1 3} +[0] 0 {2 3} +[!1&!2] 1 {1} +State: 1 +[2] 0 {0 3} +[2] 0 {1 3} +[0&2] 0 {2 3} +[!2] 1 {0} +[!2] 1 {1} +[0&!2] 1 {2} +--END-- EOF acctwelve='Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)' @@ -844,6 +867,37 @@ State: 3 [!1] 2 {0 1} [1] 3 {0} --END-- +HOA: v1 +States: 6 +Start: 0 +AP: 3 "a" "b" "c" +Acceptance: 4 (Inf(0)&Inf(2)&Inf(3)) | (Inf(0)&Inf(1)&Inf(3)) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[t] 0 +[!1&!2] 1 +[0] 2 +[1 | 2] 4 +State: 1 +[2] 0 +[!2] 1 +[0&2] 2 +[0&!2] 3 +[2] 4 +[!2] 5 +State: 2 +[0] 2 {0 1 3} +State: 3 +[0&2] 2 {0 1 3} +[0&!2] 3 {0 1} +State: 4 +[1 | 2] 4 {0 2 3} +[!1&!2] 5 {0 2} +State: 5 +[2] 4 {0 2 3} +[!2] 5 {0 2} +--END-- EOF cat >expected-tgba < output From 18e65f3bc8f7760422e68d80b420e14f1833a1c2 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 22 Dec 2017 18:27:07 +0100 Subject: [PATCH 2/5] sbacc: fix sbacc producing complete automata marked as incomplete MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fixes #312, reported by František Blahoudek. * spot/twaalgos/sbacc.cc: Detect the case were this can happen, and fix it. * tests/core/sbacc.test: New test case. * NEWS: Mention the bug. --- NEWS | 4 ++++ spot/twaalgos/sbacc.cc | 11 +++++++++++ tests/core/sbacc.test | 14 ++++++++++++++ 3 files changed, 29 insertions(+) diff --git a/NEWS b/NEWS index be9acef7a..22d53f139 100644 --- a/NEWS +++ b/NEWS @@ -6,6 +6,10 @@ New in spot 2.4.3.dev (not yet released) Fin-less & CNF version of the acceptance condition had several unit clauses. + - If the automaton passed to sbacc() was incomplete because of some + unreachable states, then it was possible that the output would + marked incomplete while it was in fact complete. + New in spot 2.4.3 (2017-12-19) Bugs fixed: diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 59701abdb..70862e432 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -168,6 +168,17 @@ namespace spot } } res->merge_edges(); + + // If the automaton was marked as not complete, and we have + // ignored some unreachable state, then it is possible that the + // result becomes complete. + if (res->prop_complete().is_false()) + for (unsigned i = 0; i < ns; ++i) + if (!si.reachable_state(i)) + { + res->prop_complete(trival::maybe()); + break; + } return res; } } diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 65482b54f..049473c26 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -265,3 +265,17 @@ EOF autfilt --sbacc alt.hoa > out.hoa diff out.hoa expect.hoa + +# Issue #312 +autfilt -S < Date: Sun, 24 Dec 2017 19:07:24 +0100 Subject: [PATCH 3/5] sbacc: more fixes related to #312 The issue also exists with determinism. * tests/core/sbacc.test: New test case. * spot/twaalgos/sbacc.cc: Fix it. * NEWS: Update. --- NEWS | 7 ++++--- spot/twaalgos/sbacc.cc | 13 ++++++++----- tests/core/sbacc.test | 13 +++++++++++++ 3 files changed, 25 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 22d53f139..9f928d271 100644 --- a/NEWS +++ b/NEWS @@ -6,9 +6,10 @@ New in spot 2.4.3.dev (not yet released) Fin-less & CNF version of the acceptance condition had several unit clauses. - - If the automaton passed to sbacc() was incomplete because of some - unreachable states, then it was possible that the output would - marked incomplete while it was in fact complete. + - If the automaton passed to sbacc() was incomplete or + non-deterministic because of some unreachable states, then it was + possible that the output would marked similarly while it was in + fact complete or deterministic. New in spot 2.4.3 (2017-12-19) diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 70862e432..d971612f6 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -169,14 +169,17 @@ namespace spot } res->merge_edges(); - // If the automaton was marked as not complete, and we have - // ignored some unreachable state, then it is possible that the - // result becomes complete. - if (res->prop_complete().is_false()) + // If the automaton was marked as not complete or not universal, + // and we have ignored some unreachable state, then it is possible + // that the result becomes complete or universal. + if (res->prop_complete().is_false() || res->prop_universal().is_false()) for (unsigned i = 0; i < ns; ++i) if (!si.reachable_state(i)) { - res->prop_complete(trival::maybe()); + if (res->prop_complete().is_false()) + res->prop_complete(trival::maybe()); + if (res->prop_universal().is_false()) + res->prop_universal(trival::maybe()); break; } return res; diff --git a/tests/core/sbacc.test b/tests/core/sbacc.test index 049473c26..57cb1938a 100755 --- a/tests/core/sbacc.test +++ b/tests/core/sbacc.test @@ -279,3 +279,16 @@ State: 0 [t] 0 {0} State: 1 --END-- EOF + +autfilt -S < Date: Mon, 25 Dec 2017 15:41:19 +0100 Subject: [PATCH 4/5] Release Spot 2.4.4 * NEWS, configure.ac, doc/org/setup.org: Bump version. --- NEWS | 2 +- configure.ac | 2 +- doc/org/setup.org | 10 +++++----- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/NEWS b/NEWS index 9f928d271..1bd037bb9 100644 --- a/NEWS +++ b/NEWS @@ -1,4 +1,4 @@ -New in spot 2.4.3.dev (not yet released) +New in spot 2.4.4 (2017-12-25) Bugs fixed: diff --git a/configure.ac b/configure.ac index e547ca657..0bf06a96a 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.4.3.dev], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.4.4], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests]) diff --git a/doc/org/setup.org b/doc/org/setup.org index 96ab4dc45..bb24c571f 100644 --- a/doc/org/setup.org +++ b/doc/org/setup.org @@ -1,8 +1,8 @@ #+OPTIONS: H:2 num:nil toc:t html-postamble:nil #+EMAIL: spot@lrde.epita.fr #+HTML_LINK_HOME: index.html -#+MACRO: SPOTVERSION 2.4.3 -#+MACRO: LASTRELEASE 2.4.3 -#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.4.3.tar.gz][=spot-2.4.3.tar.gz=]] -#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-4-3/NEWS][summary of the changes]] -#+MACRO: LASTDATE 2017-12-19 +#+MACRO: SPOTVERSION 2.4.4 +#+MACRO: LASTRELEASE 2.4.4 +#+MACRO: LASTTARBALL [[http://www.lrde.epita.fr/dload/spot/spot-2.4.4.tar.gz][=spot-2.4.4.tar.gz=]] +#+MACRO: LASTNEWS [[https://gitlab.lrde.epita.fr/spot/spot/blob/spot-2-4-4/NEWS][summary of the changes]] +#+MACRO: LASTDATE 2017-12-25 From 9c77cb321e648b13302fb8ff2c77265776492cc8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 25 Dec 2017 15:46:44 +0100 Subject: [PATCH 5/5] * NEWS, configure.ac: Bump version to 2.4.4.dev. --- NEWS | 4 ++++ configure.ac | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/NEWS b/NEWS index 1bd037bb9..9820dfc4d 100644 --- a/NEWS +++ b/NEWS @@ -1,3 +1,7 @@ +New in spot 2.4.4.dev (net yet released) + + Nothing yet. + New in spot 2.4.4 (2017-12-25) Bugs fixed: diff --git a/configure.ac b/configure.ac index 0bf06a96a..3d01d0109 100644 --- a/configure.ac +++ b/configure.ac @@ -21,7 +21,7 @@ # along with this program. If not, see . AC_PREREQ([2.61]) -AC_INIT([spot], [2.4.4], [spot@lrde.epita.fr]) +AC_INIT([spot], [2.4.4.dev], [spot@lrde.epita.fr]) AC_CONFIG_AUX_DIR([tools]) AC_CONFIG_MACRO_DIR([m4]) AM_INIT_AUTOMAKE([1.11 gnu tar-ustar color-tests parallel-tests])