diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 92b979a7f..1382e8ec4 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -464,10 +464,11 @@ namespace spot bool acc_cond::acc_code::is_dnf() const { - if (empty()) + if (empty() || size() == 2) return true; auto pos = &back(); auto start = &front(); + auto and_scope = pos + 1; if (pos->op == acc_cond::acc_op::Or) --pos; while (pos > start) @@ -477,12 +478,16 @@ namespace spot case acc_cond::acc_op::Or: return false; case acc_cond::acc_op::And: + and_scope = std::min(and_scope, pos - pos->size); --pos; break; - case acc_cond::acc_op::Inf: - case acc_cond::acc_op::InfNeg: case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: + if (pos[-1].mark.count() > 1 && pos > and_scope) + return false; + /* fall through */ + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: pos -= 2; break; } diff --git a/src/tgbatest/acc.cc b/src/tgbatest/acc.cc index f0ed5ba31..253fe2fd1 100644 --- a/src/tgbatest/acc.cc +++ b/src/tgbatest/acc.cc @@ -108,15 +108,23 @@ int main() auto code1 = ac.inf({0, 1, 3}); - std::cout << code1.size() << ' ' << code1 << '\n'; + std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; code1.append_or(ac.fin({2})); - std::cout << code1.size() << ' ' << code1 << '\n'; + std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; code1.append_or(ac.fin({0})); - std::cout << code1.size() << ' ' << code1 << '\n'; + std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; code1.append_or(ac.fin({})); - std::cout << code1.size() << ' ' << code1 << '\n'; + std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; code1.append_and(ac.inf({})); - std::cout << code1.size() << ' ' << code1 << '\n'; + std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; + auto code2 = code1; + code1.append_and(ac.fin({0, 1})); + std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; code1.append_and(ac.fin({})); - std::cout << code1.size() << ' ' << code1 << '\n'; + std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n'; + code2.append_or(ac.fin({0, 1})); + std::cout << code2.size() << ' ' << code2 << ' ' << code2.is_dnf() << '\n'; + auto code3 = ac.inf({0, 1}); + code3.append_and(ac.fin({2, 3})); + std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n'; } diff --git a/src/tgbatest/acc.test b/src/tgbatest/acc.test index c0fb7b2a3..8168a5148 100755 --- a/src/tgbatest/acc.test +++ b/src/tgbatest/acc.test @@ -59,12 +59,15 @@ stripping #1: {0} #1: {4} #1: {2} -2 Inf(0)&Inf(1)&Inf(3) -5 Fin(2) | (Inf(0)&Inf(1)&Inf(3)) -7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) -7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) -7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) -2 f +2 Inf(0)&Inf(1)&Inf(3) 1 +5 Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1 +7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1 +7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1 +7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1 +10 (Fin(0)|Fin(1)) & (Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))) 0 +2 f 1 +9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1 +5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0 EOF run 0 ../acc | tee stdout