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

expansions: latest implementation

Browse source
This commit is contained in:
Antoine Martin 2023-03-06 18:37:12 +01:00
parent 22f76b7e1c
commit 0168efea60
2 changed files with 576 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

560
spot/tl/expansions.cc
View file

@ -548,6 +548,471 @@ namespace spot
return formula::OrRat(res);
}
class bdd_finalizer
{
public:
bdd_finalizer(std::multimap<bdd, formula, bdd_less_than>& exp, bdd_dict_ptr d)
: anon_set_(bddtrue)
, d_(d)
{
for (const auto& [prefix, suffix] : exp)
{
int anon_var_num;
auto it = formula2bdd_.find(suffix);
if (it != formula2bdd_.end())
{
anon_var_num = it->second;
}
else
{
anon_var_num = d_->register_anonymous_variables(1, this);
formula2bdd_.insert({suffix, anon_var_num});
bdd2formula_.insert({anon_var_num, suffix});
}
bdd var = bdd_ithvar(anon_var_num);
anon_set_ &= var;
exp_ |= prefix & var;
}
}
~bdd_finalizer()
{
d_->unregister_all_my_variables(this);
}
std::multimap<bdd, formula, bdd_less_than>
simplify(exp_opts_new::expand_opt_new opts);
private:
bdd exp_;
bdd anon_set_;
std::map<formula, int> formula2bdd_;
std::map<int, formula> bdd2formula_;
bdd_dict_ptr d_;
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<formula> 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)
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<formula> 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));
}
std::multimap<bdd, formula, bdd_less_than>
bdd_finalizer::simplify(exp_opts_new::expand_opt_new opts)
{
std::multimap<bdd, formula, bdd_less_than> res;
if (opts & exp_opts_new::expand_opt_new::BddMinterm)
{
bdd prop_set = bdd_exist(bdd_support(exp_), anon_set_);
bdd or_labels = bdd_exist(exp_, anon_set_);
for (bdd letter: minterms_of(exp_, prop_set))
{
bdd dest_bdd = bdd_restrict(exp_, letter);
formula dest = bdd_to_sere(dest_bdd);
auto it = res.insert({letter, dest});
assert(it.second);
(void) it;
}
}
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.insert({letter, dest});
}
}
return res;
}
void
finalize_new(std::multimap<bdd, formula, bdd_less_than>& exp, exp_opts_new::expand_opt_new opts, bdd_dict_ptr d)
{
if (opts & (exp_opts_new::expand_opt_new::BddIsop
| exp_opts_new::expand_opt_new::BddMinterm))
{
bdd_finalizer bddf(exp, d);
exp = bddf.simplify(opts);
}
if (opts & exp_opts_new::expand_opt_new::UniqueSuffix)
{
std::map<formula, bdd> 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_new::expand_opt_new::UniquePrefix)
{
std::map<bdd, formula, bdd_less_than> 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});
}
}
exp.clear();
for (const auto [prefix, suffix] : unique_map)
{
exp.insert({prefix, suffix});
}
}
}
std::multimap<bdd, formula, bdd_less_than>
expansion_new(formula f, const bdd_dict_ptr& d, void *owner, exp_opts_new::expand_opt_new opts)
{
using exp_t = std::multimap<bdd, formula, bdd_less_than>;
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](formula f){
return expansion_new(f, d, owner, exp_opts_new::None);
};
switch (f.kind())
{
case op::ff:
case op::tt:
case op::ap:
SPOT_UNREACHABLE();
case op::eword:
return {{bddfalse, formula::ff()}};
case op::Concat:
{
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.insert({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.insert({bdd_l, form});
}
}
finalize_new(res, opts, d);
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.insert({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.insert({li & ki, fi});
}
}
}
if (f.min() == 0)
res.insert({bddtrue, formula::eword()});
finalize_new(res, opts, d);
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.insert({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})});
}
finalize_new(res, opts, d);
return res;
}
case op::AndNLM:
{
formula rewrite = rewrite_and_nlm(f);
auto res = rec(rewrite);
finalize_new(res, opts, d);
return res;
}
case op::first_match:
{
auto exps = rec(f[0]);
exp_t res;
for (const auto& [bdd_l, form] : exps)
{
res.insert({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)
{
finalize_new(res, opts, d);
return res;
}
exp_t res_det;
std::vector<formula> 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.insert({l, or_dests});
dests.clear();
}
for (auto& [_, dest] : res_det)
dest = formula::first_match(dest);
finalize_new(res_det, opts, d);
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.insert({li & kj, fj});
}
res.insert({li, formula::Fusion({ei, F})});
}
finalize_new(res, opts, d);
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;
for (const auto& [l_key, l_val] : exps)
{
for (const auto& [r_key, r_val] : res)
{
if ((l_key & r_key) != bddfalse)
new_res.insert({l_key & r_key, formula::multop(f.kind(), {l_val, r_val})});
}
}
res = std::move(new_res);
}
finalize_new(res, opts, d);
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.insert({label, dest});
}
finalize_new(res, opts, d);
return res;
}
default:
std::cerr << "unimplemented kind "
<< static_cast<int>(f.kind())
<< std::endl;
SPOT_UNIMPLEMENTED();
}
return {};
}
std::multimap<bdd, formula, bdd_less_than>
expansion_simple(formula f, const bdd_dict_ptr& d, void *owner)
{
@ -1031,12 +1496,13 @@ namespace spot
expansion_t
expansion(formula f, const bdd_dict_ptr& d, void *owner, exp_opts::expand_opt opts)
{
if (opts & exp_opts::Basic)
return expansion_impl<expansion_basic>(f, d, owner, opts);
if (opts & exp_opts::Bdd)
return expansion_impl<expansion_bdd>(f, d, owner, opts);
else if (opts & exp_opts::MergeSuffix)
return expansion_impl<expansion_merge_formulas>(f, d, owner, opts);
else // exp_opts::Bdd
return expansion_impl<expansion_bdd>(f, d, owner, opts);
else // exp_opts::Basic
return expansion_impl<expansion_basic>(f, d, owner, opts);
}
twa_graph_ptr
@ -1210,4 +1676,90 @@ namespace spot
aut->merge_edges();
return aut;
}
twa_graph_ptr
expand_new_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts)
{
auto finite = expand_new_finite_automaton(f, d, opts);
return from_finite(finite);
}
twa_graph_ptr
expand_new_finite_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts)
{
auto aut = make_twa_graph(d);
aut->prop_state_acc(true);
const auto acc_mark = aut->set_buchi();
auto formula2state = robin_hood::unordered_map<formula, unsigned>();
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 todo = std::vector<std::pair<formula, unsigned>>();
todo.push_back({f, init_state});
auto state_names = new std::vector<std::string>();
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
{
dst = aut->new_state();
todo.push_back({suffix, dst});
formula2state.insert({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 curr_acc_mark= curr_f.accepts_eword()
? acc_mark
: acc_cond::mark_t();
auto exp = expansion_new(curr_f, d, aut.get(), opts);
for (const auto& [letter, suffix] : exp)
{
if (suffix.is(op::ff))
continue;
auto dst = find_dst(suffix);
aut->new_edge(curr_state, dst, letter, curr_acc_mark);
}
// if state has no transitions and should be accepting, create
// artificial transition
if (aut->get_graph().state_storage(curr_state).succ == 0
&& curr_f.accepts_eword())
aut->new_edge(curr_state, curr_state, bddfalse, acc_mark);
}
aut->set_named_prop("state-names", state_names);
aut->merge_edges();
return aut;
}
}

20
spot/tl/expansions.hh
View file

@ -43,6 +43,26 @@ namespace spot
};
};
struct exp_opts_new
{
enum expand_opt_new {
None = 0,
UniqueSuffix = 1,
UniquePrefix = 2,
BddIsop = 4,
BddMinterm = 8,
};
};
SPOT_API std::multimap<bdd, formula, bdd_less_than>
expansion_new(formula f, const bdd_dict_ptr& d, void *owner, exp_opts_new::expand_opt_new opts);
SPOT_API twa_graph_ptr
expand_new_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts);
SPOT_API twa_graph_ptr
expand_new_finite_automaton(formula f, bdd_dict_ptr d, exp_opts_new::expand_opt_new opts);
SPOT_API twa_graph_ptr
expand_simple_automaton(formula f, bdd_dict_ptr d);