From b9f461c0257bf8eb69eab9d35729f916b301945a Mon Sep 17 00:00:00 2001 From: Antoine Martin Date: Wed, 30 Nov 2022 15:28:49 +0100 Subject: [PATCH] expansions: draft --- python/spot/impl.i | 2 + spot/tl/Makefile.am | 2 + spot/tl/expansions.cc | 418 ++++++++++++++++++++++++++++++++++++++++++ spot/tl/expansions.hh | 46 +++++ tests/Makefile.am | 2 + tests/core/expand.cc | 25 +++ 6 files changed, 495 insertions(+) create mode 100644 spot/tl/expansions.cc create mode 100644 spot/tl/expansions.hh create mode 100644 tests/core/expand.cc diff --git a/python/spot/impl.i b/python/spot/impl.i index 471b85cbb..725655c08 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -88,6 +88,7 @@ #include #include #include +#include #include #include #include @@ -634,6 +635,7 @@ namespace std { %include %include %include +%include %include %include %include diff --git a/spot/tl/Makefile.am b/spot/tl/Makefile.am index 1e5a68363..abb431267 100644 --- a/spot/tl/Makefile.am +++ b/spot/tl/Makefile.am @@ -32,6 +32,7 @@ tl_HEADERS = \ dot.hh \ environment.hh \ exclusive.hh \ + expansions.hh \ formula.hh \ hierarchy.hh \ length.hh \ @@ -58,6 +59,7 @@ libtl_la_SOURCES = \ derive.cc \ dot.cc \ exclusive.cc \ + expansions.cc \ formula.cc \ hierarchy.cc \ length.cc \ diff --git a/spot/tl/expansions.cc b/spot/tl/expansions.cc new file mode 100644 index 000000000..4fb2c91c3 --- /dev/null +++ b/spot/tl/expansions.cc @@ -0,0 +1,418 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#include "config.h" +#include +#include +#include +#include +#include + +namespace spot +{ + namespace + { + static void + insert_or_merge(expansion_t& exp, bdd letter, formula suffix) + { + auto res = exp.insert({letter, suffix}); + if (!res.second) + { + auto it = res.first; + it->second = formula::OrRat({it->second, suffix}); + } + } + + // FIXME: could probably just return a map directly + static std::vector + formula_aps(formula f) + { + auto res = std::unordered_set(); + + f.traverse([&res](formula f) + { + if (f.is(op::ap)) + { + res.insert(f.ap_name()); + return true; + } + + return false; + }); + + return std::vector(res.begin(), res.end()); + } + formula + rewrite_and_nlm(formula f) + { + unsigned s = f.size(); + std::vector final; + std::vector non_final; + + for (auto g: f) + if (g.accepts_eword()) + final.emplace_back(g); + else + non_final.emplace_back(g); + + if (non_final.empty()) + // (a* & b*);c = (a*|b*);c + return formula::OrRat(std::move(final)); + if (!final.empty()) + { + // let F_i be final formulae + // N_i be non final formula + // (F_1 & ... & F_n & N_1 & ... & N_m) + // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) + // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] + formula f = formula::OrRat(std::move(final)); + formula n = formula::AndNLM(std::move(non_final)); + formula t = formula::one_star(); + formula ft = formula::Concat({f, t}); + formula nt = formula::Concat({n, t}); + formula ftn = formula::AndRat({ft, n}); + formula fnt = formula::AndRat({f, nt}); + return formula::OrRat({ftn, fnt}); + } + // No final formula. + // Translate N_1 & N_2 & ... & N_n into + // N_1 && (N_2;[*]) && ... && (N_n;[*]) + // | (N_1;[*]) && N_2 && ... && (N_n;[*]) + // | (N_1;[*]) && (N_2;[*]) && ... && N_n + formula star = formula::one_star(); + std::vector disj; + for (unsigned n = 0; n < s; ++n) + { + std::vector conj; + for (unsigned m = 0; m < s; ++m) + { + formula g = f[m]; + if (n != m) + g = formula::Concat({g, star}); + conj.emplace_back(g); + } + disj.emplace_back(formula::AndRat(std::move(conj))); + } + return formula::OrRat(std::move(disj)); + } + } + + formula + expansion_to_formula(expansion_t e, bdd_dict_ptr& d) + { + std::vector res; + + for (const auto& [key, val] : e) + { + formula prefix = bdd_to_formula(key, d); + res.push_back(formula::Concat({prefix, val})); + } + + return formula::OrRat(res); + } + + expansion_t + expansion(formula f, const bdd_dict_ptr& d, void *owner) + { + if (f.is_boolean()) + { + auto f_bdd = formula_to_bdd(f, d, owner); + + if (f_bdd == bddfalse) + return {}; + + return {{f_bdd, formula::eword()}}; + } + + + 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 = expansion(f[0], d, owner); + + expansion_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 = expansion(f.all_but(0), d, owner); + for (const auto& [bdd_l, form] : exps_rest) + { + insert_or_merge(res, bdd_l, form); + } + } + 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 = expansion(E, d, owner); + expansion_t res; + for (const auto& [li, ei] : exp) + { + insert_or_merge(res, li, formula::Fusion({ei, E_i_j_minus})); + + if (ei.accepts_eword() && f.min() != 0) + { + for (const auto& [ki, fi] : expansion(E_i_j_minus, d, owner)) + { + // FIXME: build bdd once + if ((li & ki) != bddfalse) + insert_or_merge(res, li & ki, fi); + } + } + } + if (f.min() == 0) + insert_or_merge(res, bddtrue, formula::eword()); + + 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 = expansion(f[0], d, owner); + + expansion_t res; + for (const auto& [bdd_l, form] : exps) + { + res.insert({bdd_l, formula::Concat({form, formula::Star(f[0], min, max)})}); + } + + return res; + } + + case op::AndNLM: + { + formula rewrite = rewrite_and_nlm(f); + return expansion(rewrite, d, owner); + } + + case op::first_match: + { + auto exps = expansion(f[0], d, owner); + + expansion_t res; + for (const auto& [bdd_l, form] : exps) + { + res.insert({bdd_l, formula::first_match(form)}); + } + + return res; + } + + case op::Fusion: + { + expansion_t res; + formula E = f[0]; + formula F = f.all_but(0); + + expansion_t Ei = expansion(E, d, owner); + // TODO: std::option + expansion_t Fj = expansion(F, d, owner); + + for (const auto& [li, ei] : Ei) + { + if (ei.accepts_eword()) + { + for (const auto& [kj, fj] : Fj) + if ((li & kj) != bddfalse) + insert_or_merge(res, li & kj, fj); + } + insert_or_merge(res, li, formula::Fusion({ei, F})); + } + + return res; + } + + case op::AndRat: + case op::OrRat: + { + expansion_t res; + for (const auto& sub_f : f) + { + auto exps = expansion(sub_f, d, owner); + + if (exps.empty()) + { + if (f.kind() == op::OrRat) + continue; + + // 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; + } + + expansion_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) + insert_or_merge(new_res, l_key & r_key, formula::multop(f.kind(), {l_val, r_val})); + + if (f.is(op::OrRat)) + { + if ((l_key & !r_key) != bddfalse) + insert_or_merge(new_res, l_key & !r_key, l_val); + + if ((!l_key & r_key) != bddfalse) + insert_or_merge(new_res, !l_key & r_key, r_val); + } + } + } + + res = std::move(new_res); + } + + return res; + } + + default: + std::cerr << "unimplemented kind " + << static_cast(f.kind()) + << std::endl; + SPOT_UNIMPLEMENTED(); + } + + return {}; + } + + twa_graph_ptr + expand_automaton(formula f, bdd_dict_ptr d) + { + auto finite = expand_finite_automaton(f, d); + return from_finite(finite); + } + + twa_graph_ptr + expand_finite_automaton(formula f, bdd_dict_ptr d) + { + auto aut = make_twa_graph(d); + + aut->prop_state_acc(true); + const auto acc_mark = aut->set_buchi(); + + auto formula2state = robin_hood::unordered_map(); + + 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>(); + todo.push_back({f, init_state}); + + auto state_names = new std::vector(); + 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(curr_f, d, aut.get()); + + 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; + } +} diff --git a/spot/tl/expansions.hh b/spot/tl/expansions.hh new file mode 100644 index 000000000..af80d7e8b --- /dev/null +++ b/spot/tl/expansions.hh @@ -0,0 +1,46 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2021 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include + +#include + +#include +#include +#include +#include + +namespace spot +{ + using expansion_t = std::map; + + SPOT_API expansion_t + expansion(formula f, const bdd_dict_ptr& d, void *owner); + + SPOT_API formula + expansion_to_formula(expansion_t e, bdd_dict_ptr& d); + + SPOT_API twa_graph_ptr + expand_automaton(formula f, bdd_dict_ptr d); + + SPOT_API twa_graph_ptr + expand_finite_automaton(formula f, bdd_dict_ptr d); +} diff --git a/tests/Makefile.am b/tests/Makefile.am index 9bf0cef73..a061ba23d 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -69,6 +69,7 @@ check_PROGRAMS = \ core/cube \ core/emptchk \ core/equals \ + core/expand \ core/graph \ core/kind \ core/length \ @@ -111,6 +112,7 @@ core_bricks_SOURCES = core/bricks.cc core_checkpsl_SOURCES = core/checkpsl.cc core_checkta_SOURCES = core/checkta.cc core_emptchk_SOURCES = core/emptchk.cc +core_expand_SOURCES = core/expand.cc core_graph_SOURCES = core/graph.cc core_ikwiad_SOURCES = core/ikwiad.cc core_intvcomp_SOURCES = core/intvcomp.cc diff --git a/tests/core/expand.cc b/tests/core/expand.cc new file mode 100644 index 000000000..a589d6370 --- /dev/null +++ b/tests/core/expand.cc @@ -0,0 +1,25 @@ +#include "config.h" + +#include +#include +#include +#include + +int main(int argc, char** argv) +{ + if (argc != 2) + return 1; + + spot::formula f = spot::parse_infix_sere(argv[1]).f; + auto d = spot::make_bdd_dict(); + + auto m = spot::expansion(f, d, nullptr); + + for (const auto& [bdd_l, form] : m) + std::cout << '[' << bdd_to_formula(bdd_l, d) << ']' << ": " << form << std::endl; + std::cout << "formula: " << expansion_to_formula(m, d) << std::endl; + + d->unregister_all_my_variables(nullptr); + + return 0; +}