From 37f3154f1d376cd38ac23b338700b9e0606ec6bf Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 24 Jul 2017 16:13:56 +0200 Subject: [PATCH] degen, sbacc: merge accepting sinks Fixes #276. * spot/twaalgos/sbacc.cc, spot/twaalgos/degen.cc: Detect accepting sinks, and merge them. * tests/python/dualize.py: Adjust. * tests/python/sbacc.py: More test cases. --- NEWS | 3 ++ spot/twaalgos/degen.cc | 87 ++++++++++++++++++++++++++++------------- spot/twaalgos/sbacc.cc | 28 ++++++++++++- tests/python/dualize.py | 16 +++++--- tests/python/sbacc.py | 70 +++++++++++++++++++++++++++++++++ 5 files changed, 170 insertions(+), 34 deletions(-) diff --git a/NEWS b/NEWS index 816b03c39..cb643390b 100644 --- a/NEWS +++ b/NEWS @@ -150,6 +150,9 @@ New in spot 2.3.5.dev (not yet released) - spot::sbacc() is now able to work on alternating automata. + - spot::sbacc() and spot::degeneralize() learned to merge + accepting sinks. + - If the SPOT_BDD_TRACE envorinment variable is set, statistics about BDD garbage collection and table resizing are shown. diff --git a/spot/twaalgos/degen.cc b/spot/twaalgos/degen.cc index 235c635a9..c2c6d6ed8 100644 --- a/spot/twaalgos/degen.cc +++ b/spot/twaalgos/degen.cc @@ -50,7 +50,8 @@ namespace spot }; // Associate the degeneralized state to its number. - typedef std::unordered_map ds2num_map; + typedef std::unordered_map ds2num_map; // Queue of state to be processed. typedef std::deque queue_t; @@ -60,14 +61,16 @@ namespace spot class inout_acc final { const_twa_graph_ptr a_; - typedef std::tuple cache_entry; + typedef std::tuple cache_entry; // is true state std::vector cache_; + unsigned last_true_state_; const scc_info* sm_; - unsigned scc_of(unsigned s) + unsigned scc_of(unsigned s) const { return sm_ ? sm_->scc_of(s) : 0; } @@ -78,6 +81,7 @@ namespace spot acc_cond::mark_t common = a_->acc().all_sets(); acc_cond::mark_t union_ = 0U; bool has_acc_self_loop = false; + bool is_true_state = false; bool seen = false; for (auto& t: a_->out(s)) { @@ -91,7 +95,15 @@ namespace spot std::get<2>(cache_[d]) &= t.acc; // an accepting self-loop? - has_acc_self_loop |= (t.dst == s) && a_->acc().accepting(t.acc); + if ((t.dst == s) && a_->acc().accepting(t.acc)) + { + has_acc_self_loop = true; + if (t.cond == bddtrue) + { + is_true_state = true; + last_true_state_ = s; + } + } seen = true; } if (!seen) @@ -99,6 +111,7 @@ namespace spot std::get<0>(cache_[s]) = common; std::get<1>(cache_[s]) = union_; std::get<3>(cache_[s]) = has_acc_self_loop; + std::get<4>(cache_[s]) = is_true_state; } public: @@ -109,7 +122,7 @@ namespace spot 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 - // marks if there is some incoming edge. The nextx loop will + // marks if there is some incoming edge. The next loop will // constrain this value. for (auto& e: a_->edges()) if (scc_of(e.src) == scc_of(e.dst)) @@ -121,32 +134,42 @@ namespace spot } // Intersection of all outgoing acceptance sets - acc_cond::mark_t common_out_acc(unsigned s) + acc_cond::mark_t common_out_acc(unsigned s) const { assert(s < cache_.size()); return std::get<0>(cache_[s]); } // Union of all outgoing acceptance sets - acc_cond::mark_t union_out_acc(unsigned s) + acc_cond::mark_t union_out_acc(unsigned s) const { assert(s < cache_.size()); return std::get<1>(cache_[s]); } // Intersection of all incoming acceptance sets - acc_cond::mark_t common_inout_acc(unsigned s) + acc_cond::mark_t common_inout_acc(unsigned s) const { assert(s < cache_.size()); return std::get<2>(cache_[s]); } - // Has an accepting self-loop - bool has_acc_selfloop(unsigned s) + bool has_acc_selfloop(unsigned s) const { assert(s < cache_.size()); return std::get<3>(cache_[s]); } + + bool is_true_state(unsigned s) const + { + assert(s < cache_.size()); + return std::get<4>(cache_[s]); + } + + unsigned last_true_state() const + { + return last_true_state_; + } }; // Order of accepting sets (for one SCC) @@ -253,8 +276,6 @@ namespace spot // denote accepting states. std::vector order; { - // FIXME: revisit this comment once everything compiles again. - // // The order is arbitrary, but it turns out that using emplace_back // instead of push_front often gives better results because // acceptance sets at the beginning if the cycle are more often @@ -280,10 +301,6 @@ namespace spot typedef std::map tr_cache_t; tr_cache_t tr_cache; - // Read this early, because it might create a state if the - // automaton is empty. - degen_state s(a->get_init_state_number(), 0); - // State->level cache std::vector> lvl_cache(a->num_states()); @@ -297,6 +314,8 @@ namespace spot queue_t todo; + degen_state s(a->get_init_state_number(), 0); + // As a heuristic for building SBA, if the initial state has at // least one accepting self-loop, start the degeneralization on // the accepting level. @@ -323,11 +342,30 @@ namespace spot s.second = 0; } - auto new_state = [&](degen_state& ds) + auto new_state = [&](degen_state ds) { + // Merge all true states into a single one. + bool ts = inout.is_true_state(ds.first); + if (ts) + ds = {inout.last_true_state(), 0U}; + + auto di = ds2num.find(ds); + if (di != ds2num.end()) + return di->second; + unsigned ns = res->new_state(); ds2num[ds] = ns; - todo.emplace_back(ds); + if (ts) + { + res->new_acc_edge(ns, ns, bddtrue, true); + // As we do not process all outgoing transition of + // ds.first, it is possible that a non-deterministic + // automaton becomes deterministic. + if (res->prop_universal().is_false()) + res->prop_universal(trival::maybe()); + } + else + todo.emplace_back(ds); assert(ns == orig_states->size()); orig_states->emplace_back(ds.first); @@ -555,12 +593,7 @@ namespace spot } // Have we already seen this destination? - int dest; - ds2num_map::const_iterator di = ds2num.find(d); - if (di != ds2num.end()) - dest = di->second; - else - dest = new_state(d); + int dest = new_state(d); unsigned& t = tr_cache[dest * 2 + is_acc]; diff --git a/spot/twaalgos/sbacc.cc b/spot/twaalgos/sbacc.cc index 271a30d96..59701abdb 100644 --- a/spot/twaalgos/sbacc.cc +++ b/spot/twaalgos/sbacc.cc @@ -52,12 +52,22 @@ namespace spot std::vector common_out(ns, all); // Marks that label one incoming transition from the same SCC. std::vector one_in(ns, 0U); + std::vector true_state(ns, false); + acc_cond::mark_t true_state_acc = 0U; + unsigned true_state_last; for (auto& e: old->edges()) for (unsigned d: old->univ_dests(e.dst)) if (si.scc_of(e.src) == si.scc_of(d)) { common_in[d] &= e.acc; common_out[e.src] &= e.acc; + if (e.src == e.dst && e.cond == bddtrue + && old->acc().accepting(e.acc)) + { + true_state[d] = true; + true_state_acc = e.acc; + true_state_last = e.src; + } } for (unsigned s = 0; s < ns; ++s) common_out[s] |= common_in[s]; @@ -80,13 +90,29 @@ namespace spot auto new_state = [&](unsigned state, acc_cond::mark_t m) -> unsigned { + bool ts = true_state[state]; + if (ts) + { + state = true_state_last; // Merge all true states. + m = 0U; + } pair_t x(state, m); auto p = s2n.emplace(x, 0); if (p.second) // This is a new state { unsigned s = res->new_state(); p.first->second = s; - todo.emplace_back(x, s); + if (ts) + { + res->new_edge(s, s, bddtrue, true_state_acc); + // As we do not process all outgoing transition of + // STATE, it is possible that a non-deterministic + // automaton becomes deterministic. + if (res->prop_universal().is_false()) + res->prop_universal(trival::maybe()); + } + else + todo.emplace_back(x, s); } return p.first->second; }; diff --git a/tests/python/dualize.py b/tests/python/dualize.py index 825b78139..c3601f5b3 100755 --- a/tests/python/dualize.py +++ b/tests/python/dualize.py @@ -401,16 +401,20 @@ assert h == """HOA: v1 States: 3 Start: 0 AP: 2 "a" "b" -acc-name: all -Acceptance: 0 t -properties: trans-labels explicit-labels state-acc deterministic +acc-name: co-Buchi +Acceptance: 1 Fin(0) +properties: trans-labels explicit-labels state-acc complete +properties: deterministic --BODY-- State: 0 [0&1] 1 -[!0 | !1] 2 -State: 1 +[0&!1] 2 +[!0] 2 +State: 1 {0} +[t] 1 State: 2 -[t] 2 +[0] 2 +[!0] 2 --END--""" aut = spot.automaton(""" diff --git a/tests/python/sbacc.py b/tests/python/sbacc.py index 62fdd4171..e4efeb738 100644 --- a/tests/python/sbacc.py +++ b/tests/python/sbacc.py @@ -24,3 +24,73 @@ assert not aut.prop_state_acc().is_true() aut = spot.sbacc(aut) assert aut.num_states() == 2 assert aut.prop_state_acc().is_true() + + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Inf(0) | Inf(1) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0&1] 1 +[0&!1] 2 +State: 1 +[t] 1 {0} +[0] 0 +State: 2 +[t] 2 {1} +[0] 1 +--END--""") + +s = spot.sbacc(aut) +h = s.to_str('hoa') + +assert h == """HOA: v1 +States: 2 +Start: 0 +AP: 2 "b" "a" +Acceptance: 2 Inf(0) | Inf(1) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[1] 1 +State: 1 {1} +[t] 1 +--END--""" + +aut = spot.automaton("""HOA: v1 +States: 3 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Inf(0) & Inf(1) +properties: trans-labels explicit-labels trans-acc +--BODY-- +State: 0 +[0&1] 1 +[0&!1] 2 +State: 1 +[t] 1 {0 1} +[0] 0 +State: 2 +[t] 2 {1 0} +[0] 1 +--END--""") + +d = spot.degeneralize(aut) +h = d.to_str('hoa') + +assert h == """HOA: v1 +States: 2 +Start: 0 +AP: 2 "b" "a" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels state-acc deterministic +--BODY-- +State: 0 +[1] 1 +State: 1 {0} +[t] 1 +--END--"""