diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc index dc0e09182..5fb13c0de 100644 --- a/spot/tl/expansions.cc +++ b/spot/tl/expansions.cc @@ -325,6 +325,29 @@ namespace spot exp.insert({prefix, suffix}); } } + + if (opts & exp_opts::expand_opt::Determinize) + { + std::multimap 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.insert({letter, or_dests}); + dests.clear(); + } + exp = exp_new; + } } } diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh index 0aec0a106..949b25e29 100644 --- a/spot/tl/expansions.hh +++ b/spot/tl/expansions.hh @@ -41,8 +41,10 @@ namespace spot BddIsop = 4, BddMinterm = 8, BddSigmaStar = 16, - MergeEdges = 32, - SignatureMerge = 64, + BddEncode = 32, + MergeEdges = 64, + SignatureMerge = 128, + Determinize = 256, }; };