From d276f73eed04d903bbb53c339f2c4a5b00f4b2e3 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 19 May 2015 19:31:13 +0200 Subject: [PATCH] hoa: output acc-name for several acceptance types So far the HOA output would emit an acc-name only for generalized-Buchi or inferior types (Buchi, all). It now knows about none, co-Buchi, generalized-co-Buchi, Rabin, Streett, and generalized-Rabin as well. * src/twa/acc.cc, src/twa/acc.hh: Add detection code. * src/twaalgos/hoa.cc: Use it. * src/tests/remfin.test, src/tests/maskacc.test, src/tests/complete.test, src/tests/sim3.test, src/tests/ltl2dstar.test: Adjust tests. * src/tests/hoaparse.test: Adjust and add more tests. --- src/tests/complete.test | 2 + src/tests/hoaparse.test | 187 +++++++++++++++++++++++++++++++++++++++ src/tests/ltl2dstar.test | 1 + src/tests/maskacc.test | 2 + src/tests/remfin.test | 1 + src/tests/sim3.test | 2 + src/twa/acc.cc | 97 ++++++++++++++++++++ src/twa/acc.hh | 55 ++++++++---- src/twaalgos/hoa.cc | 39 ++++++++ 9 files changed, 371 insertions(+), 15 deletions(-) diff --git a/src/tests/complete.test b/src/tests/complete.test index a1a06aa57..777a41924 100755 --- a/src/tests/complete.test +++ b/src/tests/complete.test @@ -64,6 +64,7 @@ HOA: v1 States: 3 Start: 0 AP: 1 "a" +acc-name: co-Buchi Acceptance: 1 Fin(0) properties: trans-labels explicit-labels state-acc complete properties: deterministic @@ -99,6 +100,7 @@ HOA: v1 States: 2 Start: 0 AP: 1 "a" +acc-name: none Acceptance: 0 f properties: trans-labels explicit-labels state-acc complete properties: deterministic diff --git a/src/tests/hoaparse.test b/src/tests/hoaparse.test index 9bfe868ea..1c44d1574 100755 --- a/src/tests/hoaparse.test +++ b/src/tests/hoaparse.test @@ -1375,6 +1375,7 @@ HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" +acc-name: Rabin 2 Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) properties: trans-labels explicit-labels state-acc deterministic --BODY-- @@ -1428,6 +1429,7 @@ HOA: v1 States: 2 Start: 0 AP: 2 "a" "b" +acc-name: Rabin 2 Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) properties: trans-labels explicit-labels state-acc deterministic --BODY-- @@ -1731,3 +1733,188 @@ expecterr input <input <& pairs) const + { + pairs.clear(); + if (is_generalized_co_buchi()) + { + pairs.resize(num_); + return true; + } + if (code_.is_true() + || code_.back().op != acc_op::Or) + return false; + auto s = code_.back().size; + unsigned n = 0; + 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)) + { + m.clear(n); + ++p; + ++n; + } + if (m) + return false; + pairs.push_back(p); + } + else if (code_[s].op == acc_op::Fin) + { + if (code_[--s].mark != acc_cond::mark_t({n++})) + return false; + pairs.push_back(0); + } + else + { + return false; + } + } + return true; + } + namespace { bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map) diff --git a/src/twa/acc.hh b/src/twa/acc.hh index 97c31e79e..b76efcd57 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -501,12 +501,12 @@ namespace spot return res; } - template - static acc_code generalized_rabin(iterator begin, iterator end) + template + static acc_code generalized_rabin(Iterator begin, Iterator end) { acc_cond::acc_code res = f(); unsigned n = 0; - for (iterator i = begin; i != end; ++i) + for (Iterator i = begin; i != end; ++i) { acc_cond::acc_code pair = fin({n++}); acc_cond::mark_t m = 0U; @@ -854,6 +854,28 @@ namespace spot return uses_fin_acceptance_; } + bool is_true() const + { + return code_.is_true(); + } + + bool is_false() const + { + return code_.is_false(); + } + + bool is_buchi() const + { + unsigned s = code_.size(); + return num_ == 1 && + s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets(); + } + + bool is_co_buchi() const + { + return num_ == 1 && is_generalized_co_buchi(); + } + void set_generalized_buchi() { set_acceptance(inf(all_sets())); @@ -866,6 +888,21 @@ namespace spot (s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets()); } + bool is_generalized_co_buchi() const + { + unsigned s = code_.size(); + return (s == 2 && + code_[1].op == acc_op::Fin && code_[0].mark == all_sets()); + } + + // Returns a number of pairs (>=0) if Rabin, or -1 else. + int is_rabin() const; + // Returns a number of pairs (>=0) if Streett, or -1 else. + int is_streett() const; + + // Return the number of Inf in each pair. + bool is_generalized_rabin(std::vector& pairs) const; + static acc_code generalized_buchi(unsigned n) { mark_t m((1U << n) - 1); @@ -874,18 +911,6 @@ namespace spot return acc_code::inf(m); } - bool is_buchi() const - { - unsigned s = code_.size(); - return num_ == 1 && - s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets(); - } - - bool is_true() const - { - return code_.is_true(); - } - protected: bool check_fin_acceptance() const; diff --git a/src/twaalgos/hoa.cc b/src/twaalgos/hoa.cc index 8e8922932..d95216b6b 100644 --- a/src/twaalgos/hoa.cc +++ b/src/twaalgos/hoa.cc @@ -292,6 +292,45 @@ namespace spot os << "acc-name: generalized-Buchi " << num_acc; os << nl; } + else if (aut->acc().is_generalized_co_buchi()) + { + if (aut->acc().is_false()) + os << "acc-name: none"; + else if (aut->acc().is_co_buchi()) + os << "acc-name: co-Buchi"; + else + os << "acc-name: generalized-co-Buchi " << num_acc; + os << nl; + } + else + { + int r = aut->acc().is_rabin(); + assert(r != 0); + if (r > 0) + { + os << "acc-name: Rabin " << r << nl; + } + else + { + r = aut->acc().is_streett(); + assert(r != 0); + if (r > 0) + { + os << "acc-name: Streett " << r << nl; + } + else + { + std::vector pairs; + if (aut->acc().is_generalized_rabin(pairs)) + { + os << "acc-name: generalized-Rabin " << pairs.size(); + for (auto p: pairs) + os << ' ' << p; + os << nl; + } + } + } + } os << "Acceptance: " << num_acc << ' '; os << aut->acc().get_acceptance(); os << nl;