From 5b2c7b55edbf9a155234e784d07a9058664dd933 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 Feb 2015 22:36:13 +0100 Subject: [PATCH] acc: refactor strip() routines * src/tgba/acc.cc, src/tgba/acc.hh: Move the strip() routine from acc_cond into acc_cond::mark_t, and the strip() routine from cleanacc.cc into acc_cond::acc_code. Introduce helper functions to create inf()/fin()/t()/f() at the acc_code level. * src/tgbaalgos/cleanacc.cc: Simplify, using the strip() function from acc_code. * src/tgbaalgos/mask.cc (mask_acc_sets): Use the strip() function from acc_code so that it work on non-Buchi acceptance. * src/tgbatest/maskacc.test: Add a test for the latter change. * src/tgbaalgos/sccfilter.cc, src/tgbatest/acc.cc: Adjust the use mark_t::strip(). --- src/tgba/acc.cc | 129 +++++++++++++++++++++++-------- src/tgba/acc.hh | 153 +++++++++++++++++++++++++++---------- src/tgbaalgos/cleanacc.cc | 89 +-------------------- src/tgbaalgos/mask.cc | 8 +- src/tgbaalgos/sccfilter.cc | 6 +- src/tgbatest/acc.cc | 2 +- src/tgbatest/maskacc.test | 45 +++++++++++ 7 files changed, 267 insertions(+), 165 deletions(-) diff --git a/src/tgba/acc.cc b/src/tgba/acc.cc index 84250c426..4bc18fbf6 100644 --- a/src/tgba/acc.cc +++ b/src/tgba/acc.cc @@ -414,18 +414,12 @@ namespace spot acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos) { auto start = pos - pos->size; - - acc_cond::acc_code res; - res.resize(2); - res[0].mark = 0U; - res[1].size = 1; - switch (pos->op) { case acc_cond::acc_op::And: { --pos; - res[1].op = acc_cond::acc_op::Fin; // f + auto res = acc_cond::acc_code::f(); do { auto tmp = complement_rec(pos); @@ -439,7 +433,7 @@ namespace spot case acc_cond::acc_op::Or: { --pos; - res[1].op = acc_cond::acc_op::Inf; // t + auto res = acc_cond::acc_code::t(); do { auto tmp = complement_rec(pos); @@ -451,24 +445,16 @@ namespace spot return res; } case acc_cond::acc_op::Fin: - res[0].mark = pos[-1].mark; - res[1].op = acc_cond::acc_op::Inf; - return res; + return acc_cond::acc_code::inf(pos[-1].mark); case acc_cond::acc_op::Inf: - res[0].mark = pos[-1].mark; - res[1].op = acc_cond::acc_op::Fin; - return res; + return acc_cond::acc_code::fin(pos[-1].mark); case acc_cond::acc_op::FinNeg: - res[0].mark = pos[-1].mark; - res[1].op = acc_cond::acc_op::InfNeg; - return res; + return acc_cond::acc_code::inf_neg(pos[-1].mark); case acc_cond::acc_op::InfNeg: - res[0].mark = pos[-1].mark; - res[1].op = acc_cond::acc_op::FinNeg; - return res; + return acc_cond::acc_code::fin_neg(pos[-1].mark); } SPOT_UNREACHABLE(); - return acc_cond::acc_code{}; + return {}; } } @@ -476,18 +462,101 @@ namespace spot acc_cond::acc_code acc_cond::acc_code::complement() const { - if (empty()) - { - acc_cond::acc_code res; - res.resize(2); - res[0].mark = 0U; - res[1].op = acc_cond::acc_op::Fin; - res[1].size = 1; - return res; - } + if (is_true()) + return acc_cond::acc_code::f(); return complement_rec(&back()); } + namespace + { + static acc_cond::acc_code + strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing) + { + auto start = pos - pos->size; + switch (pos->op) + { + case acc_cond::acc_op::And: + { + --pos; + auto res = acc_cond::acc_code::t(); + do + { + auto tmp = strip_rec(pos, rem, missing); + tmp.append_and(std::move(res)); + std::swap(tmp, res); + pos -= pos->size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Or: + { + --pos; + auto res = acc_cond::acc_code::f(); + do + { + auto tmp = strip_rec(pos, rem, missing); + tmp.append_or(std::move(res)); + std::swap(tmp, res); + pos -= pos->size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::Fin: + if (missing && (pos[-1].mark & rem)) + return acc_cond::acc_code::t(); + return acc_cond::acc_code::fin(pos[-1].mark.strip(rem)); + case acc_cond::acc_op::Inf: + if (missing && (pos[-1].mark & rem)) + return acc_cond::acc_code::f(); + return acc_cond::acc_code::inf(pos[-1].mark.strip(rem)); + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + return {}; + } + SPOT_UNREACHABLE(); + return {}; + } + } + + acc_cond::acc_code + acc_cond::acc_code::strip(acc_cond::mark_t rem, bool missing) const + { + if (is_true() || is_false()) + return *this; + return strip_rec(&back(), rem, missing); + } + + acc_cond::mark_t + acc_cond::acc_code::used_sets() const + { + if (is_true() || is_false()) + return 0U; + acc_cond::mark_t used_in_cond = 0U; + auto pos = &back(); + auto end = &front(); + while (pos > end) + { + switch (pos->op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + used_in_cond |= pos[-1].mark; + pos -= 2; + break; + } + } + return used_in_cond; + } + std::ostream& operator<<(std::ostream& os, const spot::acc_cond::acc_code& code) { diff --git a/src/tgba/acc.hh b/src/tgba/acc.hh index 83ccd514c..76b4ad70a 100644 --- a/src/tgba/acc.hh +++ b/src/tgba/acc.hh @@ -145,6 +145,29 @@ namespace spot return id ^ r.id; } + mark_t strip(mark_t y) const + { + // strip every bit of id that is marked in y + // 100101110100.strip( + // 001011001000) + // == 10 1 11 100 + // == 10111100 + + auto xv = id; // 100101110100 + auto yv = y.id; // 001011001000 + + while (yv && xv) + { + // Mask for everything after the last 1 in y + auto rm = (~yv) & (yv - 1); // 000000000111 + // Mask for everything before the last 1 in y + auto lm = ~(yv ^ (yv - 1)); // 111111110000 + xv = ((xv & lm) >> 1) | (xv & rm); + yv = (yv & lm) >> 1; + } + return xv; + } + // Number of bits sets. unsigned count() const { @@ -321,6 +344,61 @@ namespace spot && (*this)[s - 1].op == acc_op::Fin && (*this)[s - 2].mark == 0U; } + static acc_code f() + { + acc_code res; + res.resize(2); + res[0].mark = 0U; + res[1].op = acc_op::Fin; + res[1].size = 1; + return res; + } + + static acc_code t() + { + return {}; + } + + static acc_code fin(mark_t m) + { + acc_code res; + res.resize(2); + res[0].mark = m; + res[1].op = acc_op::Fin; + res[1].size = 1; + return res; + } + + static acc_code fin_neg(mark_t m) + { + acc_code res; + res.resize(2); + res[0].mark = m; + res[1].op = acc_op::FinNeg; + res[1].size = 1; + return res; + } + + static acc_code inf(mark_t m) + { + acc_code res; + res.resize(2); + res[0].mark = m; + res[1].op = acc_op::Inf; + res[1].size = 1; + return res; + } + + static acc_code inf_neg(mark_t m) + { + acc_code res; + res.resize(2); + res[0].mark = m; + res[1].op = acc_op::InfNeg; + res[1].size = 1; + return res; + } + void append_and(acc_code&& r) { if (is_true() || r.is_false()) @@ -562,6 +640,24 @@ namespace spot acc_code complement() const; + // Remove all the acceptance sets in rem. + // + // If MISSING is set, the acceptance sets are assumed to be + // missing from the automaton, and the acceptance is updated to + // reflect this. For instance (Inf(1)&Inf(2))|Fin(3) will + // become Fin(3) if we remove 2 because it is missing from this + // automaton, because there is no way to fulfill Inf(1)&Inf(2) + // in this case. So essentially MISSING causes Inf(rem) to + // become f, and Fin(rem) to become t. + // + // If MISSING is unset, Inf(rem) become t while Fin(rem) become + // f. Removing 2 from (Inf(1)&Inf(2))|Fin(3) would then give + // Inf(1)|Fin(3). + acc_code strip(acc_cond::mark_t rem, bool missing) const; + + // Return the set of sets appearing in the condition. + acc_cond::mark_t used_sets() const; + SPOT_API friend std::ostream& operator<<(std::ostream& os, const acc_code& code); }; @@ -609,26 +705,25 @@ namespace spot (s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets()); } + 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; - acc_code primitive(mark_t mark, acc_op op) const - { - acc_word w1; - w1.mark = mark; - acc_word w2; - w2.op = op; - w2.size = 1; - acc_code c; - c.push_back(w1); - c.push_back(w2); - return c; - } - public: acc_code inf(mark_t mark) const { - return primitive(mark, acc_op::Inf); + return acc_code::inf(mark); } acc_code inf(std::initializer_list vals) const @@ -638,7 +733,7 @@ namespace spot acc_code inf_neg(mark_t mark) const { - return primitive(mark, acc_op::InfNeg); + return acc_code::inf_neg(mark); } acc_code inf_neg(std::initializer_list vals) const @@ -648,7 +743,7 @@ namespace spot acc_code fin(mark_t mark) const { - return primitive(mark, acc_op::Fin); + return acc_code::fin(mark); } acc_code fin(std::initializer_list vals) const @@ -658,7 +753,7 @@ namespace spot acc_code fin_neg(mark_t mark) const { - return primitive(mark, acc_op::FinNeg); + return acc_code::fin_neg(mark); } acc_code fin_neg(std::initializer_list vals) const @@ -795,30 +890,6 @@ namespace spot return u; } - mark_t strip(mark_t x, mark_t y) const - { - // strip every bit of x that is marked in y - // strip(100101110100, - // 001011001000) - // == 10 1 11 100 - // == 10111100 - - auto xv = x.id; // 100101110100 - auto yv = y.id; // 001011001000 - - while (yv && xv) - { - // Mask for everything after the last 1 in y - auto rm = (~yv) & (yv - 1); // 000000000111 - // Mask for everything before the last 1 in y - auto lm = ~(yv ^ (yv - 1)); // 111111110000 - xv = ((xv & lm) >> 1) | (xv & rm); - yv = (yv & lm) >> 1; - } - - return xv; - } - protected: mark_t::value_t mark_(unsigned u) const { diff --git a/src/tgbaalgos/cleanacc.cc b/src/tgbaalgos/cleanacc.cc index 15afecc16..cdfd776ba 100644 --- a/src/tgbaalgos/cleanacc.cc +++ b/src/tgbaalgos/cleanacc.cc @@ -21,61 +21,6 @@ namespace spot { - namespace - { - acc_cond::acc_code strip(const acc_cond& acc, - const acc_cond::acc_word* pos, - acc_cond::mark_t useless) - { - auto start = pos - pos->size; - switch (pos->op) - { - case acc_cond::acc_op::And: - { - --pos; - acc_cond::acc_code res; - do - { - auto tmp = strip(acc, pos, useless); - tmp.append_and(std::move(res)); - std::swap(tmp, res); - pos -= pos->size + 1; - } - while (pos > start); - return res; - } - case acc_cond::acc_op::Or: - { - --pos; - acc_cond::acc_code res = acc.fin(0); // f - do - { - auto tmp = strip(acc, pos, useless); - tmp.append_or(std::move(res)); - std::swap(tmp, res); - pos -= pos->size + 1; - } - while (pos > start); - return res; - } - case acc_cond::acc_op::Fin: - if (pos[-1].mark & useless) - return acc.inf(0U); // t - return acc.fin(acc.strip(pos[-1].mark, useless)); - case acc_cond::acc_op::Inf: - if (pos[-1].mark & useless) - return acc.fin(0U); // f - return acc.inf(acc.strip(pos[-1].mark, useless)); - case acc_cond::acc_op::FinNeg: - case acc_cond::acc_op::InfNeg: - SPOT_UNREACHABLE(); - return acc_cond::acc_code{}; - } - SPOT_UNREACHABLE(); - return acc_cond::acc_code{}; - } - } - void cleanup_acceptance(tgba_digraph_ptr& aut) { auto& acc = aut->acc(); @@ -83,29 +28,7 @@ namespace spot return; auto& c = aut->get_acceptance(); - acc_cond::mark_t used_in_cond = 0U; - if (!c.is_true()) - { - auto pos = &c.back(); - auto end = &c.front(); - while (pos > end) - { - switch (pos->op) - { - case acc_cond::acc_op::And: - case acc_cond::acc_op::Or: - --pos; - break; - case acc_cond::acc_op::Fin: - case acc_cond::acc_op::Inf: - case acc_cond::acc_op::FinNeg: - case acc_cond::acc_op::InfNeg: - used_in_cond |= pos[-1].mark; - pos -= 2; - break; - } - } - } + acc_cond::mark_t used_in_cond = c.used_sets(); acc_cond::mark_t used_in_aut = 0U; for (auto& t: aut->transitions()) @@ -120,16 +43,10 @@ namespace spot // Remove useless marks from the automaton for (auto& t: aut->transitions()) - t.acc = acc.strip(t.acc, useless); + t.acc = t.acc.strip(useless); // Remove useless marks from the acceptance condition - acc_cond::acc_code newc; - if (c.is_true() || c.is_false()) - newc = c; - else - newc = strip(acc, &c.back(), useless); - - aut->set_acceptance(useful.count(), newc); + aut->set_acceptance(useful.count(), c.strip(useless, true)); } } diff --git a/src/tgbaalgos/mask.cc b/src/tgbaalgos/mask.cc index 3967130d4..387ca59c4 100644 --- a/src/tgbaalgos/mask.cc +++ b/src/tgbaalgos/mask.cc @@ -24,14 +24,14 @@ namespace spot tgba_digraph_ptr mask_acc_sets(const const_tgba_digraph_ptr& in, acc_cond::mark_t to_remove) { - auto& inacc = in->acc(); auto res = make_tgba_digraph(in->get_dict()); res->copy_ap_of(in); res->prop_copy(in, { true, false, true, true }); - unsigned na = inacc.num_sets(); + unsigned na = in->acc().num_sets(); unsigned tr = to_remove.count(); assert(tr <= na); - res->set_generalized_buchi(na - tr); + res->set_acceptance(na - tr, + in->get_acceptance().strip(to_remove, false)); transform_accessible(in, res, [&](unsigned, bdd& cond, acc_cond::mark_t& acc, @@ -40,7 +40,7 @@ namespace spot if (acc & to_remove) cond = bddfalse; else - acc = inacc.strip(acc, to_remove); + acc = acc.strip(to_remove); }); return res; } diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc index fb2b5015f..8ad356225 100644 --- a/src/tgbaalgos/sccfilter.cc +++ b/src/tgbaalgos/sccfilter.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de -// Recherche et Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire +// de Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -240,7 +240,7 @@ namespace spot if (!this->si->is_accepting_scc(u)) acc = 0U; else - acc = this->si->get_aut()->acc().strip(acc, strip_[u]); + acc = acc.strip(strip_[u]); } return filtered_trans{keep, cond, acc}; } diff --git a/src/tgbatest/acc.cc b/src/tgbatest/acc.cc index 37d12b116..f0ed5ba31 100644 --- a/src/tgbatest/acc.cc +++ b/src/tgbatest/acc.cc @@ -103,7 +103,7 @@ int main() for (auto& v: s) { check(ac, v); - check(ac, ac.strip(v, u)); + check(ac, v.strip(u)); } diff --git a/src/tgbatest/maskacc.test b/src/tgbatest/maskacc.test index 586c60a93..f449df7e2 100755 --- a/src/tgbatest/maskacc.test +++ b/src/tgbatest/maskacc.test @@ -111,6 +111,51 @@ diff output expect3 run 0 ../../bin/autfilt --mask-acc=0 --mask-acc=1 input1 -H >output diff output expect3 +cat >input4 <expect4 <output +diff output expect4 + # Errors run 2 ../../bin/autfilt --mask-acc=a3 input1 run 2 ../../bin/autfilt --mask-acc=3-2 input1