diff --git a/NEWS b/NEWS index bfb264f56..b6ece1a41 100644 --- a/NEWS +++ b/NEWS @@ -93,6 +93,12 @@ New in spot 2.3.4.dev (not yet released) scc_info::common_sets_of(scc), and they are used by scc_info to classify some SCCs as rejecting more easily. + - The new function acc_code::remove() removes all the given + acceptance sets from the acceptance condition. + + - It is now possible to change an automaton acceptance condition + directly by calling twa::set_acceptance(). + Python: - The 'spot.gen' package exports the functions from libspotgen. diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 16c43b261..b1c4a0d73 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1253,10 +1253,8 @@ namespace spot SPOT_UNREACHABLE(); return {}; } - } - acc_cond::acc_code acc_cond::acc_code::complement() const { if (is_t()) @@ -1267,7 +1265,8 @@ namespace spot namespace { static acc_cond::acc_code - strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing) + strip_rec(const acc_cond::acc_word* pos, acc_cond::mark_t rem, bool missing, + bool strip) { auto start = pos - pos->sub.size; switch (pos->sub.op) @@ -1278,7 +1277,7 @@ namespace spot auto res = acc_cond::acc_code::t(); do { - auto tmp = strip_rec(pos, rem, missing) & std::move(res); + auto tmp = strip_rec(pos, rem, missing, strip) & std::move(res); std::swap(tmp, res); pos -= pos->sub.size + 1; } @@ -1291,7 +1290,7 @@ namespace spot auto res = acc_cond::acc_code::f(); do { - auto tmp = strip_rec(pos, rem, missing) | std::move(res); + auto tmp = strip_rec(pos, rem, missing, strip) | std::move(res); std::swap(tmp, res); pos -= pos->sub.size + 1; } @@ -1301,11 +1300,15 @@ namespace spot 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)); + return acc_cond::acc_code::fin(strip + ? pos[-1].mark.strip(rem) + : pos[-1].mark - 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)); + return acc_cond::acc_code::inf(strip + ? pos[-1].mark.strip(rem) + : pos[-1].mark - rem); case acc_cond::acc_op::FinNeg: case acc_cond::acc_op::InfNeg: SPOT_UNREACHABLE(); @@ -1321,7 +1324,15 @@ namespace spot { if (is_t() || is_f()) return *this; - return strip_rec(&back(), rem, missing); + return strip_rec(&back(), rem, missing, true); + } + + acc_cond::acc_code + acc_cond::acc_code::remove(acc_cond::mark_t rem, bool missing) const + { + if (is_t() || is_f()) + return *this; + return strip_rec(&back(), rem, missing, false); } acc_cond::mark_t diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index caa3000a7..55cfa1356 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -387,14 +387,16 @@ namespace spot case acc_cond::acc_op::InfNeg: case acc_cond::acc_op::Fin: case acc_cond::acc_op::FinNeg: - pos -= 2; - auto m = (*this)[pos].mark; - auto om = other[pos].mark; - if (m < om) - return true; - if (m > om) - return false; - break; + { + pos -= 2; + auto m = (*this)[pos].mark; + auto om = other[pos].mark; + if (m < om) + return true; + if (m > om) + return false; + break; + } } } return false; @@ -906,6 +908,8 @@ namespace spot // 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 remove(acc_cond::mark_t rem, bool missing) const; + // Same as remove, but also shift numbers acc_code strip(acc_cond::mark_t rem, bool missing) const; // Return the set of sets appearing in the condition. @@ -1295,6 +1299,38 @@ namespace spot return u; } + // 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_cond remove(mark_t rem, bool missing) const + { + return {num_sets(), code_.remove(rem, missing)}; + } + + // Same as remove, but also shift the set numbers + acc_cond strip(mark_t rem, bool missing) const + { + return + { num_sets() - (all_sets() & rem).count(), code_.strip(rem, missing) }; + } + + // Restrict an acceptance condition to a subset of set numbers + // that are occurring at some point. + acc_cond restrict_to(mark_t rem) const + { + return {num_sets(), code_.remove(all_sets() - rem, true)}; + } + protected: mark_t::value_t all_sets_() const { diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index cd4c9c305..52aa8104f 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -924,6 +924,14 @@ namespace spot acc_.set_acceptance(c); } + /// \brief Set the acceptance condition of the automaton. + /// + /// \param c another acceptance condition + void set_acceptance(const acc_cond& c) + { + acc_ = c; + } + /// Copy the acceptance condition of another TωA. void copy_acceptance_of(const const_twa_ptr& a) {