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

expansions: fixes + BDD encode changes + printer

Browse source
This commit is contained in:
Antoine Martin 2023-07-04 07:21:20 +02:00
parent f5574547ce
commit 84d3977c0d
2 changed files with 74 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

98
spot/tl/expansions.cc
View file

@ -106,41 +106,63 @@ namespace spot
class bdd_finalizer class bdd_finalizer
{ {
public: public:
bdd_finalizer(std::multimap<bdd, formula, bdd_less_than>& exp, bdd_dict_ptr d, bool opt_sigma_star) int encode(formula f)
: anon_set_(bddtrue)
, d_(d)
, opt_sigma_star_(opt_sigma_star)
{
for (const auto& [prefix, suffix] : exp)
{ {
int anon_var_num; bool is_anon = false;
auto it = formula2bdd_.find(suffix); int var_num;
auto it = formula2bdd_.find(f);
if (it != formula2bdd_.end()) if (it != formula2bdd_.end())
{ {
anon_var_num = it->second; var_num = it->second;
} }
else else
{ {
if (opt_sigma_star_ && (suffix.is(op::Star) if (opt_sigma_star_ && (f.is(op::Star)
&& suffix[0].is(op::tt) && f[0].is(op::tt)
&& suffix.min() == 0 && f.min() == 0
&& suffix.max() == formula::unbounded())) && f.max() == formula::unbounded()))
{ {
anon_var_num = -1; 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 else
{ {
anon_var_num = d_->register_anonymous_variables(1, this); var_num = d_->register_anonymous_variables(1, this);
is_anon = true;
} }
formula2bdd_.insert({suffix, anon_var_num}); formula2bdd_.insert({f, var_num});
bdd2formula_.insert({anon_var_num, suffix}); bdd2formula_.insert({var_num, f});
} }
bdd var = bddtrue; bdd var = bdd_ithvar(var_num);
if (anon_var_num != -1)
var = bdd_ithvar(anon_var_num); if (is_anon)
anon_set_ &= var; anon_set_ &= var;
return var_num;
}
bdd_finalizer(std::multimap<bdd, formula, bdd_less_than>& 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; exp_ |= prefix & var;
} }
} }
@ -160,6 +182,7 @@ namespace spot
std::map<int, formula> bdd2formula_; std::map<int, formula> bdd2formula_;
bdd_dict_ptr d_; bdd_dict_ptr d_;
bool opt_sigma_star_; bool opt_sigma_star_;
bool opt_bdd_encode_;
formula var_to_formula(int var); formula var_to_formula(int var);
formula conj_bdd_to_sere(bdd b); formula conj_bdd_to_sere(bdd b);
@ -249,7 +272,8 @@ namespace spot
{ {
bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_); bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
bdd or_labels = bdd_exist(exp_, anon_set_); bdd or_labels = bdd_exist(exp_, anon_set_);
for (bdd letter: minterms_of(exp_, prop_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); bdd dest_bdd = bdd_restrict(exp_, letter);
formula dest = bdd_to_sere(dest_bdd); formula dest = bdd_to_sere(dest_bdd);
@ -282,7 +306,7 @@ namespace spot
if (opts & (exp_opts::expand_opt::BddIsop if (opts & (exp_opts::expand_opt::BddIsop
| exp_opts::expand_opt::BddMinterm)) | exp_opts::expand_opt::BddMinterm))
{ {
bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar); bdd_finalizer bddf(exp, d, opts & exp_opts::expand_opt::BddSigmaStar, opts & exp_opts::expand_opt::BddEncode);
exp = bddf.simplify(opts); exp = bddf.simplify(opts);
} }
@ -365,6 +389,14 @@ namespace spot
return formula::OrRat(res); return formula::OrRat(res);
} }
void print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict)
{
for (const auto& [prefix, suffix] : exp)
{
std::cout << bdd_to_formula(prefix, dict) << ": " << suffix << std::endl;
}
}
expansion_t expansion_t
expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts) expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts)
@ -581,15 +613,26 @@ namespace spot
} }
exp_t new_res; exp_t new_res;
bool inserted = false;
for (const auto& [l_key, l_val] : exps) for (const auto& [l_key, l_val] : exps)
{ {
for (const auto& [r_key, r_val] : res) for (const auto& [r_key, r_val] : res)
{ {
if ((l_key & r_key) != bddfalse) if ((l_key & r_key) != bddfalse)
new_res.insert({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})}); {
new_res.insert({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); res = std::move(new_res);
} }
@ -671,14 +714,15 @@ namespace spot
aut->set_init_state(init_state); aut->set_init_state(init_state);
formula2state.insert({ f, init_state }); formula2state.insert({ f, init_state });
if (signature_merge)
signature2state.insert({ {f.accepts_eword(), expansion(f, d, aut.get(), opts)}, init_state});
auto f_aps = formula_aps(f); auto f_aps = formula_aps(f);
for (auto& ap : f_aps) for (auto& ap : f_aps)
aut->register_ap(ap); aut->register_ap(ap);
if (signature_merge)
signature2state.insert({ {f.accepts_eword(), expansion(f, d, aut.get(), opts)}, init_state});
auto todo = std::vector<std::pair<formula, unsigned>>(); auto todo = std::vector<std::pair<formula, unsigned>>();
todo.push_back({f, init_state}); todo.push_back({f, init_state});

3
spot/tl/expansions.hh
View file

@ -59,4 +59,7 @@ namespace spot
SPOT_API formula SPOT_API formula
expansion_to_formula(expansion_t e, bdd_dict_ptr& d); expansion_to_formula(expansion_t e, bdd_dict_ptr& d);
SPOT_API void
print_expansion(const expansion_t& exp, const bdd_dict_ptr& dict);
} }