From e04b4eb9fbbbf1b4dce5102b43ee0efb4b81db9a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 May 2015 08:07:13 +0200 Subject: [PATCH] acc: better Rabin/Streett detection * src/twa/acc.cc: Allow duplicate and reordered pairs. Also recognize the single-pair cases. * src/twaalgos/hoa.cc: When Rabin or Streett is detected, canonicalize the Acceptance: line. * src/tests/hoaparse.test, wrap/python/tests/accparse2.py: More tests. * src/tests/sbacc.test: Adjust. --- src/tests/hoaparse.test | 86 +++++++++++++++++ src/tests/sbacc.test | 1 + src/twa/acc.cc | 167 +++++++++++++++++++++++---------- src/twaalgos/hoa.cc | 13 ++- wrap/python/tests/accparse2.py | 63 +++++++++++++ 5 files changed, 280 insertions(+), 50 deletions(-) diff --git a/src/tests/hoaparse.test b/src/tests/hoaparse.test index da4885b58..307f6a02e 100755 --- a/src/tests/hoaparse.test +++ b/src/tests/hoaparse.test @@ -1769,6 +1769,21 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" +/* This is Streett, but badly ordered */ +Acceptance: 4 (Inf(3) | Fin(2)) & (Fin(0) | Inf(1)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&!1] 0 {2} +[0&!1] 0 {1 2} +[!0&1] 0 {3} +[0&1] 0 {1 3} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" Acceptance: 6 Fin(0) | (Fin(1) & Inf(2) & Inf(3)) | (Fin(4) & Inf(5)) --BODY-- State: 0 @@ -1781,6 +1796,19 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" +/* generalized-Rabin, but badely ordered */ +Acceptance: 6 (Inf(5) & Fin(4)) | Fin(0) | (Inf(2) & Fin(1) & Inf(3)) +--BODY-- +State: 0 +[!0&!1] 0 {0 1 4} +[0&!1] 0 {2 4} +[!0&1] 0 {3 5} +[0&1] 0 {1 3} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" Acceptance: 3 Fin(0)|Fin(1)|Fin(2) --BODY-- State: 0 @@ -1875,6 +1903,36 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" +acc-name: Streett 2 +Acceptance: 4 (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&!1] 0 {2} +[0&!1] 0 {1 2} +[!0&1] 0 {3} +[0&1] 0 {1 3} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +acc-name: generalized-Rabin 3 0 2 1 +Acceptance: 6 Fin(0) | (Fin(1) & (Inf(2)&Inf(3))) | (Fin(4) & Inf(5)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&!1] 0 {0 1 4} +[0&!1] 0 {2 4} +[!0&1] 0 {3 5} +[0&1] 0 {1 3} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" acc-name: generalized-Rabin 3 0 2 1 Acceptance: 6 Fin(0) | (Fin(1) & (Inf(2)&Inf(3))) | (Fin(4) & Inf(5)) properties: trans-labels explicit-labels trans-acc complete @@ -2000,6 +2058,20 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" +Acceptance: 4 (Fin(3) & Inf(2)) | (Fin(1) & Inf(0)) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&!1] 0 {2} +[0&!1] 0 {1 2} +[!0&1] 0 {3} +[0&1] 0 {1 3} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" Acceptance: 6 (Inf(1) | (Fin(2)|Fin(3))) & (Inf(4) | Fin(5)) & Inf(0) properties: trans-labels explicit-labels trans-acc complete properties: deterministic @@ -2014,6 +2086,20 @@ HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" +Acceptance: 6 (Inf(4) | Fin(5)) & (Inf(1) | (Fin(2)|Fin(3))) & Inf(0) +properties: trans-labels explicit-labels trans-acc complete +properties: deterministic +--BODY-- +State: 0 +[!0&!1] 0 {0 1 4} +[0&!1] 0 {2 4} +[!0&1] 0 {3 5} +[0&1] 0 {1 3} +--END-- +HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" acc-name: generalized-Buchi 3 Acceptance: 3 Inf(0)&Inf(1)&Inf(2) properties: trans-labels explicit-labels trans-acc complete diff --git a/src/tests/sbacc.test b/src/tests/sbacc.test index e2eee7d11..49028f366 100755 --- a/src/tests/sbacc.test +++ b/src/tests/sbacc.test @@ -85,6 +85,7 @@ HOA: v1 States: 3 Start: 0 AP: 1 "a" +acc-name: Streett 1 Acceptance: 2 Fin(0) | Inf(1) properties: trans-labels explicit-labels state-acc deterministic --BODY-- diff --git a/src/twa/acc.cc b/src/twa/acc.cc index 0335f8164..e0088c208 100644 --- a/src/twa/acc.cc +++ b/src/twa/acc.cc @@ -348,55 +348,92 @@ namespace spot return false; } + + namespace + { + // Is Rabin or Streett, depending on highop and lowop. + static bool + is_rs(const acc_cond::acc_code& code, + acc_cond::acc_op highop, + acc_cond::acc_op lowop, + acc_cond::mark_t all_sets) + { + unsigned s = code.back().size; + auto mainop = code.back().op; + if (mainop == highop) + { + // The size must be a multiple of 5. + if ((s != code.size() - 1) || (s % 5)) + return false; + } + else // Single pair? + { + if (s != 4 || mainop != lowop) + return false; + // Pretend we where in a unary highop. + s = 5; + } + acc_cond::mark_t seen_fin = 0U; + acc_cond::mark_t seen_inf = 0U; + while (s) + { + if (code[--s].op != lowop) + return false; + auto o1 = code[--s].op; + auto m1 = code[--s].mark; + auto o2 = code[--s].op; + auto m2 = code[--s].mark; + + // We assume + // Fin(n) lowop Inf(n+1) + // o1 (m1) o2 (m2) + // swap if it is the converse + if (o2 == acc_cond::acc_op::Fin) + { + std::swap(o1, o2); + std::swap(m1, m2); + } + if (o1 != acc_cond::acc_op::Fin + || o2 != acc_cond::acc_op::Inf + || m1.count() != 1 + || m2.id != (m1.id << 1)) + return false; + seen_fin |= m1; + seen_inf |= m2; + } + + return (!(seen_fin & seen_inf) + && (seen_fin | seen_inf) == all_sets); + } + } + int acc_cond::is_rabin() const { if (code_.is_false()) return num_ == 0 ? 0 : -1; - if ((num_ & 1) - || code_.is_true() - || code_.back().op != acc_op::Or) + if ((num_ & 1) || code_.is_true()) return -1; - // The size must be a multiple of 5. - auto s = code_.back().size; - if ((s != code_.size() - 1) || (s % 5)) + + if (is_rs(code_, acc_op::Or, acc_op::And, all_sets())) + return num_ / 2; + else return -1; - auto p = s / 5; // number of pairs - unsigned n = 0; - while (s) - if (code_[--s].op != acc_op::And - || code_[--s].op != acc_op::Fin - || code_[--s].mark != acc_cond::mark_t({n++}) - || code_[--s].op != acc_op::Inf - || code_[--s].mark != acc_cond::mark_t({n++})) - return -1; - return p; } int acc_cond::is_streett() const { if (code_.is_true()) return num_ == 0 ? 0 : -1; - if ((num_ & 1) - || code_.is_false() - || code_.back().op != acc_op::And) + if ((num_ & 1) || code_.is_false()) return -1; - // The size must be a multiple of 5. - auto s = code_.back().size; - if ((s != code_.size() - 1) || (s % 5)) + + if (is_rs(code_, acc_op::And, acc_op::Or, all_sets())) + return num_ / 2; + else return -1; - auto p = s / 5; // number of pairs - unsigned n = 0; - while (s) - if (code_[--s].op != acc_op::Or - || code_[--s].op != acc_op::Fin - || code_[--s].mark != acc_cond::mark_t({n++}) - || code_[--s].op != acc_op::Inf - || code_[--s].mark != acc_cond::mark_t({n++})) - return -1; - return p; } - // Return the number of Inf in each pair. + // PAIRS contains the number of Inf in each pair. bool acc_cond::is_generalized_rabin(std::vector& pairs) const { pairs.clear(); @@ -408,41 +445,73 @@ namespace spot if (code_.is_true() || code_.back().op != acc_op::Or) return false; + auto s = code_.back().size; - unsigned n = 0; + acc_cond::mark_t seen_fin = 0U; + acc_cond::mark_t seen_inf = 0U; + // Each pairs is the position of a Fin followed + // by the number of Inf. + std::map p; while (s) { --s; if (code_[s].op == acc_op::And) { - if (code_[--s].op != acc_op::Fin - || code_[--s].mark != acc_cond::mark_t({n++}) - || code_[--s].op != acc_op::Inf) - return false; - unsigned p = 0; - auto m = code_[--s].mark; - while (m.has(n)) + auto o1 = code_[--s].op; + auto m1 = code_[--s].mark; + auto o2 = code_[--s].op; + auto m2 = code_[--s].mark; + + // We assume + // Fin(n) & Inf({n+1,n+2,...,n+i}) + // o1 (m1) o2 (m2) + // swap if it is the converse + if (o2 == acc_cond::acc_op::Fin) { - m.clear(n); - ++p; - ++n; + std::swap(o1, o2); + std::swap(m1, m2); } - if (m) + + if (o1 != acc_cond::acc_op::Fin + || o2 != acc_cond::acc_op::Inf + || m1.count() != 1) return false; - pairs.push_back(p); + + unsigned i = m2.count(); + // If we have seen this pair already, it must have the + // same size. + if (p.emplace(m1.max_set(), i).first->second != i) + return false; + assert(i > 0); + unsigned j = m1.max_set(); // == n+1 + do + if (!m2.has(j++)) + return false; + while (--i); + + seen_fin |= m1; + seen_inf |= m2; } else if (code_[s].op == acc_op::Fin) { - if (code_[--s].mark != acc_cond::mark_t({n++})) + auto m1 = code_[--s].mark; + if (m1.count() != 1) return false; - pairs.push_back(0); + // If we have seen this pair already, it must have the + // same size. + if (p.emplace(m1.max_set(), 0U).first->second != 0U) + return false; + seen_fin |= m1; } else { return false; } } - return true; + for (auto i: p) + pairs.push_back(i.second); + return (!(seen_fin & seen_inf) + && (seen_fin | seen_inf) == all_sets()); } acc_cond::acc_code diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 499bff7dd..e56e3928d 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -282,6 +282,7 @@ namespace spot os << nl; unsigned num_acc = aut->acc().num_sets(); + acc_cond::acc_code acc_c = aut->acc().get_acceptance(); if (aut->acc().is_generalized_buchi()) { if (aut->acc().is_true()) @@ -309,6 +310,9 @@ namespace spot if (r > 0) { os << "acc-name: Rabin " << r << nl; + // Force the acceptance to remove any duplicate sets, and + // make sure it is correctly ordered. + acc_c = acc_cond::acc_code::rabin(r); } else { @@ -317,6 +321,9 @@ namespace spot if (r > 0) { os << "acc-name: Streett " << r << nl; + // Force the acceptance to remove any duplicate sets, and + // make sure it is correctly ordered. + acc_c = acc_cond::acc_code::streett(r); } else { @@ -327,6 +334,10 @@ namespace spot for (auto p: pairs) os << ' ' << p; os << nl; + // Force the acceptance to remove any duplicate + // sets, and make sure it is correctly ordered. + acc_c = acc_cond::acc_code::generalized_rabin(pairs.begin(), + pairs.end()); } else { @@ -342,7 +353,7 @@ namespace spot } } os << "Acceptance: " << num_acc << ' '; - os << aut->acc().get_acceptance(); + os << acc_c; os << nl; os << "properties:"; // Make sure the property line is not too large, diff --git a/wrap/python/tests/accparse2.py b/wrap/python/tests/accparse2.py index 9b05c84b8..9a69a3c11 100644 --- a/wrap/python/tests/accparse2.py +++ b/wrap/python/tests/accparse2.py @@ -31,3 +31,66 @@ a.set_acceptance(spot.parse_acc_code( 'Inf(4) | (Fin(3)&Inf(2)) | (Fin(3)&Fin(1)&Inf(0))')) assert(a.is_parity() == [False, False, False]) assert(a.is_parity(True) == [True, True, False]) + +a = spot.acc_cond(0) +a.set_acceptance(spot.parse_acc_code('all')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 0) +a.set_acceptance(spot.parse_acc_code('none')) +assert(a.is_rabin() == 0) +assert(a.is_streett() == -1) + +a = spot.acc_cond(2) +a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))')) +assert(a.is_rabin() == 1) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('Inf(1)&Fin(0)')) +assert(a.is_rabin() == 1) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 1) +a.set_acceptance(spot.parse_acc_code('Inf(1)|Fin(0)')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 1) + +a = spot.acc_cond(4) +a.set_acceptance(spot.parse_acc_code('(Fin(0)&Inf(1))|(Fin(2)&Inf(3))')) +assert(a.is_rabin() == 2) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(0)&Inf(1))')) +assert(a.is_rabin() == 2) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('(Inf(2)&Fin(3))|(Fin(0)&Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('(Inf(3)&Fin(2))|(Fin(2)&Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('(Inf(1)&Fin(0))|(Fin(0)&Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) +r = spot.parse_acc_code('(Fin(0)&Inf(1))|(Inf(1)&Fin(0))|(Inf(3)&Fin(2))') +a.set_acceptance(r) +assert(a.is_rabin() == 2) +assert(a.is_streett() == -1) + +a.set_acceptance(spot.parse_acc_code('(Fin(0)|Inf(1))&(Fin(2)|Inf(3))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 2) +a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(0)|Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 2) +a.set_acceptance(spot.parse_acc_code('(Inf(2)|Fin(3))&(Fin(0)|Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('(Inf(3)|Fin(2))&(Fin(2)|Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) +a.set_acceptance(spot.parse_acc_code('(Inf(1)|Fin(0))&(Fin(0)|Inf(1))')) +assert(a.is_rabin() == -1) +assert(a.is_streett() == -1) +r = spot.parse_acc_code('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))') +a.set_acceptance(r) +assert(a.is_rabin() == -1) +assert(a.is_streett() == 2)