alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

expansions: determinize only once per state

Browse source
This commit is contained in:
Antoine Martin 2023-02-06 11:04:47 +01:00
parent faaefa7424
commit ce9a94f224
2 changed files with 31 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

59
spot/tl/expansions.cc
View file

@ -35,7 +35,7 @@ namespace spot
using exp_map = std::map<bdd, formula, bdd_less_than>; using exp_map = std::map<bdd, formula, bdd_less_than>;
virtual void insert(bdd letter, formula suffix) = 0; virtual void insert(bdd letter, formula suffix) = 0;
virtual void finalize(bool deterministic, std::function<formula(formula)> wrap = formula_identity) = 0; virtual void finalize(bool deterministic) = 0;
virtual exp_map& result() = 0; virtual exp_map& result() = 0;
virtual bool empty() = 0; virtual bool empty() = 0;
virtual void clear() = 0; virtual void clear() = 0;
@ -56,7 +56,7 @@ namespace spot
void insert(bdd letter, formula suffix) final; void insert(bdd letter, formula suffix) final;
void finalize(bool deterministic, std::function<formula(formula)> wrap = formula_identity) final; void finalize(bool deterministic) final;
exp_map& result() final exp_map& result() final
{ {
@ -88,7 +88,7 @@ namespace spot
} }
} }
void expansion_basic::finalize(bool deterministic, std::function<formula(formula)> wrap) void expansion_basic::finalize(bool deterministic)
{ {
if (!deterministic) if (!deterministic)
return; return;
@ -108,8 +108,6 @@ namespace spot
{ {
// we don't need to determinize the expansion, it's already // we don't need to determinize the expansion, it's already
// deterministic // deterministic
for (auto& [_, dest] : bdd2formula_)
dest = wrap(dest);
return; return;
} }
@ -123,7 +121,7 @@ namespace spot
dests.push_back(ndet_dest); dests.push_back(ndet_dest);
} }
formula or_dests = formula::OrRat(dests); formula or_dests = formula::OrRat(dests);
res.insert({l, wrap(or_dests)}); res.insert({l, or_dests});
dests.clear(); dests.clear();
} }
@ -145,7 +143,7 @@ namespace spot
void insert(bdd letter, formula suffix) final; void insert(bdd letter, formula suffix) final;
void finalize(bool deterministic, std::function<formula(formula)> wrap = formula_identity) final; void finalize(bool deterministic) final;
exp_map& result() final exp_map& result() final
{ {
@ -173,7 +171,7 @@ namespace spot
terms_.push_back({letter, suffix}); terms_.push_back({letter, suffix});
} }
void expansion_merge_formulas::finalize(bool deterministic, std::function<formula(formula)> wrap) void expansion_merge_formulas::finalize(bool deterministic)
{ {
res_.clear(); res_.clear();
@ -234,8 +232,6 @@ namespace spot
{ {
// we don't need to determinize the expansion, it's already // we don't need to determinize the expansion, it's already
// deterministic // deterministic
for (auto& [_, dest] : res_)
dest = wrap(dest);
return; return;
} }
@ -249,7 +245,7 @@ namespace spot
dests.push_back(ndet_dest); dests.push_back(ndet_dest);
} }
formula or_dests = formula::OrRat(dests); formula or_dests = formula::OrRat(dests);
res.insert({l, wrap(or_dests)}); res.insert({l, or_dests});
dests.clear(); dests.clear();
} }
@ -305,7 +301,7 @@ namespace spot
void insert(bdd letter, formula suffix) final; void insert(bdd letter, formula suffix) final;
void finalize(bool deterministic, std::function<formula(formula)> wrap = formula_identity) final; void finalize(bool deterministic) final;
exp_map& result() final exp_map& result() final
{ {
@ -427,7 +423,7 @@ namespace spot
return formula::OrRat(std::move(v)); return formula::OrRat(std::move(v));
} }
void expansion_bdd::finalize(bool deterministic, std::function<formula(formula)> wrap) void expansion_bdd::finalize(bool deterministic)
{ {
if (deterministic) if (deterministic)
{ {
@ -436,7 +432,7 @@ namespace spot
for (bdd letter: minterms_of(exp_, prop_set)) for (bdd letter: minterms_of(exp_, prop_set))
{ {
bdd dest_bdd = bdd_restrict(exp_, letter); bdd dest_bdd = bdd_restrict(exp_, letter);
formula dest = wrap(bdd_to_sere(dest_bdd)); formula dest = bdd_to_sere(dest_bdd);
auto it = res_.insert({letter, dest}); auto it = res_.insert({letter, dest});
assert(it.second); assert(it.second);
@ -567,6 +563,10 @@ namespace spot
return {{f_bdd, formula::eword()}}; return {{f_bdd, formula::eword()}};
} }
auto rec = [&d, owner](formula f){
return expansion_impl<ExpansionBuilder>(f, d, owner, exp_opts::None);
};
switch (f.kind()) switch (f.kind())
{ {
@ -580,7 +580,7 @@ namespace spot
case op::Concat: case op::Concat:
{ {
auto exps = expansion(f[0], d, owner, opts); auto exps = rec(f[0]);
ExpansionBuilder res(d); ExpansionBuilder res(d);
for (const auto& [bdd_l, form] : exps) for (const auto& [bdd_l, form] : exps)
@ -590,7 +590,7 @@ namespace spot
if (f[0].accepts_eword()) if (f[0].accepts_eword())
{ {
auto exps_rest = expansion(f.all_but(0), d, owner, opts); auto exps_rest = rec(f.all_but(0));
for (const auto& [bdd_l, form] : exps_rest) for (const auto& [bdd_l, form] : exps_rest)
{ {
res.insert(bdd_l, form); res.insert(bdd_l, form);
@ -615,7 +615,7 @@ namespace spot
auto E_i_j_minus = formula::FStar(E, min, max); auto E_i_j_minus = formula::FStar(E, min, max);
auto exp = expansion(E, d, owner, opts); auto exp = rec(E);
ExpansionBuilder res(d); ExpansionBuilder res(d);
for (const auto& [li, ei] : exp) for (const auto& [li, ei] : exp)
{ {
@ -623,7 +623,7 @@ namespace spot
if (ei.accepts_eword() && f.min() != 0) if (ei.accepts_eword() && f.min() != 0)
{ {
for (const auto& [ki, fi] : expansion(E_i_j_minus, d, owner, opts)) for (const auto& [ki, fi] : rec(E_i_j_minus))
{ {
// FIXME: build bdd once // FIXME: build bdd once
if ((li & ki) != bddfalse) if ((li & ki) != bddfalse)
@ -645,7 +645,7 @@ namespace spot
? formula::unbounded() ? formula::unbounded()
: (f.max() - 1); : (f.max() - 1);
auto exps = expansion(f[0], d, owner, opts); auto exps = rec(f[0]);
ExpansionBuilder res(d); ExpansionBuilder res(d);
for (const auto& [bdd_l, form] : exps) for (const auto& [bdd_l, form] : exps)
@ -660,12 +660,12 @@ namespace spot
case op::AndNLM: case op::AndNLM:
{ {
formula rewrite = rewrite_and_nlm(f); formula rewrite = rewrite_and_nlm(f);
return expansion(rewrite, d, owner, opts); return rec(rewrite);
} }
case op::first_match: case op::first_match:
{ {
auto exps = expansion(f[0], d, owner, opts); auto exps = rec(f[0]);
ExpansionBuilder res(d); ExpansionBuilder res(d);
for (const auto& [bdd_l, form] : exps) for (const auto& [bdd_l, form] : exps)
@ -673,10 +673,11 @@ namespace spot
res.insert(bdd_l, form); res.insert(bdd_l, form);
} }
res.finalize(true, [](formula f){ res.finalize(true);
return formula::first_match(f); auto res2 = res.result();
}); for (auto& [_, dest] : res2)
return res.result(); dest = formula::first_match(dest);
return res2;
} }
case op::Fusion: case op::Fusion:
@ -685,9 +686,9 @@ namespace spot
formula E = f[0]; formula E = f[0];
formula F = f.all_but(0); formula F = f.all_but(0);
expansion_t Ei = expansion(E, d, owner, opts); expansion_t Ei = rec(E);
// TODO: std::option // TODO: std::option
expansion_t Fj = expansion(F, d, owner, opts); expansion_t Fj = rec(F);
for (const auto& [li, ei] : Ei) for (const auto& [li, ei] : Ei)
{ {
@ -709,7 +710,7 @@ namespace spot
ExpansionBuilder res(d); ExpansionBuilder res(d);
for (const auto& sub_f : f) for (const auto& sub_f : f)
{ {
auto exps = expansion(sub_f, d, owner, opts); auto exps = rec(sub_f);
if (exps.empty()) if (exps.empty())
{ {
@ -750,7 +751,7 @@ namespace spot
ExpansionBuilder res(d); ExpansionBuilder res(d);
for (const auto& sub_f : f) for (const auto& sub_f : f)
{ {
auto exps = expansion(sub_f, d, owner, opts); auto exps = rec(sub_f);
if (exps.empty()) if (exps.empty())
continue; continue;

6
spot/tl/expansions.hh
View file

@ -32,14 +32,10 @@ namespace spot
{ {
using expansion_t = std::map<bdd, formula, bdd_less_than>; using expansion_t = std::map<bdd, formula, bdd_less_than>;
formula formula_identity(formula f)
{
return f;
}
struct exp_opts struct exp_opts
{ {
enum expand_opt { enum expand_opt {
None = 0,
Deterministic = 1, Deterministic = 1,
Basic = 2, Basic = 2,
MergeSuffix = 4, MergeSuffix = 4,