From 516e9536df573ab5f8bdc11f300765304e4086ac Mon Sep 17 00:00:00 2001 From: Maximilien Colange Date: Wed, 25 Jul 2018 18:49:01 +0200 Subject: [PATCH] LAR made smarter with symmetry-based degeneralization * spot/twaalgos/toparity.cc: here * spot/twa/acc.hh, spot/twa/acc.cc: compute symmetries of an acceptance condition * tests/python/accparse2.py, tests/python/toparity.py: test it --- spot/twa/acc.cc | 49 +++++++++++++++- spot/twa/acc.hh | 6 ++ spot/twaalgos/toparity.cc | 117 +++++++++++++++++++++++++++++++------- tests/python/accparse2.py | 9 ++- tests/python/toparity.py | 15 +++++ 5 files changed, 173 insertions(+), 23 deletions(-) diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 6d6f3ea51..32ddc058a 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -958,7 +958,6 @@ namespace spot const acc_cond::acc_code& rhs) { auto used = lhs.used_sets() | rhs.used_sets(); - unsigned c = used.count(); unsigned umax = used.max_set(); @@ -975,6 +974,54 @@ namespace spot } } + std::vector + acc_cond::acc_code::symmetries() const + { + auto used = used_sets(); + unsigned umax = used.max_set(); + + bdd_allocator ba; + int base = ba.allocate_variables(umax+2); + assert(base == 0); + std::vector r; + for (unsigned i = 0; r.size() < umax; ++i) + r.emplace_back(bdd_ithvar(base++)); + bdd bddcode = to_bdd_rec(&back(), &r[0]); + bdd tmp; + + std::vector res(umax); + for (unsigned x = 0; x < umax; ++x) + res[x] = x; + + for (unsigned x : used.sets()) + for (unsigned y : used.sets()) + { + if (x >= y) + continue; + if (res[x] != x) + continue; + + { + bddPair* p = bdd_newpair(); + bdd_setpair(p, x, umax + 0); + bdd_setpair(p, y, umax + 1); + tmp = bdd_replace(bddcode, p); + bdd_freepair(p); + + p = bdd_newpair(); + bdd_setpair(p, umax + 0, y); + bdd_setpair(p, umax + 1, x); + tmp = bdd_replace(tmp, p); + bdd_freepair(p); + } + + if (tmp == bddcode) + res[y] = x; + } + + return res; + } + bool acc_cond::is_parity(bool& max, bool& odd, bool equiv) const { unsigned sets = num_; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 9b1b6e20a..783b943f2 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -904,6 +904,12 @@ namespace spot trival maybe_accepting(mark_t infinitely_often, mark_t always_present) const; + // Return all symmetric marks of the condition. + // If two marks x and y are symmetric, it means that swapping them does + // not change (logically) the acc_code. + // In the returned vector, each mark points to the "root" of its symmetry + // class. + std::vector symmetries() const; // Remove all the acceptance sets in rem. // diff --git a/spot/twaalgos/toparity.cc b/spot/twaalgos/toparity.cc index e637dd43a..2af07b556 100644 --- a/spot/twaalgos/toparity.cc +++ b/spot/twaalgos/toparity.cc @@ -34,10 +34,19 @@ namespace spot { unsigned state; std::vector perm; + std::vector count; bool operator<(const lar_state& s) const { - return state == s.state ? perm < s.perm : state < s.state; + if (state == s.state) + { + if (perm == s.perm) + return count < s.count; + else + return perm < s.perm; + } + else + return state < s.state; } std::string to_string() const @@ -46,11 +55,12 @@ namespace spot s << state << " ["; for (unsigned i = 0; i != perm.size(); ++i) { - s << perm[i]; + s << perm[i] << '@' << count[i]; if (i < perm.size() - 1) - s << ','; + s << ", "; } s << ']'; + return s.str(); } }; @@ -71,10 +81,42 @@ namespace spot twa_graph_ptr run() { + auto symm = aut_->acc().get_acceptance().symmetries(); + // we need to know for each symmetry class: + // - its id + // - its elements in order (any arbitrary order will do) + // - its size + std::vector classes; + std::vector acc2class(aut_->num_sets(), -1U); + std::vector accpos(aut_->num_sets(), -1U); + for (unsigned k : aut_->acc().all_sets().sets()) + { + unsigned r = symm[k]; + if (k == r) // new class + { + acc2class[k] = classes.size(); + accpos[k] = 0; + classes.push_back({k}); + } + else + { + unsigned c = acc2class[r]; + acc2class[k] = c; + accpos[k] = classes[c].count(); + classes[c].set(k); + } + } + + // create resulting automaton res_ = make_twa_graph(aut_->get_dict()); res_->copy_ap_of(aut_); - std::deque todo; + struct stack_elem + { + unsigned num; + lar_state s; + }; + std::deque todo; auto get_state = [this, &todo](const lar_state& s) { auto it = lar2num.emplace(s, -1U); @@ -82,16 +124,21 @@ namespace spot { unsigned nb = res_->new_state(); it.first->second = nb; - todo.push_back(s); + todo.push_back({nb, s}); } return it.first->second; }; + // initial state { std::vector p0; - for (unsigned k : aut_->acc().all_sets().sets()) - p0.push_back(k); - lar_state s0{aut_->get_init_state_number(), p0}; + std::vector c0; + for (unsigned i = 0; i < classes.size(); ++i) + { + p0.push_back(i); + c0.push_back(0); + } + lar_state s0{aut_->get_init_state_number(), p0, c0}; unsigned init = get_state(s0); // put s0 in todo res_->set_init_state(init); } @@ -99,39 +146,67 @@ namespace spot // main loop while (!todo.empty()) { - lar_state current = todo.front(); + lar_state current = std::move(todo.front().s); + unsigned src_num = todo.front().num; todo.pop_front(); - // TODO todo could store this number to avoid one lookup - unsigned src_num = get_state(current); - for (const auto& e : aut_->out(current.state)) { // find the new permutation std::vector new_perm = current.perm; + std::vector new_count = current.count; + std::vector hits(new_count.size(), 0); unsigned h = 0; for (unsigned k : e.acc.sets()) { - auto it = std::find(new_perm.begin(), new_perm.end(), k); - h = std::max(h, unsigned(new_perm.end() - it)); - std::rotate(it, it+1, new_perm.end()); + unsigned c = acc2class[k]; + if (accpos[k] == new_count[c]) + new_count[c] += 1; + else + ++hits[c]; + if (new_count[c] == classes[c].count()) + { + new_count[c] = 0; + auto it = + std::find(new_perm.begin(), new_perm.end(), c); + assert(it != new_perm.end()); + h = std::max(h, unsigned(new_perm.end() - it)); + std::rotate(it, it+1, new_perm.end()); + } } - lar_state dst{e.dst, new_perm}; + lar_state dst{e.dst, new_perm, new_count}; unsigned dst_num = get_state(dst); // do the h last elements satisfy the acceptance condition? - acc_cond::mark_t m(new_perm.end() - h, new_perm.end()); + acc_cond::mark_t m({}); + for (auto c = new_perm.end() - h; c != new_perm.end(); ++c) + m |= classes[*c]; + for (auto c = new_perm.begin(); c != new_perm.end() - h; ++c) + { + for (unsigned k : classes[*c].sets()) + { + if (hits[*c] == 0) + break; + m.set(k); + --hits[*c]; + } + } + if (aut_->acc().accepting(m)) - res_->new_edge(src_num, dst_num, e.cond, {2*h}); + res_->new_edge(src_num, dst_num, e.cond, {2*m.count()}); else - res_->new_edge(src_num, dst_num, e.cond, {2*h+1}); + res_->new_edge(src_num, dst_num, e.cond, {2*m.count()+1}); } } // parity max even - res_->set_acceptance(2*aut_->num_sets() + 2, - acc_cond::acc_code::parity(true, false, 2*aut_->num_sets() + 2)); + unsigned nb_colors = 2*aut_->num_sets() + 2; + res_->set_acceptance(nb_colors, + acc_cond::acc_code::parity(true, false, nb_colors)); + + // inherit properties of the input automaton + res_->prop_copy(aut_, { false, false, true, false, true, true }); if (pretty_print) { diff --git a/tests/python/accparse2.py b/tests/python/accparse2.py index 952d19703..4e6eb1cb3 100644 --- a/tests/python/accparse2.py +++ b/tests/python/accparse2.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement +# Copyright (C) 2015, 2017-2018 Laboratoire de Recherche et Développement # de l'Epita # # This file is part of Spot, a model checking library. @@ -107,3 +107,10 @@ assert(a.is_streett() == -1) a.set_acceptance('(Fin(0)|Inf(1))&(Inf(1)|Fin(0))&(Inf(3)|Fin(2))') assert(a.is_rabin() == -1) assert(a.is_streett() == 2) + +a = spot.acc_code('Inf(0)&Inf(1)&Inf(3) | Fin(0)&(Fin(1)|Fin(3))') +u = a.symmetries() +assert u[0] == 0 +assert u[1] == 1 +assert u[2] == 2 +assert u[3] == 1 diff --git a/tests/python/toparity.py b/tests/python/toparity.py index edb8f77f1..59bd13660 100644 --- a/tests/python/toparity.py +++ b/tests/python/toparity.py @@ -20,6 +20,21 @@ import spot +a = spot.automaton("""HOA: v1 +States: 1 +Start: 0 +AP: 2 "a" "b" +Acceptance: 2 Inf(0)|Inf(1) +--BODY-- +State: 0 +[0&1] 0 {0 1} +[0&!1] 0 {0} +[!0&1] 0 {1} +[!0&!1] 0 +--END--""") +p = spot.to_parity(a) +assert spot.are_equivalent(a, p) + for f in spot.randltl(4, 400): d = spot.translate(f, "det", "G") p = spot.to_parity(d)