From 0168efea60334b5f3336d1f1fe3e7490e4429e15 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Mon, 6 Mar 2023 18:37:12 +0100 Subject: [PATCH] expansions: latest implementation --- spot/tl/expansions.cc | 560 +++++++++++++++++++++++++++++++++++++++++- spot/tl/expansions.hh | 20 ++ 2 files changed, 576 insertions(+), 4 deletions(-) diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index 20efe4eb2..1d225b603 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -548,6 +548,471 @@ namespace spot return formula::OrRat(res); } + class bdd_finalizer + { + public: + bdd_finalizer(std::multimap& exp, bdd_dict_ptr d) + : anon_set_(bddtrue) + , d_(d) + { + for (const auto& [prefix, suffix] : exp) + { + int anon_var_num; + auto it = formula2bdd_.find(suffix); + if (it != formula2bdd_.end()) + { + anon_var_num = it->second; + } + else + { + anon_var_num = d_->register_anonymous_variables(1, this); + formula2bdd_.insert({suffix, anon_var_num}); + bdd2formula_.insert({anon_var_num, suffix}); + } + + bdd var = bdd_ithvar(anon_var_num); + anon_set_ &= var; + exp_ |= prefix & var; + } + } + + ~bdd_finalizer() + { + d_->unregister_all_my_variables(this); + } + + std::multimap + simplify(exp_opts_new::expand_opt_new opts); + + private: + bdd exp_; + bdd anon_set_; + std::map formula2bdd_; + std::map bdd2formula_; + bdd_dict_ptr d_; + + formula var_to_formula(int var); + formula conj_bdd_to_sere(bdd b); + formula bdd_to_sere(bdd b); + }; + + formula + bdd_finalizer::var_to_formula(int var) + { + formula f = bdd2formula_[var]; + assert(f); + return f; + } + + formula + bdd_finalizer::bdd_to_sere(bdd f) + { + if (f == bddfalse) + return formula::ff(); + + std::vector v; + minato_isop isop(f); + bdd cube; + while ((cube = isop.next()) != bddfalse) + v.emplace_back(conj_bdd_to_sere(cube)); + return formula::OrRat(std::move(v)); + } + + formula + bdd_finalizer::conj_bdd_to_sere(bdd b) + { + if (b == bddtrue) + return formula::tt(); + if (b == bddfalse) + return formula::ff(); + + // Unroll the first loop of the next do/while loop so that we + // do not have to create v when b is not a conjunction. + formula res = var_to_formula(bdd_var(b)); + bdd high = bdd_high(b); + if (high == bddfalse) + { + res = formula::Not(res); + b = bdd_low(b); + } + else + { + assert(bdd_low(b) == bddfalse); + b = high; + } + if (b == bddtrue) + return res; + std::vector v{std::move(res)}; + do + { + res = var_to_formula(bdd_var(b)); + high = bdd_high(b); + if (high == bddfalse) + { + res = formula::Not(res); + b = bdd_low(b); + } + else + { + assert(bdd_low(b) == bddfalse); + b = high; + } + assert(b != bddfalse); + v.emplace_back(std::move(res)); + } + while (b != bddtrue); + return formula::multop(op::AndRat, std::move(v)); + } + + std::multimap + bdd_finalizer::simplify(exp_opts_new::expand_opt_new opts) + { + std::multimap res; + + if (opts & exp_opts_new::expand_opt_new::BddMinterm) + { + bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_); + bdd or_labels = bdd_exist(exp_, anon_set_); + for (bdd letter: minterms_of(exp_, prop_set)) + { + bdd dest_bdd = bdd_restrict(exp_, letter); + formula dest = bdd_to_sere(dest_bdd); + + auto it = res.insert({letter, dest}); + assert(it.second); + (void) it; + } + } + else // BddIsop + { + minato_isop isop(exp_); + bdd cube; + while ((cube = isop.next()) != bddfalse) + { + bdd letter = bdd_exist(cube, anon_set_); + bdd suffix = bdd_existcomp(cube, anon_set_); + formula dest = conj_bdd_to_sere(suffix); + + res.insert({letter, dest}); + } + } + + return res; + } + + void + finalize_new(std::multimap& exp, exp_opts_new::expand_opt_new opts, bdd_dict_ptr d) + { + if (opts & (exp_opts_new::expand_opt_new::BddIsop + | exp_opts_new::expand_opt_new::BddMinterm)) + { + bdd_finalizer bddf(exp, d); + exp = bddf.simplify(opts); + } + + if (opts & exp_opts_new::expand_opt_new::UniqueSuffix) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({suffix, prefix}); + if (!res.second) + { + auto it = res.first; + it->second |= prefix; + } + } + + exp.clear(); + for (const auto [suffix, prefix] : unique_map) + { + exp.insert({prefix, suffix}); + } + } + + if (opts & exp_opts_new::expand_opt_new::UniquePrefix) + { + std::map unique_map; + for (const auto& [prefix, suffix] : exp) + { + auto res = unique_map.insert({prefix, suffix}); + if (!res.second) + { + auto it = res.first; + it->second = formula::OrRat({it->second, suffix}); + } + } + + exp.clear(); + for (const auto [prefix, suffix] : unique_map) + { + exp.insert({prefix, suffix}); + } + } + } + + std::multimap + expansion_new(formula f, const bdd_dict_ptr& d, void *owner, exp_opts_new::expand_opt_new opts) + { + using exp_t = std::multimap; + + if (f.is_boolean()) + { + auto f_bdd = formula_to_bdd(f, d, owner); + + if (f_bdd == bddfalse) + return {}; + + return {{f_bdd, formula::eword()}}; + } + + auto rec = [&d, owner, opts](formula f){ + return expansion_new(f, d, owner, exp_opts_new::None); + }; + + + switch (f.kind()) + { + case op::ff: + case op::tt: + case op::ap: + SPOT_UNREACHABLE(); + + case op::eword: + return {{bddfalse, formula::ff()}}; + + case op::Concat: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.insert({bdd_l, formula::Concat({form, f.all_but(0)})}); + } + + if (f[0].accepts_eword()) + { + auto exps_rest = rec(f.all_but(0)); + for (const auto& [bdd_l, form] : exps_rest) + { + res.insert({bdd_l, form}); + } + } + + finalize_new(res, opts, d); + return res; + } + + case op::FStar: + { + formula E = f[0]; + + if (f.min() == 0 && f.max() == 0) + return {{bddtrue, formula::eword()}}; + + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + auto E_i_j_minus = formula::FStar(E, min, max); + + auto exp = rec(E); + exp_t res; + for (const auto& [li, ei] : exp) + { + res.insert({li, formula::Fusion({ei, E_i_j_minus})}); + + if (ei.accepts_eword() && f.min() != 0) + { + for (const auto& [ki, fi] : rec(E_i_j_minus)) + { + // FIXME: build bdd once + if ((li & ki) != bddfalse) + res.insert({li & ki, fi}); + } + } + } + if (f.min() == 0) + res.insert({bddtrue, formula::eword()}); + + finalize_new(res, opts, d); + return res; + } + + case op::Star: + { + auto min = f.min() == 0 ? 0 : (f.min() - 1); + auto max = f.max() == formula::unbounded() + ? formula::unbounded() + : (f.max() - 1); + + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.insert({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})}); + } + + finalize_new(res, opts, d); + return res; + } + + case op::AndNLM: + { + formula rewrite = rewrite_and_nlm(f); + auto res = rec(rewrite); + finalize_new(res, opts, d); + return res; + } + + case op::first_match: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.insert({bdd_l, form}); + } + + // determinize + bdd or_labels = bddfalse; + bdd support = bddtrue; + bool is_det = true; + for (const auto& [l, _] : res) + { + support &= bdd_support(l); + if (is_det) + is_det = !bdd_have_common_assignment(l, or_labels); + or_labels |= l; + } + + if (is_det) + { + finalize_new(res, opts, d); + return res; + } + + exp_t res_det; + std::vector dests; + for (bdd l: minterms_of(or_labels, support)) + { + for (const auto& [ndet_label, ndet_dest] : res) + { + if (bdd_implies(l, ndet_label)) + dests.push_back(ndet_dest); + } + formula or_dests = formula::OrRat(dests); + res_det.insert({l, or_dests}); + dests.clear(); + } + + for (auto& [_, dest] : res_det) + dest = formula::first_match(dest); + finalize_new(res_det, opts, d); + return res_det; + } + + case op::Fusion: + { + exp_t res; + formula E = f[0]; + formula F = f.all_but(0); + + exp_t Ei = rec(E); + // TODO: std::option + exp_t Fj = rec(F); + + for (const auto& [li, ei] : Ei) + { + if (ei.accepts_eword()) + { + for (const auto& [kj, fj] : Fj) + if ((li & kj) != bddfalse) + res.insert({li & kj, fj}); + } + res.insert({li, formula::Fusion({ei, F})}); + } + + finalize_new(res, opts, d); + return res; + } + + case op::AndRat: + { + exp_t res; + for (const auto& sub_f : f) + { + auto exps = rec(sub_f); + + if (exps.empty()) + { + // op::AndRat: one of the expansions was empty (the only + // edge was `false`), so the AndRat is empty as + // well + res.clear(); + break; + } + + if (res.empty()) + { + res = std::move(exps); + continue; + } + + exp_t new_res; + for (const auto& [l_key, l_val] : exps) + { + for (const auto& [r_key, r_val] : res) + { + if ((l_key & r_key) != bddfalse) + new_res.insert({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})}); + } + } + + res = std::move(new_res); + } + + finalize_new(res, opts, d); + return res; + } + + case op::OrRat: + { + exp_t res; + for (const auto& sub_f : f) + { + auto exps = rec(sub_f); + if (exps.empty()) + continue; + + if (res.empty()) + { + res = std::move(exps); + continue; + } + + for (const auto& [label, dest] : exps) + res.insert({label, dest}); + } + + finalize_new(res, opts, d); + return res; + } + + default: + std::cerr << "unimplemented kind " + << static_cast(f.kind()) + << std::endl; + SPOT_UNIMPLEMENTED(); + } + + return {}; + } + std::multimap expansion_simple(formula f, const bdd_dict_ptr& d, void *owner) { @@ -1031,12 +1496,13 @@ namespace spot expansion_t expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts) { - if (opts & exp_opts::Basic) - return expansion_impl(f, d, owner, opts); + + if (opts & exp_opts::Bdd) + return expansion_impl(f, d, owner, opts); else if (opts & exp_opts::MergeSuffix) return expansion_impl(f, d, owner, opts); - else // exp_opts::Bdd - return expansion_impl(f, d, owner, opts); + else // exp_opts::Basic + return expansion_impl(f, d, owner, opts); } twa_graph_ptr @@ -1210,4 +1676,90 @@ namespace spot aut->merge_edges(); return aut; } + + twa_graph_ptr + expand_new_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts) + { + auto finite = expand_new_finite_automaton(f, d, opts); + return from_finite(finite); + } + + twa_graph_ptr + expand_new_finite_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts) + { + auto aut = make_twa_graph(d); + + aut->prop_state_acc(true); + const auto acc_mark = aut->set_buchi(); + + auto formula2state = robin_hood::unordered_map(); + + unsigned init_state = aut->new_state(); + aut->set_init_state(init_state); + formula2state.insert({ f, init_state }); + + auto f_aps = formula_aps(f); + for (auto& ap : f_aps) + aut->register_ap(ap); + + auto todo = std::vector>(); + todo.push_back({f, init_state}); + + auto state_names = new std::vector(); + std::ostringstream ss; + ss << f; + state_names->push_back(ss.str()); + + auto find_dst = [&](formula suffix) -> unsigned + { + unsigned dst; + auto it = formula2state.find(suffix); + if (it != formula2state.end()) + { + dst = it->second; + } + else + { + dst = aut->new_state(); + todo.push_back({suffix, dst}); + formula2state.insert({suffix, dst}); + std::ostringstream ss; + ss << suffix; + state_names->push_back(ss.str()); + } + + return dst; + }; + + while (!todo.empty()) + { + auto [curr_f, curr_state] = todo[todo.size() - 1]; + todo.pop_back(); + + auto curr_acc_mark= curr_f.accepts_eword() + ? acc_mark + : acc_cond::mark_t(); + + auto exp = expansion_new(curr_f, d, aut.get(), opts); + + for (const auto& [letter, suffix] : exp) + { + if (suffix.is(op::ff)) + continue; + + auto dst = find_dst(suffix); + aut->new_edge(curr_state, dst, letter, curr_acc_mark); + } + + // if state has no transitions and should be accepting, create + // artificial transition + if (aut->get_graph().state_storage(curr_state).succ == 0 + && curr_f.accepts_eword()) + aut->new_edge(curr_state, curr_state, bddfalse, acc_mark); + } + + aut->set_named_prop("state-names", state_names); + aut->merge_edges(); + return aut; + } } diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh index ff6977f9b..4286e8fd6 100644 --- a/spot/tl/expansions.hh +++ b/spot/tl/expansions.hh @@ -43,6 +43,26 @@ namespace spot }; }; + struct exp_opts_new + { + enum expand_opt_new { + None = 0, + UniqueSuffix = 1, + UniquePrefix = 2, + BddIsop = 4, + BddMinterm = 8, + }; + }; + + SPOT_API std::multimap + expansion_new(formula f, const bdd_dict_ptr& d, void *owner, exp_opts_new::expand_opt_new opts); + + SPOT_API twa_graph_ptr + expand_new_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts); + + SPOT_API twa_graph_ptr + expand_new_finite_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts); + SPOT_API twa_graph_ptr expand_simple_automaton(formula f, bdd_dict_ptr d);