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