From 50e99cdca78bbc8409190d1c6af75fa5c342e380 Mon Sep 17 00:00:00 2001 From: Alexandre GBAGUIDI AISSE Date: Sat, 17 Jun 2017 21:06:31 +0200 Subject: [PATCH] twaalgos/totgba: Add dnf_to_streett() method * NEWS: Update. * spot/twaalgos/totgba.hh: Declare dnf_to_streett(). * spot/twaalgos/totgba.cc: Implement dnf_to_streett(). * bin/autfilt.cc: Add --dnf-to-streett cmd line option. * tests/core/dnfstreett.test: Add test. * tests/Makefile.am: Add test file. --- NEWS | 9 + bin/autfilt.cc | 11 + spot/twaalgos/totgba.cc | 403 +++++++++++++++++++++++++++++++++++++ spot/twaalgos/totgba.hh | 36 ++++ tests/Makefile.am | 3 +- tests/core/dnfstreett.test | 97 +++++++++ 6 files changed, 558 insertions(+), 1 deletion(-) create mode 100644 tests/core/dnfstreett.test diff --git a/NEWS b/NEWS index 3745c5629..9d5f3ee47 100644 --- a/NEWS +++ b/NEWS @@ -9,6 +9,10 @@ New in spot 2.4.0.dev (not yet released) --ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) --ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) + - autfilt learned --streett-like to convert an automaton in order to + have a Streett-like acceptance condition. It only works with + ω-automata having an acceptance in disjunctive normal form. + Library: - Rename three methods of spot::scc_info. New names are clearer. The @@ -26,6 +30,11 @@ New in spot 2.4.0.dev (not yet released) recognize more if the original language can not be expressed with a co-Büchi acceptance condition. + - The new function dnf_to_streett() is able to convert any automaton + with an acceptance condition in Disjunctive Normal Form to a + Streett-like automaton. This is used by the new option + '--streett-like' of autfilt. + Deprecation notices: (These functions still work but compilers emit warnings.) diff --git a/bin/autfilt.cc b/bin/autfilt.cc index fd81c51af..29cb9f342 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -142,6 +142,7 @@ enum { OPT_SIMPLIFY_EXCLUSIVE_AP, OPT_SPLIT_EDGES, OPT_STATES, + OPT_STREETT_LIKE, OPT_STRIPACC, OPT_SUM_OR, OPT_SUM_AND, @@ -275,6 +276,9 @@ static const argp_option options[] = "initial state. Implies --remove-unreachable-states.", 0 }, { "dnf-acceptance", OPT_DNF_ACC, nullptr, 0, "put the acceptance condition in Disjunctive Normal Form", 0 }, + { "streett-like", OPT_STREETT_LIKE, nullptr, 0, + "convert to an automaton with Streett-like acceptance. Works only with " + "acceptance condition in DNF", 0 }, { "cnf-acceptance", OPT_CNF_ACC, nullptr, 0, "put the acceptance condition in Conjunctive Normal Form", 0 }, { "remove-fin", OPT_REM_FIN, nullptr, 0, @@ -520,6 +524,7 @@ static int opt_highlight_nondet_states = -1; static int opt_highlight_nondet_edges = -1; static bool opt_highlight_languages = false; static bool opt_dca = false; +static bool opt_streett_like = false; static spot::twa_graph_ptr ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false) @@ -622,6 +627,9 @@ parse_opt(int key, char* arg, struct argp_state*) opt_dnf_acc = true; opt_cnf_acc = false; break; + case OPT_STREETT_LIKE: + opt_streett_like = true; + break; case OPT_EDGES: opt_edges = parse_range(arg, 0, std::numeric_limits::max()); break; @@ -1205,6 +1213,9 @@ namespace if (opt_dca) aut = spot::to_dca(aut, false); + if (opt_streett_like) + aut = spot::dnf_to_streett(aut); + if (opt_simplify_exclusive_ap && !opt->excl_ap.empty()) aut = opt->excl_ap.constrain(aut, true); else if (opt_rem_unused_ap) // constrain(aut, true) already does that diff --git a/spot/twaalgos/totgba.cc b/spot/twaalgos/totgba.cc index ea8f981ac..f28a7cc05 100644 --- a/spot/twaalgos/totgba.cc +++ b/spot/twaalgos/totgba.cc @@ -25,8 +25,411 @@ #include #include +#define DEBUG 0 +#if DEBUG +#define debug std::cerr +#else +#define debug while (0) std::cerr +#endif + namespace spot { + namespace + { + class dnf_to_streett_converter + { + private: + typedef std::pair mark_pair; + + const const_twa_graph_ptr& in_; // The given aut. + scc_info si_; // SCC information. + unsigned nb_scc_; // Number of SCC. + unsigned max_set_in_; // Max acc. set nb of in_. + bool state_based_; // Is in_ state_based ? + unsigned init_st_in_; // Initial state of in_. + bool init_reachable_; // Init reach from itself? + twa_graph_ptr res_; // Resulting automaton. + acc_cond::mark_t all_fin_; // All acc. set marked as + // Fin. + acc_cond::mark_t all_inf_; // All acc. set marked as + // Inf. + unsigned num_sets_res_; // Future nb of acc. set. + std::vector all_clauses_; // All clauses. + std::vector set_to_keep_; // Set to keep for each clause + std::vector set_to_add_; // New set for each clause. + acc_cond::mark_t all_set_to_add_; // All new set to add. + std::vector assigned_sets_; // Set that will be add. + std::vector> acc_clauses_; // Acc. clauses. + unsigned res_init_; // Future initial st. + + // A state can be copied at most as many times as their are clauses for + // which it is not rejecting and must be copied one time (to remain + // consistent with the recognized language). This vector records each + // created state following this format: + // st_repr_[orig_st_nb] gives a vector>. + std::vector>> st_repr_; + + // Split the DNF acceptance condition and get all the sets used in each + // clause. It separates those that must be seen finitely often from + // those that must be seen infinitely often. + void + split_dnf_clauses(const acc_cond::acc_code& code) + { + bool one_conjunction = false; + const acc_cond::acc_op root_op = code.back().sub.op; + auto s = code.back().sub.size; + while (s) + { + --s; + if (code[s].sub.op == acc_cond::acc_op::And + || ((one_conjunction = root_op == acc_cond::acc_op::And))) + { + debug << "WABA" << std::endl; + s = one_conjunction ? s + 1 : s; + const unsigned short size = code[s].sub.size; + acc_cond::mark_t fin = 0u; + acc_cond::mark_t inf = 0u; + for (unsigned i = 1; i <= size; i += 2) + { + if (code[s-i].sub.op == acc_cond::acc_op::Fin) + fin |= code[s-i-1].mark; + else if (code[s-i].sub.op == acc_cond::acc_op::Inf) + inf |= code[s-i-1].mark; + else + SPOT_UNREACHABLE(); + } + all_clauses_.emplace_back(fin, inf); + set_to_keep_.emplace_back(fin | inf); + s -= size; + } + else if (code[s].sub.op == acc_cond::acc_op::Fin) // Fin + { + auto m1 = code[--s].mark; + for (unsigned int s : m1.sets()) + { + all_clauses_.emplace_back(acc_cond::mark_t({s}), 0u); + set_to_keep_.emplace_back(acc_cond::mark_t({s})); + } + } + else if (code[s].sub.op == acc_cond::acc_op::Inf) // Inf + { + auto m2 = code[--s].mark; + all_clauses_.emplace_back(0u, m2); + set_to_keep_.emplace_back(m2); + } + else + { + SPOT_UNREACHABLE(); + } + } +#if DEBUG + debug << "\nPrinting all clauses\n"; + for (unsigned i = 0; i < all_clauses_.size(); ++i) + { + debug << i << " Fin:" << all_clauses_[i].first << " Inf:" + << all_clauses_[i].second << std::endl; + } +#endif + } + + // Compute all the acceptance sets that will be needed: + // -Inf(x) will be converted to (Inf(x) | Fin(y)) with y appearing + // on every edge. + // -Fin(x) will be converted to (Inf(y) | Fin(x)) with y appearing + // nowhere. + // + // All the previous 'y' are the new sets assigned. + void + assign_new_sets() + { + unsigned int next_set = 0; + unsigned int missing_set = -1U; + assigned_sets_.resize(max_set_in_, -1U); + + acc_cond::mark_t all_m = all_fin_ | all_inf_; + for (unsigned set = 0; set < max_set_in_; ++set) + if (all_fin_.has(set)) + { + if ((int)missing_set < 0) + { + while (all_m & acc_cond::mark_t({next_set})) + ++next_set; + missing_set = next_set++; + } + + assigned_sets_[set] = missing_set; + } + else if (all_inf_.has(set)) + { + while (all_m & acc_cond::mark_t({next_set})) + ++next_set; + + assigned_sets_[set] = next_set++; + } + + num_sets_res_ = next_set > max_set_in_ ? next_set : max_set_in_; + } + + // Precompute: + // -the sets to add for each clause, + // -all sets to add. + void + find_set_to_add() + { + assign_new_sets(); + + unsigned nb_clause = all_clauses_.size(); + for (unsigned clause = 0; clause < nb_clause; ++clause) + { + if (all_clauses_[clause].second) + { + acc_cond::mark_t m = 0u; + for (unsigned set = 0; set < max_set_in_; ++set) + if (all_clauses_[clause].second.has(set)) + { + assert((int)assigned_sets_[set] >= 0); + m |= acc_cond::mark_t({assigned_sets_[set]}); + } + set_to_add_.push_back(m); + } + else + { + set_to_add_.emplace_back(0u); + } + } + + all_set_to_add_ = 0u; + for (unsigned s = 0; s < max_set_in_; ++s) + if (all_inf_.has(s)) + { + assert((int)assigned_sets_[s] >= 0); + all_set_to_add_.set(assigned_sets_[s]); + } + } + + // Check whether the initial state is reachable from itself. + bool + is_init_reachable() + { + for (const auto& e : in_->edges()) + for (unsigned d : in_->univ_dests(e)) + if (d == init_st_in_) + return true; + return false; + } + + // Get all non rejecting scc for each clause of the acceptance + // condition. Actually, for each clause, an scc will be kept if it + // contains all the 'Inf' acc. sets of the clause. + void + find_probably_accepting_scc(std::vector>& res) + { + res.resize(nb_scc_); + unsigned nb_clause = all_clauses_.size(); + for (unsigned scc = 0; scc < nb_scc_; ++scc) + { + if (si_.is_rejecting_scc(scc)) + continue; + + acc_cond::mark_t acc = si_.acc_sets_of(scc); + for (unsigned clause = 0; clause < nb_clause; ++clause) + { + if ((acc & all_clauses_[clause].second) + == all_clauses_[clause].second) + res[scc].push_back(clause); + } + } +#if DEBUG + debug << "accepting clauses" << std::endl; + for (unsigned i = 0; i < res.size(); ++i) + { + debug << "scc(" << i << ") --> "; + for (auto elt : res[i]) + debug << elt << ','; + debug << std::endl; + } + debug << std::endl; +#endif + } + + // Add all possible representatives of the original state provided. + // Actually, this state will be copied as many times as there are clauses + // for which its SCC is not rejecting. + void + add_state(unsigned st) + { + debug << "add_state(" << st << ')' << std::endl; + if (st_repr_[st].empty()) + { + unsigned st_scc = si_.scc_of(st); + if (st == init_st_in_ && !init_reachable_) + st_repr_[st].emplace_back(-1U, res_init_); + + else if (!acc_clauses_[st_scc].empty()) + for (const auto& clause : acc_clauses_[st_scc]) + st_repr_[st].emplace_back(clause, res_->new_state()); + + else + st_repr_[st].emplace_back(-1U, res_->new_state()); + debug << "added" << std::endl; + } + } + + // Compute the mark that will be set (instead of the provided e_acc) + // according to the current clause in process. This function is only + // called for accepting SCC. + acc_cond::mark_t + get_edge_mark(const acc_cond::mark_t& e_acc, + unsigned clause) + { + assert((int)clause >= 0); + return (e_acc & set_to_keep_[clause]) | set_to_add_[clause]; + } + + // Set the acceptance condition once the resulting automaton is ready. + void + set_acc_condition() + { + acc_cond::acc_code p_code; + for (unsigned set = 0; set < max_set_in_; ++set) + { + if (all_fin_.has(set)) + p_code &= + acc_cond::acc_code::inf(acc_cond::mark_t({assigned_sets_[set]})) + | acc_cond::acc_code::fin(acc_cond::mark_t({set})); + else if (all_inf_.has(set)) + p_code &= + acc_cond::acc_code::inf(acc_cond::mark_t({set})) + | acc_cond::acc_code::fin( + acc_cond::mark_t({assigned_sets_[set]})); + } + res_->set_acceptance(num_sets_res_, p_code); + } + + public: + dnf_to_streett_converter(const const_twa_graph_ptr& in, + const acc_cond::acc_code& code) + : in_(in), + si_(scc_info(in)), + nb_scc_(si_.scc_count()), + max_set_in_(code.used_sets().max_set()), + state_based_(in->prop_state_acc() == true), + init_st_in_(in->get_init_state_number()), + init_reachable_(is_init_reachable()) + { + debug << "State based ? " << state_based_ << std::endl; + std::tie(all_inf_, all_fin_) = code.used_inf_fin_sets(); + split_dnf_clauses(code); + find_set_to_add(); + find_probably_accepting_scc(acc_clauses_); + } + + ~dnf_to_streett_converter() + {} + + twa_graph_ptr run(bool original_states) + { + res_ = make_twa_graph(in_->get_dict()); + res_->copy_ap_of(in_); + st_repr_.resize(in_->num_states()); + res_init_ = res_->new_state(); + res_->set_init_state(res_init_); + + for (unsigned scc = 0; scc < nb_scc_; ++scc) + { + bool rej_scc = acc_clauses_[scc].empty(); + for (auto st : si_.states_of(scc)) + { + add_state(st); + for (const auto& e : in_->out(st)) + { + debug << "working_on_edge(" << st << ',' << e.dst << ')' + << std::endl; + + add_state(e.dst); + bool same_scc = scc == si_.scc_of(e.dst); + + if (st == init_st_in_) + { + for (const auto& p_dst : st_repr_[e.dst]) + res_->new_edge(res_init_, p_dst.second, e.cond, 0u); + if (!init_reachable_) + continue; + } + + if (!rej_scc) + for (const auto& p_src : st_repr_[st]) + for (const auto& p_dst : st_repr_[e.dst]) + { + debug << "repr(" << p_src.second << ',' + << p_dst.second << ')' << std::endl; + + if (same_scc && p_src.first == p_dst.first) + res_->new_edge(p_src.second, p_dst.second, e.cond, + get_edge_mark(e.acc, p_src.first)); + + else if (!same_scc) + res_->new_edge(p_src.second, p_dst.second, e.cond, + state_based_ ? + get_edge_mark(e.acc, p_src.first) + : 0u); + } + else + { + assert(st_repr_[st].size() == 1); + unsigned src = st_repr_[st][0].second; + + acc_cond::mark_t m = 0u; + if (same_scc || state_based_) + m = all_set_to_add_; + + for (const auto& p_dst : st_repr_[e.dst]) + res_->new_edge(src, p_dst.second, e.cond, m); + } + } + } + } + + // Mapping between each state of the resulting automaton and the + // original state of the input automaton. + if (original_states) + { + auto orig_states = new std::vector(); + orig_states->resize(res_->num_states(), -1U); + res_->set_named_prop("original-states", orig_states); + unsigned orig_num_states = in_->num_states(); + for (unsigned orig = 0; orig < orig_num_states; ++orig) + for (const auto& p : st_repr_[orig]) + (*orig_states)[p.second] = orig; +#if DEBUG + for (unsigned i = 1; i < orig_states->size(); ++i) + assert((int)(*orig_states)[i] >= 0); +#endif + } + + set_acc_condition(); + res_->prop_state_acc(state_based_); + return res_; + } + }; + } + + + twa_graph_ptr + dnf_to_streett(const const_twa_graph_ptr& in, bool original_states) + { + const acc_cond::acc_code& code = in->get_acceptance(); + if (!code.is_dnf()) + throw std::runtime_error("dnf_to_streett() should only be" + " called on automata with DNF acceptance"); + if (code.is_t() || code.is_f() || in->acc().is_streett() > 0) + return make_twa_graph(in, twa::prop_set::all()); + + dnf_to_streett_converter dnf_to_streett(in, code); + return dnf_to_streett.run(original_states); + } + + namespace { struct st2gba_state diff --git a/spot/twaalgos/totgba.hh b/spot/twaalgos/totgba.hh index 07d5ebfd1..0dbc70c3d 100644 --- a/spot/twaalgos/totgba.hh +++ b/spot/twaalgos/totgba.hh @@ -21,6 +21,8 @@ #include +#include + namespace spot { /// \brief Take an automaton with any acceptance condition and return @@ -66,4 +68,38 @@ namespace spot SPOT_API twa_graph_ptr to_generalized_streett(const const_twa_graph_ptr& aut, bool share_fin = false); + + /// \brief Converts any DNF acceptance condition into Streett-like. + /// + /// This function is an optimized version of the construction described + /// by Lemma 4 and 5 of the paper below. + /** \verbatim + @Article{boker.2009.lcs, + author = {Udi Boker and Orna Kupferman}, + title = {Co-Büching Them All}, + booktitle = {Foundations of Software Science and Computational + Structures - 14th International Conference, FOSSACS 2011} + year = {2011}, + pages = {184--198}, + url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} + } + \endverbatim */ + /// + /// In the described construction, as many copies as there are minterms in + /// the acceptance condition are made and the union of all those copies is + /// returned. + /// Instead of cloning the automaton for each minterm and end up with many + /// rejecting and useless SCC, we construct the automaton SCC by SCC. Each SCC + /// is copied at most as many times as there are minterms for which it is not + /// rejecting and at least one time if it is always rejecting (to be + /// consistent with the recognized language). + /// + /// \a aut The automaton to convert. + /// \a original_states Enable mapping between each state of the resulting + /// automaton and the original state of the input automaton. This is stored + /// in the "original-states" named property of the produced automaton. Call + /// `aut->get_named_prop>("original-states")` + /// to retrieve it. + SPOT_API twa_graph_ptr + dnf_to_streett(const const_twa_graph_ptr& aut, bool original_states = false); } diff --git a/tests/Makefile.am b/tests/Makefile.am index 79e3bdd42..9122d38cb 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -300,7 +300,8 @@ TESTS_twa = \ core/randpsl.test \ core/cycles.test \ core/acc_word.test \ - core/dca.test + core/dca.test \ + core/dnfstreett.test ############################## PYTHON ############################## diff --git a/tests/core/dnfstreett.test b/tests/core/dnfstreett.test new file mode 100644 index 000000000..ad289cc1e --- /dev/null +++ b/tests/core/dnfstreett.test @@ -0,0 +1,97 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 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 . + +. ./defs +set -e + + +cat >accs << 'EOF' +(Fin(0) & Inf(1)) | Fin(2) +(Fin(0) & Inf(1)) | Inf(2) +(Fin(0) & Fin(1) & Fin(2) & Inf(3)) | Inf(4) | Fin(5) +Rabin1 +Rabin2 +Rabin3 +(Fin(0) & Inf(1)) | (Fin(2) & Fin(3) & Fin(4)) | (Inf(5) & Inf(6) & Inf(7)) +Fin(0) | (Fin(1) & Fin(2) & Inf(3)) | (Inf(4) & Inf(5) & Fin(6)) +Fin(0) | Inf(1) | Inf(2) | Fin(3) +EOF + +while read line +do + randaut -A "$line" a b c > input.hoa + autfilt --streett-like input.hoa > res.hoa + autfilt input.hoa --equivalent-to='res.hoa' + autfilt --complement input.hoa > input_comp.hoa + autfilt --complement res.hoa > res_comp.hoa + autfilt input_comp.hoa --equivalent-to='res_comp.hoa' +done < accs + +cat >random_ltl<< 'EOF' +F(a R !c) +XXF(a R b) +FG(Xa xor !(a W c)) +XX(1 U ((X(b W a) M 1) R c)) +(b | GFXb) -> (a xor b) +F(!a R c) | (b <-> XX(!Gb R b)) +X!G(0 R (b M 1)) +XF((Fc <-> (!b W c)) <-> (Gc M 1)) +F((!b | FGc) -> (b W (!c <-> Xc))) +((a xor b) -> a) U (Ga & (b R c)) +F((a M Xc) | FG(Xb <-> X(b | c))) +XFG!a +((b R c) | F!XGF(b | c)) R !b +Xc U Ga +(Fa & Xc) | G(b U Ga) +X!(((c <-> (!a M b)) W 0) W 0) +b U (c W Fa) +F(Xa W (b xor (Ga U !Xb))) +!(G(c R Gc) U X(Fc W !Xb)) +F(0 R (c W a)) +EOF +ltlcross -F random_ltl \ + --timeout=60 \ + '{1} ltl2tgba %f | autfilt --gra >%T' \ + '{2} ltl2tgba %f | autfilt --gra | autfilt --streett-like >%T' + +cat >input.hoa<< 'EOF' +HOA: v1 +States: 4 +Start: 0 +AP: 2 "a" "b" +Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)) +--BODY-- +State: 0 +[!0&!1] 3 +[!0&!1] 1 +State: 1 +[0&1] 2 {1 2 4} +State: 2 +[0&1] 1 +State: 3 +[!0&1] 0 {0 3 5} +[!0&!1] 2 {1 2 4} +--END-- +EOF +autfilt --streett-like input.hoa > res.hoa +autfilt input.hoa --equivalent-to='res.hoa' +autfilt --complement input.hoa > input_comp.hoa +autfilt --complement res.hoa > res_comp.hoa +autfilt input_comp.hoa --equivalent-to='res_comp.hoa' -- GitLab