diff --git a/NEWS b/NEWS index 67278dc05..e056b813d 100644 --- a/NEWS +++ b/NEWS @@ -58,7 +58,7 @@ New in spot 2.8.5.dev (not yet released) parity_min_even(n) = parity_min(false, n) - partial_degeneralize() is a new function performing partial - degeneralization to get rid of conjunction of Inf terms in + degeneralization to get rid of conjunctions of Inf terms in acceptance conditions. - simplify_acceptance_here() and simplify_acceptance() learned to @@ -68,6 +68,16 @@ New in spot 2.8.5.dev (not yet released) and the automaton is adjusted to that i also appears where j appeared. + - propagate_marks_vector() and propagate_marks_here() are helper + functions for propagatings marks on the automaton: ignoring + self-loop and out-of-SCC transitions, marks common to all the + input transitions of a state can be pushed to all outgoing + transitions of a state, and vice-versa. This is repeated until a + fix point is reached. propagate_marks_vector() does not modify + the automaton and returns a vector of the acc_cond::mark_t that + should be on each transition; propagate_marks_here() actually + modifies the automaton. + New in spot 2.8.5 (2020-01-04) Bugs fixed: diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 0c9951e65..29743fbab 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2019 Laboratoire de Recherche +// Copyright (C) 2012-2020 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -122,7 +122,7 @@ namespace spot unsigned n = a->num_states(); acc_cond::mark_t all = a_->acc().all_sets(); // slot 2 will hold acceptance mark that are common to the - // incoming transitions of each state. For know with all + // incoming transitions of each state. For now with all // marks if there is some incoming edge. The next loop will // constrain this value. for (auto& e: a_->edges()) @@ -176,36 +176,59 @@ namespace spot // Order of accepting sets (for one SCC) class acc_order final { + std::vector> found_; std::vector order_; - acc_cond::mark_t found_; public: - unsigned - next_level(int slevel, acc_cond::mark_t set, bool skip_levels) + acc_order(acc_cond::mark_t all) { - // Update the order with any new set we discover - if (auto newsets = set - found_) - { - newsets.fill(std::back_inserter(order_)); - found_ |= newsets; - } + unsigned count = all.count(); + found_.emplace_back(all, count); + order_.insert(order_.begin(), count, 0); + } - unsigned next = slevel; - while (next < order_.size() && set.has(order_[next])) + unsigned + next_level(unsigned slevel, acc_cond::mark_t set) + { + unsigned last = order_.size(); + if (last == 0) + return slevel; + unsigned index = order_[slevel]; + + while (slevel < last + && (found_[index].first & set) == found_[index].first) + slevel += found_[index++].second; + if (slevel == last) + return slevel; + if (acc_cond::mark_t match = (found_[index].first & set)) { - ++next; - if (!skip_levels) - break; + unsigned matchsize = match.count(); + found_[index].first -= match; + found_[index].second -= matchsize; + found_.emplace(found_.begin() + index, match, matchsize); + slevel += matchsize; + // update order_ + unsigned opos = 0; + unsigned fpos = 0; + for (auto& p: found_) + { + for (unsigned n = 0; n < p.second; ++n) + order_[opos++] = fpos; + ++fpos; + } } - return next; + return slevel; } void print(int scc) { std::cout << "Order_" << scc << ":\t"; + for (auto i: found_) + std::cout << i.first << ' '; + std::cout << " // "; for (auto i: order_) - std::cout << i << ", "; + std::cout << i << ' '; std::cout << '\n'; } }; @@ -213,27 +236,26 @@ namespace spot // Accepting order for each SCC class scc_orders final { - std::map orders_; - bool skip_levels_; + std::vector orders_; public: - scc_orders(bool skip_levels): - skip_levels_(skip_levels) + scc_orders(acc_cond::mark_t all, unsigned scc_count) + : orders_(scc_count, acc_order(all)) { } unsigned next_level(int scc, int slevel, acc_cond::mark_t set) { - return orders_[scc].next_level(slevel, set, skip_levels_); + return orders_[scc].next_level(slevel, set); } void print() { - std::map::iterator i; - for (i = orders_.begin(); i != orders_.end(); i++) - i->second.print(i->first); + unsigned sz = orders_.size(); + for (unsigned i = 0; i < sz; ++i) + orders_[i].print(i); } }; @@ -348,9 +370,6 @@ namespace spot order.emplace_back(i - 1); } - // Initialize scc_orders - scc_orders orders(skip_levels); - // and vice-versa. ds2num_map ds2num; @@ -370,6 +389,11 @@ namespace spot ? std::make_unique(a, scc_info_options::NONE) : nullptr; + // Initialize scc_orders + std::unique_ptr orders = use_cust_acc_orders + ? std::make_unique(a->acc().all_sets(), m->scc_count()) + : nullptr; + // Cache for common outgoing/incoming acceptances. inout_acc inout(a, m.get()); @@ -390,7 +414,7 @@ namespace spot { auto set = inout.common_inout_acc(s.first); if (SPOT_UNLIKELY(use_cust_acc_orders)) - s.second = orders.next_level(m->initial(), s.second, set); + s.second = orders->next_level(m->initial(), s.second, set); else while (s.second < order.size() && set.has(order[s.second])) { @@ -589,7 +613,7 @@ namespace spot // for this scc if (use_cust_acc_orders) { - d.second = orders.next_level(scc, next, acc); + d.second = orders->next_level(scc, next, acc); } // Else compute level according the global acc order else @@ -628,7 +652,7 @@ namespace spot // In case we are building a TBA is_acc has to be // set differently for each edge, and - // we do not need to stay use final level. + // we do not need to stay on final level. if (!want_sba) { is_acc = d.second == order.size(); @@ -640,7 +664,7 @@ namespace spot { if (use_cust_acc_orders) { - d.second = orders.next_level(scc, d.second, acc); + d.second = orders->next_level(scc, d.second, acc); } else { @@ -670,7 +694,7 @@ namespace spot for (auto i: order) std::cout << i << ", "; std::cout << '\n'; - orders.print(); + orders->print(); #endif res->merge_edges(); if (remove_extra_scc) @@ -808,21 +832,40 @@ namespace spot update_acc_for_partial_degen(acc, todegen, tostrip, degenmark); res->set_acceptance(acc); - std::vector order; - for (unsigned set: todegen.sets()) - order.push_back(set); - - //auto* names = new std::vector; - //res->set_named_prop("state-names", names); + // auto* names = new std::vector; + // res->set_named_prop("state-names", names); auto orig_states = new std::vector(); auto levels = new std::vector(); - orig_states->reserve(a->num_states()); // likely more are needed. + unsigned ns = a->num_states(); + orig_states->reserve(ns); // likely more are needed. levels->reserve(a->num_states()); res->set_named_prop("original-states", orig_states); res->set_named_prop("degen-levels", levels); scc_info si_orig(a, scc_info_options::NONE); + auto marks = propagate_marks_vector(a, &si_orig); + + std::vector highest_level(ns, 0); + // Compute the marks that are common to all incoming or all + // outgoing transitions of each state, ignoring self-loops and + // out-of-SCC transitions. Note that because + // propagate_marks_verctor() has been used, the intersection + // of all incoming marks is equal to the intersection of all + // outgoing marks unless the state has no predecessor or no + // successor. We take the outgoing marks because states without + // successor are useless (but states without predecessors are not). + std::vector inout(ns, todegen); + for (auto& e: a->edges()) + if (e.src != e.dst && si_orig.scc_of(e.src) == si_orig.scc_of(e.dst)) + { + unsigned idx = a->edge_number(e); + inout[e.src] &= marks[idx]; + } + + scc_orders orders(todegen, si_orig.scc_count()); + unsigned ordersize = todegen.count(); + // degen_states -> new state numbers ds2num_map ds2num; @@ -834,25 +877,41 @@ namespace spot if (di != ds2num.end()) return di->second; + highest_level[ds.first] = + std::max(highest_level[ds.first], ds.second); + unsigned ns = res->new_state(); ds2num[ds] = ns; todo.emplace_back(ds); - //std::ostringstream os; - //os << ds.first << ',' << ds.second; - //names->push_back(os.str()); + // std::ostringstream os; + // os << ds.first << ',' << ds.second; + // names->push_back(os.str()); assert(ns == orig_states->size()); orig_states->emplace_back(ds.first); levels->emplace_back(ds.second); return ns; }; - degen_state s(a->get_init_state_number(), 0); + + unsigned init = a->get_init_state_number(); + degen_state s(init, 0); + // The initial level can be anything. As a heuristic, pretend we + // have just seen the acceptance condition common to incoming + // edges. + s.second = orders.next_level(si_orig.scc_of(init), 0, inout[init]); + if (s.second == ordersize) + s.second = 0; + new_state(s); + // A list of edges are that "all accepting" and whose destination + // could be redirected to a higher level. + std::vector allaccedges; + while (!todo.empty()) { - s = todo.front(); - todo.pop_front(); + s = todo.back(); + todo.pop_back(); int src = ds2num[s]; unsigned slevel = s.second; @@ -860,22 +919,39 @@ namespace spot unsigned scc_src = si_orig.scc_of(orig_src); for (auto& e: a->out(orig_src)) { + bool saveedge = false; unsigned nextlvl = slevel; acc_cond::mark_t accepting = {}; if (si_orig.scc_of(e.dst) == scc_src) { - while (nextlvl < order.size() && e.acc.has(order[nextlvl])) - ++nextlvl; - - if (nextlvl == order.size()) + unsigned idx = a->edge_number(e); + acc_cond::mark_t acc = marks[idx] & todegen; + nextlvl = orders.next_level(scc_src, nextlvl, acc); + if (nextlvl == ordersize) { accepting = degenmark; nextlvl = 0; - - if ((e.acc & todegen) != todegen) - while (nextlvl < order.size() - && e.acc.has(order[nextlvl])) - ++nextlvl; + if ((acc & todegen) != todegen) + { + nextlvl = orders.next_level(scc_src, nextlvl, acc); + } + else + { + // Because we have seen all sets on this + // transition, we can jump to any level we + // like. As a heuristic, let's jump to the + // highest existing level. + nextlvl = highest_level[e.dst]; + if (nextlvl == 0 // probably a new state -> + // use inout for now + && inout[e.dst] != todegen) + nextlvl = orders.next_level(scc_src, nextlvl, + inout[e.dst]); + // It's possible that we have not yet seen the + // highest level yet, so let's save this edge + // and revisit this issue at the end. + saveedge = true; + } } accepting |= e.acc.strip(tostrip); } @@ -886,13 +962,87 @@ namespace spot degen_state ds_dst(e.dst, nextlvl); unsigned dst = new_state(ds_dst); - res->new_edge(src, dst, e.cond, accepting); + unsigned idx = res->new_edge(src, dst, e.cond, accepting); + if (saveedge) + allaccedges.push_back(idx); } } - + // Raise the destination of the "all-accepting" edges to the + // highest existing level. + auto& ev = res->edge_vector(); + for (unsigned idx: allaccedges) + { + unsigned dst = ev[idx].dst; + unsigned orig_dst = (*orig_states)[dst]; + unsigned hl = highest_level[orig_dst]; + ev[idx].dst = ds2num[degen_state{orig_dst, hl}]; + } + //orders.print(); res->merge_edges(); keep_bottommost_copies(res, si_orig, orig_states); return res; } + + std::vector + propagate_marks_vector(const const_twa_graph_ptr& aut, + scc_info* si) + { + bool own_si = true; + if (si) + own_si = false; + else + si = new scc_info(aut); + + unsigned ns = aut->num_states(); + acc_cond::mark_t allm = aut->acc().all_sets(); + unsigned es = aut->edge_vector().size(); + std::vector marks(es, acc_cond::mark_t{}); + const auto& edges = aut->edge_vector(); + for (unsigned e = 1; e < es; ++e) + marks[e] = edges[e].acc; + + std::vector common_in(ns, allm); + std::vector common_out(ns, allm); + + for (;;) + { + bool changed = false; + for (auto& e: aut->edges()) + if (e.src != e.dst && si->scc_of(e.src) == si->scc_of(e.dst)) + { + unsigned idx = aut->edge_number(e); + common_in[e.dst] &= marks[idx]; + common_out[e.src] &= marks[idx]; + } + for (auto& e: aut->edges()) + if (e.src != e.dst && si->scc_of(e.src) == si->scc_of(e.dst)) + { + unsigned idx = aut->edge_number(e); + auto acc = marks[idx] | common_in[e.src] | common_out[e.dst]; + if (acc != marks[idx]) + { + marks[idx] = acc; + changed = true; + } + } + if (!changed) + break; + std::fill(common_in.begin(), common_in.end(), allm); + std::fill(common_out.begin(), common_out.end(), allm); + } + if (own_si) + delete si; + return marks; + } + + void propagate_marks_here(twa_graph_ptr& aut, scc_info* si) + { + auto marks = propagate_marks_vector(aut, si); + for (auto& e: aut->edges()) + { + unsigned idx = aut->edge_number(e); + e.acc = marks[idx]; + } + } } diff --git a/spot/twaalgos/degen.hh b/spot/twaalgos/degen.hh index 7caa4ee21..f3a6f3e30 100644 --- a/spot/twaalgos/degen.hh +++ b/spot/twaalgos/degen.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2015, 2017-2019 Laboratoire de +// Copyright (C) 2012-2015, 2017-2020 Laboratoire de // Recherche et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -23,6 +23,8 @@ namespace spot { + class scc_info; + /// \ingroup twa_acc_transform /// \brief Degeneralize a spot::tgba into an equivalent sba with /// only one acceptance condition. @@ -101,4 +103,29 @@ namespace spot SPOT_API twa_graph_ptr partial_degeneralize(const const_twa_graph_ptr& a, acc_cond::mark_t todegen); + + /// \ingroup twa_algorithms + /// \brief Propagate marks around the automaton + /// + /// For each state of the automaton, marks that are common + /// to all input transitions will be pushed on the outgoing + /// transitions, and marks that are common to all outgoing + /// transitions will be pulled to the input transitions. + /// This considers only transitions that are not self-loops + /// and that belong to some SCC. If an scc_info has already + /// been built, pass it as \a si to avoid building it again. + /// + /// Two variants of the algorithm are provided. One modifies + /// the automaton in place; the second returns a vector of marks + /// indexed by transition numbers. + /// + /// @{ + SPOT_API std::vector + propagate_marks_vector(const const_twa_graph_ptr& aut, + scc_info* si = nullptr); + + SPOT_API void + propagate_marks_here(twa_graph_ptr& aut, + scc_info* si = nullptr); + /// @} } diff --git a/tests/python/pdegen.py b/tests/python/pdegen.py index 02f7ed0c8..d8771d9c4 100644 --- a/tests/python/pdegen.py +++ b/tests/python/pdegen.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2019 Laboratoire de Recherche et Développement de +# Copyright (C) 2019, 2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -80,10 +80,10 @@ Acceptance: 2 Fin(0) | Inf(1) properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 0 "2#0" +[0] 1 +State: 1 "0#0" {0 1} [0] 2 -State: 1 "1#0" -[0] 2 -State: 2 "0#1" {0 1} +State: 2 "1#0" {1} [0] 1 --END--""" @@ -96,3 +96,65 @@ dd = spot.partial_degeneralize(d, []) assert dd.equivalent_to(d) assert dd.num_states() == 1 assert str(dd.get_acceptance()) == 'Inf(1) & Fin(0)' + +aut5 = spot.automaton(""" HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" +acc-name: generalized-Buchi 10 Acceptance: 10 +Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4)&Inf(5)&Inf(6)&Inf(7)&Inf(8)&Inf(9) +properties: trans-labels explicit-labels trans-acc deterministic --BODY-- +State: 0 [0&!1&2] 3 {2 4 9} State: 1 [!0&1&2] 5 {2 6 7 8} [!0&!1&!2] 0 {2} +State: 2 [0&!1&2] 3 {1 4 9} State: 3 [0&!1&2] 4 {0 1 5 9} State: 4 [!0&!1&2] 1 +{7} [0&!1&2] 6 {1 2} State: 5 [!0&1&2] 7 {3 5} State: 6 [!0&!1&2] 2 {1 3 5} +State: 7 [0&!1&!2] 0 {4 7} --END--""") + +daut5 = spot.degeneralize_tba(aut5) +assert daut5.equivalent_to(aut5) +sets = list(range(aut5.num_sets())) +pdaut5 = spot.partial_degeneralize(aut5, sets) +assert pdaut5.equivalent_to(aut5) +assert daut5.num_states() == 10 +assert pdaut5.num_states() == 8 + +aut6 = spot.automaton("""HOA: v1 States: 6 Start: 0 AP: 3 "p0" "p1" "p2" +acc-name: generalized-Buchi 3 Acceptance: 3 Inf(0)&Inf(1)&Inf(2) properties: +trans-labels explicit-labels trans-acc deterministic --BODY-- State: 0 +[0&!1&!2] 4 {1} State: 1 [!0&!1&!2] 2 {0 1} State: 2 [!0&1&2] 0 {1} State: 3 +[0&1&!2] 5 {1} State: 4 [!0&1&!2] 0 {1 2} [0&!1&!2] 3 {0} State: 5 [!0&1&2] 1 +--END-- """) +daut6 = spot.degeneralize_tba(aut6) +assert daut6.equivalent_to(aut6) +sets = list(range(aut6.num_sets())) +pdaut6 = spot.partial_degeneralize(aut6, sets) +assert pdaut6.equivalent_to(aut6) +assert daut6.num_states() == 8 +assert pdaut6.num_states() == 8 + + +aut7 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" +acc-name: generalized-Buchi 4 Acceptance: 4 Inf(0)&Inf(1)&Inf(2)&Inf(3) +properties: trans-labels explicit-labels trans-acc deterministic --BODY-- +State: 0 [0&!1&2] 1 {2 3} State: 1 [0&!1&2] 0 {0 2} [0&!1&!2] 6 State: 2 +[0&1&2] 0 [!0&!1&2] 5 [!0&1&!2] 6 {1} State: 3 [0&!1&2] 5 [0&!1&!2] 6 State: 4 +[!0&!1&!2] 3 State: 5 [0&1&!2] 0 [!0&1&2] 7 State: 6 [0&1&2] 2 {1} State: 7 +[!0&!1&2] 0 {0} [!0&1&!2] 4 --END--""") +daut7 = spot.degeneralize_tba(aut7) +assert daut7.equivalent_to(aut7) +sets = list(range(aut7.num_sets())) +pdaut7 = spot.partial_degeneralize(aut7, sets) +assert pdaut7.equivalent_to(aut7) +assert daut7.num_states() == 11 +assert pdaut7.num_states() == 10 + +aut8 = spot.automaton("""HOA: v1 States: 8 Start: 0 AP: 3 "p0" "p1" "p2" +acc-name: generalized-Buchi 5 Acceptance: 5 Inf(0)&Inf(1)&Inf(2)&Inf(3)&Inf(4) +properties: trans-labels explicit-labels trans-acc deterministic --BODY-- +State: 0 [!0&1&!2] 7 {0} State: 1 [!0&1&2] 1 {4} [0&!1&2] 6 {1 2} State: 2 +[!0&!1&2] 3 {1 2} [0&1&2] 5 State: 3 [0&1&2] 2 {2} State: 4 [!0&!1&!2] 3 State: +5 [!0&1&!2] 0 {1 3} State: 6 [0&1&2] 4 [0&1&!2] 6 State: 7 [!0&!1&!2] 1 +--END--""") +daut8 = spot.degeneralize_tba(aut8) +assert daut8.equivalent_to(aut8) +sets = list(range(aut8.num_sets())) +pdaut8 = spot.partial_degeneralize(aut8, sets) +assert pdaut8.equivalent_to(aut8) +assert daut8.num_states() == 22 +assert pdaut8.num_states() == 9