From 0e2ebef70992e6b8249a67fa7a0c2f2380a1ee13 Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Thu, 19 Sep 2024 08:41:04 +0200 Subject: [PATCH] expansions: split --- python/spot/impl.i | 2 + spot/tl/Makefile.am | 3 +- spot/tl/expansions.cc | 31 +- spot/tl/expansions.hh | 2 + spot/tl/expansions2.cc | 930 +++++++++++++++++++++++++++++++++++++++++ spot/tl/expansions2.hh | 45 ++ tests/Makefile.am | 2 - 7 files changed, 999 insertions(+), 16 deletions(-) create mode 100644 spot/tl/expansions2.cc create mode 100644 spot/tl/expansions2.hh diff --git a/python/spot/impl.i b/python/spot/impl.i index ee2c6a81e..a435758f6 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -89,6 +89,7 @@ #include #include #include +#include #include #include #include @@ -638,6 +639,7 @@ namespace std { %include %include %include +%include %include %include %include diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index abb431267..f2ff0fcad 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -32,7 +32,7 @@ tl_HEADERS = \ dot.hh \ environment.hh \ exclusive.hh \ - expansions.hh \ + expansions2.hh \ formula.hh \ hierarchy.hh \ length.hh \ @@ -60,6 +60,7 @@ libtl_la_SOURCES = \ dot.cc \ exclusive.cc \ expansions.cc \ + expansions2.cc \ formula.cc \ hierarchy.cc \ length.cc \ diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index 756af4082..c09aec083 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -278,11 +278,11 @@ namespace spot bdd dest_bdd = bdd_restrict(exp_, letter); formula dest = bdd_to_sere(dest_bdd); - #ifndef NDEBUG - // make sure it didn't exist before - auto it = std::find(res.begin(), res.end(), {letter, dest}); - SPOT_ASSERT(it == res.end()); - #endif + // #ifndef NDEBUG + // // make sure it didn't exist before + // auto it = std::find(res.begin(), res.end(), {letter, dest}); + // SPOT_ASSERT(it == res.end()); + // #endif res.push_back({letter, dest}); } @@ -338,7 +338,7 @@ namespace spot expansion_t res; - for (const auto [prefix, suffix] : unique_map) + for (const auto& [prefix, suffix] : unique_map) { if (!suffix.is(op::OrRat)) { @@ -435,17 +435,22 @@ namespace spot } exp.clear(); - for (const auto [suffix, prefix] : unique_map) + for (const auto& [suffix, prefix] : unique_map) { exp.push_back({prefix, suffix}); } } - if (opts & exp_opts::expand_opt::UniquePrefix) + if (opts & exp_opts::expand_opt::UniquePrefix + || opts & exp_opts::expand_opt::UniquePrefixSeenOpt + || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) { - exp = unique_prefix(exp); - //exp = unique_prefix_seen(exp, seen); - //exp = unique_prefix_count(exp, seen); + if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt) + exp = unique_prefix_seen(exp, seen); + else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) + exp = unique_prefix_count(exp, seen); + else + exp = unique_prefix(exp); } if (opts & exp_opts::expand_opt::UniqueSuffixPost) @@ -462,7 +467,7 @@ namespace spot } exp.clear(); - for (const auto [suffix, prefix] : unique_map) + for (const auto& [suffix, prefix] : unique_map) { exp.push_back({prefix, suffix}); } @@ -817,7 +822,7 @@ namespace spot struct signature_hash { std::size_t - operator() (const std::pair& sig) const + operator() (const std::pair& sig) const noexcept { size_t hash = std::hash()(sig.first); diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh index 036ac945a..9db8d2c8d 100644 --- a/spot/tl/expansions.hh +++ b/spot/tl/expansions.hh @@ -47,6 +47,8 @@ namespace spot Determinize = 256, UniquePrefixSeenOpt = 512, UniqueSuffixPost = 1024, + UniquePrefixSeenCountOpt = 2048, + TransitionBased = 4096, }; }; diff --git a/spot/tl/expansions2.cc b/spot/tl/expansions2.cc new file mode 100644 index 000000000..012ac11e8 --- /dev/null +++ b/spot/tl/expansions2.cc @@ -0,0 +1,930 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "config.h" +#include +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + // FIXME: could probably just return a map directly + static std::vector + formula_aps(formula f) + { + auto res = std::unordered_set(); + + f.traverse([&res](formula f) + { + if (f.is(op::ap)) + { + res.insert(f.ap_name()); + return true; + } + + return false; + }); + + return std::vector(res.begin(), res.end()); + } + + formula + rewrite_and_nlm(formula f) + { + unsigned s = f.size(); + std::vector final; + std::vector non_final; + + for (auto g: f) + if (g.accepts_eword()) + final.emplace_back(g); + else + non_final.emplace_back(g); + + if (non_final.empty()) + // (a* & b*);c = (a*|b*);c + return formula::OrRat(std::move(final)); + if (!final.empty()) + { + // let F_i be final formulae + // N_i be non final formula + // (F_1 & ... & F_n & N_1 & ... & N_m) + // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) + // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] + formula f = formula::OrRat(std::move(final)); + formula n = formula::AndNLM(std::move(non_final)); + formula t = formula::one_star(); + formula ft = formula::Concat({f, t}); + formula nt = formula::Concat({n, t}); + formula ftn = formula::AndRat({ft, n}); + formula fnt = formula::AndRat({f, nt}); + return formula::OrRat({ftn, fnt}); + } + // No final formula. + // Translate N_1 & N_2 & ... & N_n into + // N_1 && (N_2;[*]) && ... && (N_n;[*]) + // | (N_1;[*]) && N_2 && ... && (N_n;[*]) + // | (N_1;[*]) && (N_2;[*]) && ... && N_n + formula star = formula::one_star(); + std::vector disj; + for (unsigned n = 0; n < s; ++n) + { + std::vector conj; + for (unsigned m = 0; m < s; ++m) + { + formula g = f[m]; + if (n != m) + g = formula::Concat({g, star}); + conj.emplace_back(g); + } + disj.emplace_back(formula::AndRat(std::move(conj))); + } + return formula::OrRat(std::move(disj)); + } + + class bdd_finalizer + { + public: + int encode(formula f) + { + bool is_anon = false; + int var_num; + auto it = formula2bdd_.find(f); + if (it != formula2bdd_.end()) + { + var_num = it->second; + } + else + { + if (opt_sigma_star_ && (f.is(op::Star) + && f[0].is(op::tt) + && f.min() == 0 + && f.max() == formula::unbounded())) + { + var_num = bddtrue.id(); + } + else if (opt_bdd_encode_ && (f.is(op::AndRat) || f.is(op::OrRat))) + { + bdd var = f.is(op::AndRat) ? bdd(bddtrue) : bdd(bddfalse); + for (const auto& sub_f : f) + { + int bddid = encode(sub_f); + bdd subvar = bdd_ithvar(bddid); + var = f.is(op::AndRat) ? var & subvar : var | subvar; + } + var_num = var.id(); + } + else + { + var_num = d_->register_anonymous_variables(1, this); + is_anon = true; + } + + formula2bdd_.insert({f, var_num}); + bdd2formula_.insert({var_num, f}); + } + + bdd var = bdd_ithvar(var_num); + + if (is_anon) + anon_set_ &= var; + + return var_num; + } + + bdd_finalizer(expansion_t& exp, bdd_dict_ptr d, bool opt_sigma_star, bool opt_bdd_encode) + : anon_set_(bddtrue) + , d_(d) + , opt_sigma_star_(opt_sigma_star) + , opt_bdd_encode_(opt_bdd_encode) + { + for (const auto& [prefix, suffix] : exp) + { + int var_num = encode(suffix); + bdd var = bdd_ithvar(var_num); + exp_ |= prefix & var; + } + } + + ~bdd_finalizer() + { + d_->unregister_all_my_variables(this); + } + + expansion_t + simplify(exp_opts::expand_opt opts); + + private: + bdd exp_; + bdd anon_set_; + std::map formula2bdd_; + std::map bdd2formula_; + bdd_dict_ptr d_; + bool opt_sigma_star_; + bool opt_bdd_encode_; + + 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) + { + if (opt_sigma_star_){ + return formula::Star(formula::tt(), 0, formula::unbounded()); + } else { + 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)); + } + + expansion_t + bdd_finalizer::simplify(exp_opts::expand_opt opts) + { + expansion_t res; + + if (opts & exp_opts::expand_opt::BddMinterm) + { + bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_); + bdd or_labels = bdd_exist(exp_, anon_set_); + // TODO: check are_equivalent avec or_labels/exp_ en premier argument + for (bdd letter: minterms_of(or_labels, prop_set)) + { + bdd dest_bdd = bdd_restrict(exp_, letter); + formula dest = bdd_to_sere(dest_bdd); + + // #ifndef NDEBUG + // // make sure it didn't exist before + // auto it = std::find(res.begin(), res.end(), {letter, dest}); + // SPOT_ASSERT(it == res.end()); + // #endif + + res.push_back({letter, dest}); + } + } + 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.push_back({letter, dest}); + } + } + + return res; + } + + expansion_t + unique_prefix(const expansion_t& exp) + { + 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}); + } + } + + expansion_t res(unique_map.begin(), unique_map.end()); + return res; + } + + expansion_t + unique_prefix_seen(const expansion_t& exp, std::unordered_set* seen) + { + 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}); + } + } + + expansion_t res; + + for (const auto& [prefix, suffix] : unique_map) + { + if (!suffix.is(op::OrRat)) + { + res.push_back({prefix, suffix}); + continue; + } + + std::vector merge; + std::vector single; + + for (const auto& sub_f : suffix) + { + if (seen->find(sub_f) != seen->end()) + { + single.push_back(sub_f); + } + else + { + merge.push_back(sub_f); + } + } + + for (const auto& sub_f : single) + res.push_back({prefix, sub_f}); + + if (!merge.empty()) + res.push_back({prefix, formula::OrRat(merge)}); + } + + return res; + } + + size_t count_new(const expansion_t& exp, std::unordered_set* seen) + { + size_t count = 0; + for (const auto& [_, suffix] : exp) + { + if (seen->find(suffix) == seen->end()) + count++; + } + return count; + } + + const expansion_t& + find_smallest(const expansion_t& left, + const expansion_t& right, + std::unordered_set* seen) + { + size_t left_new = count_new(left, seen); + size_t right_new = count_new(right, seen); + + if (left_new < right_new) + return left; + + if (left_new == right_new && left.size() > right.size()) + return right; + + return right; + } + + expansion_t + unique_prefix_count(const expansion_t& exp, std::unordered_set* seen) + { + expansion_t up = unique_prefix(exp); + expansion_t up_seen = unique_prefix_seen(exp, seen); + + const expansion_t& maybe_smallest = find_smallest(exp, up, seen); + const expansion_t& smallest = find_smallest(maybe_smallest, up_seen, seen); + + return smallest; + } + + void + finalize(expansion_t& exp, exp_opts::expand_opt opts, bdd_dict_ptr d, std::unordered_set* seen) + { + if (opts & (exp_opts::expand_opt::BddIsop + | exp_opts::expand_opt::BddMinterm)) + { + bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode); + exp = bddf.simplify(opts); + } + + if (opts & exp_opts::expand_opt::UniqueSuffixPre) + { + 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.push_back({prefix, suffix}); + } + } + + if (opts & exp_opts::expand_opt::UniquePrefix + || opts & exp_opts::expand_opt::UniquePrefixSeenOpt + || opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) + { + if (opts & exp_opts::expand_opt::UniquePrefixSeenOpt) + exp = unique_prefix_seen(exp, seen); + else if (opts & exp_opts::expand_opt::UniquePrefixSeenCountOpt) + exp = unique_prefix_count(exp, seen); + else + exp = unique_prefix(exp); + } + + if (opts & exp_opts::expand_opt::UniqueSuffixPost) + { + 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.push_back({prefix, suffix}); + } + } + + if (opts & exp_opts::expand_opt::Determinize) + { + expansion_t exp_new; + + bdd props = bddtrue; + for (const auto& [prefix, _] : exp) + props &= bdd_support(prefix); + + std::vector dests; + for (bdd letter : minterms_of(bddtrue, props)) + { + for (const auto& [prefix, suffix] : exp) + { + if (bdd_implies(letter, prefix)) + dests.push_back(suffix); + } + formula or_dests = formula::OrRat(dests); + exp_new.push_back({letter, or_dests}); + dests.clear(); + } + exp = exp_new; + } + } + } + + formula + expansion_to_formula2(expansion_t e, bdd_dict_ptr& d) + { + std::vector res; + + for (const auto& [key, val] : e) + { + formula prefix = bdd_to_formula(key, d); + res.push_back(formula::Concat({prefix, val})); + } + + return formula::OrRat(res); + } + + expansion_t + expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen) + { + using exp_t = expansion_t; + + 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, seen](formula f){ + return expansion2(f, d, owner, exp_opts::None, seen); + }; + + + switch (f.kind()) + { + case op::ff: + case op::tt: + case op::ap: + SPOT_UNREACHABLE(); + + case op::eword: + // return {{bddfalse, formula::ff()}}; + return {}; + + case op::Concat: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({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.push_back({bdd_l, form}); + } + } + + finalize(res, opts, d, seen); + 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.push_back({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.push_back({li & ki, fi}); + } + } + } + if (f.min() == 0) + res.push_back({bddtrue, formula::eword()}); + + finalize(res, opts, d, seen); + 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.push_back({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})}); + } + + finalize(res, opts, d, seen); + return res; + } + + case op::AndNLM: + { + formula rewrite = rewrite_and_nlm(f); + auto res = rec(rewrite); + finalize(res, opts, d, seen); + return res; + } + + case op::first_match: + { + auto exps = rec(f[0]); + + exp_t res; + for (const auto& [bdd_l, form] : exps) + { + res.push_back({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) + { + for (auto& [_, dest] : res) + dest = formula::first_match(dest); + finalize(res, opts, d, seen); + 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.push_back({l, or_dests}); + dests.clear(); + } + + for (auto& [_, dest] : res_det) + dest = formula::first_match(dest); + finalize(res_det, opts, d, seen); + 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.push_back({li & kj, fj}); + } + res.push_back({li, formula::Fusion({ei, F})}); + } + + finalize(res, opts, d, seen); + 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; + bool inserted = false; + for (const auto& [l_key, l_val] : exps) + { + for (const auto& [r_key, r_val] : res) + { + if ((l_key & r_key) != bddfalse) + { + new_res.push_back({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})}); + inserted = true; + } + } + } + + if (!inserted) + { + // all prefix conjuctions led to bddfalse, And is empty + res.clear(); + break; + } + + res = std::move(new_res); + } + + finalize(res, opts, d, seen); + 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.push_back({label, dest}); + } + + finalize(res, opts, d, seen); + return res; + } + + default: + std::cerr << "unimplemented kind " + << static_cast(f.kind()) + << std::endl; + SPOT_UNIMPLEMENTED(); + } + + return {}; + } + + twa_graph_ptr + expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts) + { + auto finite = expand_finite_automaton2(f, d, opts); + return from_finite(finite); + } + + struct signature_hash + { + std::size_t + operator() (const expansion_t& sig) const noexcept + { + size_t hash = 0; + + for (const auto& keyvalue : sig) + { + hash ^= (bdd_hash()(keyvalue.first) ^ std::hash()(keyvalue.second)) + + 0x9e3779b9 + (hash << 6) + (hash >> 2); + } + + return hash; + } + }; + + twa_graph_ptr + expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts) + { + bool signature_merge = opts & exp_opts::expand_opt::SignatureMerge; + + auto aut = make_twa_graph(d); + + aut->prop_state_acc(false); + const auto acc_mark = aut->set_buchi(); + + auto formula2state = robin_hood::unordered_map(); + auto signature2state = std::unordered_map(); + auto seen = std::unordered_set(); + seen.insert(f); + + 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 formula2signature = robin_hood::unordered_map(); + auto get_signature = [&](const formula& form) -> expansion_t + { + auto it = formula2signature.find(form); + if (it != formula2signature.end()) + { + return it->second; + } + auto exp = expansion2(form, d, aut.get(), opts, &seen); + formula2signature.insert({form, exp}); + return exp; + }; + + if (signature_merge) + signature2state.insert({ get_signature(f), init_state}); + + 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 + { + if (signature_merge) + { + auto exp = get_signature(suffix); + + auto it2 = signature2state.find(exp); + if (it2 != signature2state.end()) + { + formula2state.insert({suffix, it2->second}); + return it2->second; + } + } + + dst = aut->new_state(); + todo.push_back({suffix, dst}); + seen.insert(suffix); + + formula2state.insert({suffix, dst}); + if (signature_merge) + signature2state.insert({get_signature(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 exp = get_signature(curr_f); + + for (const auto& [letter, suffix] : exp) + { + if (suffix.is(op::ff)) + // TODO ASSERT NOT + continue; + + auto dst = find_dst(suffix); + + auto curr_acc_mark = suffix.accepts_eword() ? acc_mark : acc_cond::mark_t(); + aut->new_edge(curr_state, dst, letter, curr_acc_mark); + } + } + + aut->set_named_prop("state-names", state_names); + + if ((opts & exp_opts::MergeEdges) + && !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost)) + aut->merge_edges(); + + return aut; + } +} diff --git a/spot/tl/expansions2.hh b/spot/tl/expansions2.hh new file mode 100644 index 000000000..e517bb87a --- /dev/null +++ b/spot/tl/expansions2.hh @@ -0,0 +1,45 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include + +#include + +#include +#include +#include +#include +#include + +namespace spot +{ + SPOT_API expansion_t + expansion2(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts, std::unordered_set* seen = nullptr); + + SPOT_API twa_graph_ptr + expand_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts); + + SPOT_API twa_graph_ptr + expand_finite_automaton2(formula f, bdd_dict_ptr d, exp_opts::expand_opt opts); + + SPOT_API formula + expansion_to_formula2(expansion_t e, bdd_dict_ptr& d); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index a061ba23d..9bf0cef73 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -69,7 +69,6 @@ check_PROGRAMS = \ core/cube \ core/emptchk \ core/equals \ - core/expand \ core/graph \ core/kind \ core/length \ @@ -112,7 +111,6 @@ core_bricks_SOURCES = core/bricks.cc core_checkpsl_SOURCES = core/checkpsl.cc core_checkta_SOURCES = core/checkta.cc core_emptchk_SOURCES = core/emptchk.cc -core_expand_SOURCES = core/expand.cc core_graph_SOURCES = core/graph.cc core_ikwiad_SOURCES = core/ikwiad.cc core_intvcomp_SOURCES = core/intvcomp.cc