diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index 8b0309246..564468452 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -310,7 +310,7 @@ namespace spot exp = bddf.simplify(opts); } - if (opts & exp_opts::expand_opt::UniqueSuffix) + if (opts & exp_opts::expand_opt::UniqueSuffixPre) { std::map unique_map; for (const auto& [prefix, suffix] : exp) @@ -378,6 +378,26 @@ namespace spot } } + 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.insert({prefix, suffix}); + } + } + if (opts & exp_opts::expand_opt::Determinize) { std::multimap exp_new; @@ -831,7 +851,7 @@ namespace spot aut->set_named_prop("state-names", state_names); if ((opts & exp_opts::MergeEdges) - && !(opts & exp_opts::UniqueSuffix)) + && !(opts & exp_opts::UniqueSuffixPre || opts & exp_opts::UniqueSuffixPost)) aut->merge_edges(); return aut; diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh index 36476bd31..2418b1103 100644 --- a/spot/tl/expansions.hh +++ b/spot/tl/expansions.hh @@ -36,7 +36,7 @@ namespace spot { enum expand_opt { None = 0, - UniqueSuffix = 1, + UniqueSuffixPre = 1, UniquePrefix = 2, BddIsop = 4, BddMinterm = 8, @@ -46,6 +46,7 @@ namespace spot SignatureMerge = 128, Determinize = 256, UniquePrefixSeenOpt = 512, + UniqueSuffixPost = 1024, }; };