From fcf6e25132be220f124c5c2ec8238979bedfe563 Mon Sep 17 00:00:00 2001 From: Thibaud Michaud Date: Wed, 29 Oct 2014 10:47:52 +0100 Subject: [PATCH] Optimizing closure and sl. * src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh: Using vectors instead of sets and unordered maps, adding an overload to handle rvalue references. * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh: Adding an overload to handle rvalue references. * bench/stutter/stutter_invariance_formulas.cc, bench/stutter/stutter_invariance_randomgraph.cc: Automata are modified in-place by is_stutter_invariant so they have to be copied before being processed. * src/tgbaalgos/stutter_invariance.cc, src/tgbaalgos/stutter_invariance.hh: Use the in-place version of closure and sl. --- bench/stutter/stutter_invariance_formulas.cc | 22 ++- .../stutter/stutter_invariance_randomgraph.cc | 11 +- src/tgbaalgos/closure.cc | 138 +++++++----------- src/tgbaalgos/closure.hh | 5 + src/tgbaalgos/stutter_invariance.cc | 31 ++-- src/tgbaalgos/stutter_invariance.hh | 4 +- src/tgbaalgos/stutterize.cc | 45 +++--- src/tgbaalgos/stutterize.hh | 5 + 8 files changed, 130 insertions(+), 131 deletions(-) diff --git a/bench/stutter/stutter_invariance_formulas.cc b/bench/stutter/stutter_invariance_formulas.cc index b90d49ff2..66e7b22af 100644 --- a/bench/stutter/stutter_invariance_formulas.cc +++ b/bench/stutter/stutter_invariance_formulas.cc @@ -23,6 +23,7 @@ #include "bin/common_output.hh" #include "tgbaalgos/translate.hh" #include "tgbaalgos/stutter_invariance.hh" +#include "tgbaalgos/dupexp.hh" #include "ltlast/allnodes.hh" #include "ltlvisit/apcollect.hh" #include "ltlvisit/length.hh" @@ -30,13 +31,6 @@ #include #include "error.h" -#include "tgbaalgos/closure.hh" -#include "tgbaalgos/stutterize.hh" -#include "tgbaalgos/dotty.hh" -#include "tgba/tgbaproduct.hh" - -static unsigned n = 10; - const char argp_program_doc[] =""; const struct argp_child children[] = @@ -74,8 +68,9 @@ namespace const spot::ltl::formula* nf = spot::ltl::unop::instance(spot::ltl::unop::Not, f->clone()); - spot::const_tgba_digraph_ptr a = trans.run(f); - spot::const_tgba_digraph_ptr na = trans.run(nf); + spot::tgba_digraph_ptr a = trans.run(f); + spot::tgba_digraph_ptr na = trans.run(nf); + unsigned num_states = a->num_states(); spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f); bdd apdict = spot::ltl::atomic_prop_collect_as_bdd(f, a); bool res; @@ -88,13 +83,16 @@ namespace setenv("SPOT_STUTTER_CHECK", algostr, true); spot::stopwatch sw; + auto dup_a = std::make_shared(a); + auto dup_na = std::make_shared(na); + sw.start(); - for (unsigned i = 0; i < n; ++i) - res = spot::is_stutter_invariant(a, na, apdict); + res = spot::is_stutter_invariant(std::move(dup_a), + std::move(dup_na), apdict); const double time = sw.stop(); std::cout << formula << ", " << algo << ", " << ap->size() << ", " - << a->num_states() << ", " << res << ", " << time << std::endl; + << num_states << ", " << res << ", " << time * 1000000 << std::endl; if (algo > '1') assert(res == prev); diff --git a/bench/stutter/stutter_invariance_randomgraph.cc b/bench/stutter/stutter_invariance_randomgraph.cc index c479db5b2..80a5a9197 100644 --- a/bench/stutter/stutter_invariance_randomgraph.cc +++ b/bench/stutter/stutter_invariance_randomgraph.cc @@ -75,18 +75,24 @@ main() for (char algo = '1'; algo <= '8'; ++algo) { - // set SPOT_STUTTER_CHECK environment variable + // Set SPOT_STUTTER_CHECK environment variable. char algostr[2] = { 0 }; algostr[0] = algo; setenv("SPOT_STUTTER_CHECK", algostr, true); + // Copy vec, because is_stutter_invariant modifies the + // automata. + std::vector dup(vec); spot::stopwatch sw; sw.start(); bool res; for (auto& a: vec) - res = spot::is_stutter_invariant(a.first, a.second, apdict); + res = spot::is_stutter_invariant(std::move(a.first), + std::move(a.second), + apdict); const double time = sw.stop(); + vec = dup; std::cout << algo << ", " << props_n << ", " << states_n << ", " << res << ", " << time << std::endl; } @@ -95,6 +101,5 @@ main() } } - return 0; } diff --git a/src/tgbaalgos/closure.cc b/src/tgbaalgos/closure.cc index 83ed4fffe..ee03c4644 100644 --- a/src/tgbaalgos/closure.cc +++ b/src/tgbaalgos/closure.cc @@ -21,101 +21,73 @@ #include #include "closure.hh" #include "dupexp.hh" +#include namespace spot { - namespace + tgba_digraph_ptr + closure(tgba_digraph_ptr&& a) { - struct transition - { - unsigned dst; - acc_cond::mark_t acc; - transition(unsigned dst, acc_cond::mark_t acc) : - dst(dst), acc(acc) - { - } - }; + unsigned n = a->num_states(); + std::vector todo; + std::vector > dst2trans(n); - struct transition_hash - { - size_t - operator()(const transition& t) const + for (unsigned state = 0; state < n; ++state) { - return wang32_hash(t.dst) ^ wang32_hash(t.acc); - } - }; + auto trans = a->out(state); - struct transition_equal - { - bool - operator()(const transition& left, const transition& right) const - { - return left.dst == right.dst - && left.acc == right.acc; - } - }; + for (auto it = trans.begin(); it != trans.end(); ++it) + { + todo.push_back(it.trans()); + dst2trans[it->dst].push_back(it.trans()); + } - typedef std::unordered_map tmap_t; - typedef std::set tset_t; + while (!todo.empty()) + { + auto t1 = a->trans_storage(todo.back()); + todo.pop_back(); + + for (auto& t2 : a->out(t1.dst)) + { + bdd cond = t1.cond & t2.cond; + if (cond != bddfalse) + { + bool need_new_trans = true; + acc_cond::mark_t acc = t1.acc | t2.acc; + for (auto& t: dst2trans[t2.dst]) + { + auto& ts = a->trans_storage(t); + if (acc == ts.acc) + { + if (!bdd_implies(cond, ts.cond)) + { + ts.cond = ts.cond | cond; + if (std::find(todo.begin(), todo.end(), t) + == todo.end()) + todo.push_back(t); + } + need_new_trans = false; + } + } + if (need_new_trans) + { + unsigned i = + a->new_transition(state, t2.dst, cond, acc); + dst2trans[t2.dst].push_back(i); + todo.push_back(i); + } + } + } + } + for (auto& it: dst2trans) + it.clear(); + } + return a; } tgba_digraph_ptr closure(const const_tgba_digraph_ptr& a) { - tgba_digraph_ptr res = tgba_dupexp_dfs(a); - unsigned n = res->num_states(); - tset_t todo; - - for (unsigned state = 0; state < n; ++state) - { - tmap_t uniq; - auto trans = res->out(state); - - for (auto it = trans.begin(); it != trans.end(); ++it) - { - todo.insert(it.trans()); - uniq.emplace(transition(it->dst, it->acc), it.trans()); - } - - while (!todo.empty()) - { - unsigned t1 = *todo.begin(); - todo.erase(t1); - tgba_graph_trans_data td = res->trans_data(t1); - unsigned dst = res->trans_storage(t1).dst; - - for (auto& t2 : res->out(dst)) - { - bdd cond = td.cond & t2.cond; - if (cond != bddfalse) - { - acc_cond::mark_t acc = td.acc | t2.acc; - transition jump(t2.dst, acc); - unsigned i; - auto u = uniq.find(jump); - - if (u == uniq.end()) - { - i = res->new_transition(state, t2.dst, cond, acc); - uniq.emplace(jump, i); - todo.insert(i); - } - - else - { - bdd old_cond = res->trans_data(u->second).cond; - if (!bdd_implies(cond, old_cond)) - { - res->trans_data(u->second).cond = cond | old_cond; - todo.insert(u->second); - } - } - } - } - } - uniq.clear(); - } - return res; + return closure(make_tgba_digraph(a)); } } diff --git a/src/tgbaalgos/closure.hh b/src/tgbaalgos/closure.hh index c51fbfb3d..f4e2ea090 100644 --- a/src/tgbaalgos/closure.hh +++ b/src/tgbaalgos/closure.hh @@ -26,6 +26,11 @@ namespace spot { SPOT_API tgba_digraph_ptr closure(const const_tgba_digraph_ptr&); + +#ifndef SWIG + SPOT_API tgba_digraph_ptr + closure(tgba_digraph_ptr&&); +#endif } #endif diff --git a/src/tgbaalgos/stutter_invariance.cc b/src/tgbaalgos/stutter_invariance.cc index d19aa8b1a..326ca7f72 100644 --- a/src/tgbaalgos/stutter_invariance.cc +++ b/src/tgbaalgos/stutter_invariance.cc @@ -60,16 +60,16 @@ namespace spot } const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone()); translator trans; - auto aut_f = trans.run(f); - auto aut_nf = trans.run(nf); + tgba_digraph_ptr aut_f = trans.run(f); + tgba_digraph_ptr aut_nf = trans.run(nf); bdd aps = atomic_prop_collect_as_bdd(f, aut_f); nf->destroy(); - return is_stutter_invariant(aut_f, aut_nf, aps); + return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps); } bool - is_stutter_invariant(const const_tgba_digraph_ptr& aut_f, - const const_tgba_digraph_ptr& aut_nf, bdd aps) + is_stutter_invariant(tgba_digraph_ptr&& aut_f, + tgba_digraph_ptr&& aut_nf, bdd aps) { const char* stutter_check = getenv("SPOT_STUTTER_CHECK"); char algo = stutter_check ? stutter_check[0] : '8'; @@ -79,32 +79,38 @@ namespace spot // sl(aut_f) x sl(aut_nf) case '1': { - return product(sl(aut_f, aps), sl(aut_nf, aps))->is_empty(); + return product(sl(std::move(aut_f), aps), + sl(std::move(aut_nf), aps))->is_empty(); } // sl(cl(aut_f)) x aut_nf case '2': { - return product(sl(closure(aut_f), aps), aut_nf)->is_empty(); + return product(sl(closure(std::move(aut_f)), aps), + std::move(aut_nf))->is_empty(); } // (cl(sl(aut_f)) x aut_nf case '3': { - return product(closure(sl(aut_f, aps)), aut_nf)->is_empty(); + return product(closure(sl(std::move(aut_f), aps)), + std::move(aut_nf))->is_empty(); } // sl2(aut_f) x sl2(aut_nf) case '4': { - return product(sl2(aut_f, aps), sl2(aut_nf, aps))->is_empty(); + return product(sl2(std::move(aut_f), aps), + sl2(std::move(aut_nf), aps))->is_empty(); } // sl2(cl(aut_f)) x aut_nf case '5': { - return product(sl2(closure(aut_f), aps), aut_nf)->is_empty(); + return product(sl2(closure(std::move(aut_f)), aps), + std::move(aut_nf))->is_empty(); } // (cl(sl2(aut_f)) x aut_nf case '6': { - return product(closure(sl2(aut_f, aps)), aut_nf)->is_empty(); + return product(closure(sl2(std::move(aut_f), aps)), + std::move(aut_nf))->is_empty(); } // on-the-fly sl(aut_f) x sl(aut_nf) case '7': @@ -116,7 +122,8 @@ namespace spot // cl(aut_f) x cl(aut_nf) case '8': { - return product(closure(aut_f), closure(aut_nf))->is_empty(); + return product(closure(std::move(aut_f)), + closure(std::move(aut_nf)))->is_empty(); } default: throw std::runtime_error("invalid value for SPOT_STUTTER_CHECK."); diff --git a/src/tgbaalgos/stutter_invariance.hh b/src/tgbaalgos/stutter_invariance.hh index a5efee93b..95133eccc 100644 --- a/src/tgbaalgos/stutter_invariance.hh +++ b/src/tgbaalgos/stutter_invariance.hh @@ -29,8 +29,8 @@ namespace spot is_stutter_invariant(const ltl::formula* f); SPOT_API bool - is_stutter_invariant(const const_tgba_digraph_ptr& aut_f, - const const_tgba_digraph_ptr& aut_nf, bdd aps); + is_stutter_invariant(tgba_digraph_ptr&& aut_f, + tgba_digraph_ptr&& aut_nf, bdd aps); } #endif diff --git a/src/tgbaalgos/stutterize.cc b/src/tgbaalgos/stutterize.cc index 24ae54211..99eec217e 100644 --- a/src/tgbaalgos/stutterize.cc +++ b/src/tgbaalgos/stutterize.cc @@ -133,38 +133,45 @@ namespace spot } tgba_digraph_ptr - sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + sl2(tgba_digraph_ptr&& a, bdd atomic_propositions) { - tgba_digraph_ptr res = tgba_dupexp_dfs(a); - unsigned num_states = res->num_states(); + unsigned num_states = a->num_states(); + unsigned num_transitions = a->num_transitions(); for (unsigned state = 0; state < num_states; ++state) { - std::vector out; - auto trans = res->out(state); + auto trans = a->out(state); - for (auto it = trans.begin(); it != trans.end(); ++it) - out.push_back(it.trans()); - for (auto it: out) + for (auto it = trans.begin(); it != trans.end() + && it.trans() <= num_transitions; ++it) { - if (res->trans_storage(it).dst != state) + if (it->dst != state) { - bdd all = res->trans_storage(it).cond; + bdd all = it->cond; while (all != bddfalse) { - unsigned dst = res->trans_storage(it).dst; + unsigned dst = it->dst; bdd one = bdd_satoneset(all, atomic_propositions, bddtrue); - unsigned tmp = res->new_state(); - res->new_transition(state, tmp, one, - res->trans_storage(it).acc); - res->new_transition(tmp, tmp, one, 0U); - res->new_transition(tmp, dst, one, - res->trans_storage(it).acc); + unsigned tmp = a->new_state(); + unsigned i = a->new_transition(state, tmp, one, + it->acc); + assert(i > num_transitions); + i = a->new_transition(tmp, tmp, one, 0U); + assert(i > num_transitions); + i = a->new_transition(tmp, dst, one, + it->acc); + assert(i > num_transitions); all -= one; } } } } - res->merge_transitions(); - return res; + a->merge_transitions(); + return a; + } + + tgba_digraph_ptr + sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions) + { + return sl2(make_tgba_digraph(a), atomic_propositions); } } diff --git a/src/tgbaalgos/stutterize.hh b/src/tgbaalgos/stutterize.hh index 93de1aa70..47d94cf1e 100644 --- a/src/tgbaalgos/stutterize.hh +++ b/src/tgbaalgos/stutterize.hh @@ -38,6 +38,11 @@ namespace spot SPOT_API tgba_digraph_ptr sl2(const const_tgba_digraph_ptr&, bdd); + +#ifndef SWIG + SPOT_API tgba_digraph_ptr + sl2(tgba_digraph_ptr&&); +#endif } #endif