diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index 71601d39c..835efc765 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -54,7 +54,7 @@ #include "twaalgos/stripacc.hh" #include "twaalgos/remfin.hh" #include "twaalgos/cleanacc.hh" - +#include "twaalgos/dtgbasat.hh" static const char argp_program_doc[] ="\ Convert, transform, and filter Büchi automata.\v\ @@ -91,6 +91,7 @@ enum { OPT_REM_DEAD, OPT_REM_UNREACH, OPT_REM_FIN, + OPT_SAT_MINIMIZE, OPT_SEED, OPT_SEP_SETS, OPT_SIMPLIFY_EXCLUSIVE_AP, @@ -167,6 +168,10 @@ static const argp_option options[] = { "separate-sets", OPT_SEP_SETS, 0, 0, "if both Inf(x) and Fin(x) appear in the acceptance condition, replace " "Fin(x) by a new Fin(y) and adjust the automaton", 0 }, + { "sat-minimize", OPT_SAT_MINIMIZE, "options", OPTION_ARG_OPTIONAL, + "minimize the automaton using a SAT solver (only work for deterministic" + " automata)", 0 }, + /**************************************************/ { 0, 0, 0, 0, "Filtering options:", 6 }, { "are-isomorphic", OPT_ARE_ISOMORPHIC, "FILENAME", 0, "keep automata that are isomorphic to the automaton in FILENAME", 0 }, @@ -261,6 +266,7 @@ static bool opt_simplify_exclusive_ap = false; static bool opt_rem_dead = false; static bool opt_rem_unreach = false; static bool opt_sep_sets = false; +static const char* opt_sat_minimize = nullptr; static int parse_opt(int key, char* arg, struct argp_state*) @@ -431,6 +437,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_REM_UNREACH: opt_rem_unreach = true; break; + case OPT_SAT_MINIMIZE: + opt_sat_minimize = arg ? arg : ""; + break; case OPT_SEED: opt_seed = to_int(arg); break; @@ -574,6 +583,13 @@ namespace if (opt->product) aut = spot::product(std::move(aut), opt->product); + if (opt_sat_minimize) + { + aut = spot::sat_minimize(aut, opt_sat_minimize); + if (!aut) + return 0; + } + aut = post.run(aut, nullptr); if (randomize_st || randomize_tr) diff --git a/src/misc/optionmap.cc b/src/misc/optionmap.cc index 95ead80bc..d01faa365 100644 --- a/src/misc/optionmap.cc +++ b/src/misc/optionmap.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et +// Copyright (C) 2008, 2013, 2014, 2015 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -84,29 +84,44 @@ namespace spot if (!*options) return name_start; - char* val_end; - int val = strtol(options, &val_end, 10); - if (val_end == options) - return name_start; - - if (*val_end == 'K') + if (*options == '\'' || *options == '"') { - val *= 1024; - ++val_end; + auto sep = *options; + auto start = options + 1; + do + ++options; + while (*options && *options != sep); + if (*options != sep) + return start - 1; + std::string val(start, options); + options_str_[name] = val; + if (*options) + ++options; } - else if (*val_end == 'M') + else { - val *= 1024 * 1024; - ++val_end; - } - else if (*val_end && !strchr(" \t\n,;", *val_end)) - { - return options; - } + char* val_end; + int val = strtol(options, &val_end, 10); + if (val_end == options) + return name_start; - options = val_end; - - options_[name] = val; + if (*val_end == 'K') + { + val *= 1024; + ++val_end; + } + else if (*val_end == 'M') + { + val *= 1024 * 1024; + ++val_end; + } + else if (*val_end && !strchr(" \t\n,;", *val_end)) + { + return options; + } + options = val_end; + options_[name] = val; + } } } return 0; @@ -115,12 +130,15 @@ namespace spot int option_map::get(const char* option, int def) const { - std::map::const_iterator it = options_.find(option); - if (it == options_.end()) - // default value if not declared - return def; - else - return it->second; + auto it = options_.find(option); + return (it == options_.end()) ? def : it->second; + } + + std::string + option_map::get_str(const char* option, std::string def) const + { + auto it = options_str_.find(option); + return (it == options_str_.end()) ? def : it->second; } int @@ -137,12 +155,19 @@ namespace spot return old; } + std::string + option_map::set_str(const char* option, std::string val, std::string def) + { + std::string old = get_str(option, def); + options_str_[option] = val; + return old; + } + void option_map::set(const option_map& o) { - for (std::map::const_iterator it = o.options_.begin(); - it != o.options_.end(); ++it) - options_[it->first] = it->second; + options_ = o.options_; + options_str_ = o.options_str_; } int& @@ -154,9 +179,10 @@ namespace spot std::ostream& operator<<(std::ostream& os, const option_map& m) { - for (std::map::const_iterator it = m.options_.begin(); - it != m.options_.end(); ++it) - os << '"' << it->first << "\" = " << it->second << '\n'; + for (auto p: m.options_) + os << '"' << p.first << "\" = " << p.second << '\n'; + for (auto p: m.options_str_) + os << '"' << p.first << "\" = \"" << p.second << "\"\n"; return os; } } diff --git a/src/misc/optionmap.hh b/src/misc/optionmap.hh index 90bfd4678..751157639 100644 --- a/src/misc/optionmap.hh +++ b/src/misc/optionmap.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Developpement de +// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement de // l'Epita (LRDE) // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -60,6 +60,13 @@ namespace spot /// \see operator[]() int get(const char* option, int def = 0) const; + /// \brief Get the value of \a option. + /// + /// \return The value associated to \a option if it exists, + /// \a def otherwise. + /// \see operator[]() + std::string get_str(const char* option, std::string def = {}) const; + /// \brief Get the value of \a option. /// /// \return The value associated to \a option if it exists, 0 otherwise. @@ -72,6 +79,13 @@ namespace spot /// or \a def otherwise. int set(const char* option, int val, int def = 0); + /// \brief Set the value of a string \a option to \a val. + /// + /// \return The previous value associated to \a option if declared, + /// or \a def otherwise. + std::string set_str(const char* option, + std::string val, std::string def = {}); + /// Acquire all the settings of \a o. void set(const option_map& o); @@ -84,5 +98,6 @@ namespace spot private: std::map options_; + std::map options_str_; }; } diff --git a/src/tests/acc.cc b/src/tests/acc.cc index e1719867f..c9672ffe4 100644 --- a/src/tests/acc.cc +++ b/src/tests/acc.cc @@ -34,6 +34,25 @@ void check(spot::acc_cond& ac, spot::acc_cond::mark_t m) std::cout << '\n'; } +void print(const std::vector>& res) +{ + for (auto& v: res) + { + std::cout << '{'; + const char* comma = ""; + for (int s: v) + { + std::cout << comma; + if (s < 0) + std::cout << '!' << (-s - 1); + else + std::cout << s; + comma = ", "; + } + std::cout << "}\n"; + } +} + int main() { spot::acc_cond ac(4); @@ -128,6 +147,16 @@ int main() code3.append_and(ac.fin({2, 3})); std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n'; + // code3 == (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) + // {0} + // {1} + // {2, 3} + std::cout << code3 << ' ' << "{0} true\n"; + spot::acc_cond::mark_t m = 0U; + m.set(0); + print(code3.missing(m, true)); + std::cout << code3 << ' ' << "{0} false\n"; + print(code3.missing(m, false)); std::cout << spot::parse_acc_code("t") << '\n'; std::cout << spot::parse_acc_code("f") << '\n'; diff --git a/src/tests/acc.test b/src/tests/acc.test index d0b1a766e..742d00ef2 100755 --- a/src/tests/acc.test +++ b/src/tests/acc.test @@ -68,6 +68,12 @@ stripping 2 f 1 9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1 5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0 +(Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) {0} true +{1} +{!2, !3} +(Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) {0} false +{!1, 2} +{!1, 3} t f Fin(2) diff --git a/src/tests/ltl2tgba.cc b/src/tests/ltl2tgba.cc index d2e164b76..77dcd73de 100644 --- a/src/tests/ltl2tgba.cc +++ b/src/tests/ltl2tgba.cc @@ -1278,8 +1278,9 @@ checked_main(int argc, char** argv) else if (opt_dtgbasat >= 0) { tm.start("dtgbasat"); - auto satminimized = dtgba_sat_minimize(ensure_digraph(a), - opt_dtgbasat); + auto satminimized = dtgba_sat_minimize + (ensure_digraph(a), opt_dtgbasat, + spot::acc_cond::generalized_buchi(opt_dtgbasat)); tm.stop("dtgbasat"); if (satminimized) a = satminimized; diff --git a/src/twa/acc.cc b/src/twa/acc.cc index 1b0bdd771..da0509523 100644 --- a/src/twa/acc.cc +++ b/src/twa/acc.cc @@ -293,18 +293,18 @@ namespace spot } } - bool acc_cond::accepting(mark_t inf) const + bool acc_cond::acc_code::accepting(mark_t inf) const { - if (code_.empty()) + if (empty()) return true; - return eval(inf, &code_.back()); + return eval(inf, &back()); } - bool acc_cond::inf_satisfiable(mark_t inf) const + bool acc_cond::acc_code::inf_satisfiable(mark_t inf) const { - if (code_.empty()) + if (empty()) return true; - return inf_eval(inf, &code_.back()); + return inf_eval(inf, &back()); } acc_cond::mark_t acc_cond::accepting_sets(mark_t inf) const @@ -602,6 +602,81 @@ namespace spot return {true, i}; } + std::vector> + acc_cond::acc_code::missing(mark_t inf, bool accepting) const + { + if (empty()) + { + if (accepting) + return {}; + else + return { + {} + }; + } + auto used = acc_cond::acc_code::used_sets(); + unsigned c = used.count(); + + bdd_allocator ba; + int base = ba.allocate_variables(c); + assert(base == 0); + std::vector r; + std::vector sets(c); + bdd known = bddtrue; + for (unsigned i = 0; r.size() < c; ++i) + { + if (used.has(i)) + { + sets[base] = i; + bdd v = bdd_ithvar(base++); + r.push_back(v); + if (inf.has(i)) + known &= v; + } + else + { + r.push_back(bddfalse); + } + } + + bdd res = to_bdd_rec(&back(), &r[0]); + + res = bdd_restrict(res, known); + + if (accepting) + res = !res; + + if (res == bddfalse) + return {}; + + minato_isop isop(res); + bdd cube; + std::vector> result; + while ((cube = isop.next()) != bddfalse) + { + std::vector partial; + while (cube != bddtrue) + { + // The acceptance set associated to this BDD variable + int s = sets[bdd_var(cube)]; + + bdd h = bdd_high(cube); + if (h == bddfalse) // Negative variable + { + partial.push_back(s); + cube = bdd_low(cube); + } + else // Positive variable + { + partial.push_back(-s - 1); + cube = h; + } + } + result.emplace_back(std::move(partial)); + } + return result; + } + bool acc_cond::acc_code::is_dnf() const { if (empty() || size() == 2) diff --git a/src/twa/acc.hh b/src/twa/acc.hh index d759af105..1645d8e03 100644 --- a/src/twa/acc.hh +++ b/src/twa/acc.hh @@ -674,6 +674,18 @@ namespace spot acc_code complement() const; + // Return a list of acceptance marks needed to close a cycle + // that already visit INF infinitely often, so that the cycle is + // accepting (ACCEPTING=true) or rejecting (ACCEPTING=false). + // Positive values describe positive set. + // A negative value x means the set -x-1 must be absent. + std::vector> + missing(mark_t inf, bool accepting) const; + + bool accepting(mark_t inf) const; + + bool inf_satisfiable(mark_t inf) const; + // Remove all the acceptance sets in rem. // // If MISSING is set, the acceptance sets are assumed to be @@ -766,6 +778,14 @@ namespace spot (s == 2 && code_[1].op == acc_op::Inf && code_[0].mark == all_sets()); } + static acc_code generalized_buchi(unsigned n) + { + mark_t m((1U << n) - 1); + if (n == 8 * sizeof(mark_t::value_t)) + m = mark_t(-1U); + return acc_code::inf(m); + } + bool is_buchi() const { unsigned s = code_.size(); @@ -900,11 +920,15 @@ namespace spot return all_; } - bool accepting(mark_t inf) const; + bool accepting(mark_t inf) const + { + return code_.accepting(inf); + } - // Assume all Fin(x) in the condition a true. Would the resulting - // condition (involving only Inf(y)) be satisfiable? - bool inf_satisfiable(mark_t inf) const; + bool inf_satisfiable(mark_t inf) const + { + return code_.inf_satisfiable(inf); + } mark_t accepting_sets(mark_t inf) const; diff --git a/src/twaalgos/complete.hh b/src/twaalgos/complete.hh index 05c6158fa..e44840ad4 100644 --- a/src/twaalgos/complete.hh +++ b/src/twaalgos/complete.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -28,7 +28,7 @@ namespace spot /// If the tgba has no acceptance set, one will be added. The /// returned value is the number of the sink state (it can be a new /// state added for completion, or an existing non-accepting state - /// that has been reused as sink state because it had not outgoing + /// that has been reused as sink state because it had no outgoing /// transitions apart from self-loops.) SPOT_API unsigned tgba_complete_here(twa_graph_ptr aut); diff --git a/src/twaalgos/dtbasat.hh b/src/twaalgos/dtbasat.hh index f13309cda..7553d8258 100644 --- a/src/twaalgos/dtbasat.hh +++ b/src/twaalgos/dtbasat.hh @@ -26,7 +26,7 @@ namespace spot /// \brief Attempt to synthetize an equivalent deterministic TBA /// with a SAT solver. /// - /// \param a the input TGBA. It should have only one acceptance + /// \param a the input TGA. It should have only one acceptance /// set and be deterministic. I.e., it should be a deterministic TBA. /// /// \param target_state_number the desired number of states wanted diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc index 36803a98d..65ad89dca 100644 --- a/src/twaalgos/dtgbasat.cc +++ b/src/twaalgos/dtgbasat.cc @@ -32,7 +32,13 @@ #include "misc/satsolver.hh" #include "misc/timer.hh" #include "isweakscc.hh" +#include "isdet.hh" #include "dotty.hh" +#include "complete.hh" +#include "misc/optionmap.hh" +#include "dtbasat.hh" +#include "sccfilter.hh" +#include "sbacc.hh" // If you set the SPOT_TMPKEEP environment variable the temporary // file used to communicate with the sat solver will be left in @@ -269,7 +275,7 @@ namespace spot // int_map int_to_state; unsigned cand_size; unsigned int cand_nacc; - std::vector cand_acc; // size cand_nacc + acc_cond::acc_code cand_acc; std::vector all_cand_acc; std::vector all_ref_acc; @@ -289,13 +295,11 @@ namespace spot dict& d, bdd ap, bool state_based, scc_info& sm) { bdd_dict_ptr bd = aut->get_dict(); - d.cand_acc.resize(d.cand_nacc); d.cacc.add_sets(d.cand_nacc); d.all_cand_acc.push_back(0U); for (unsigned n = 0; n < d.cand_nacc; ++n) { auto c = d.cacc.mark(n); - d.cand_acc[n] = c; size_t s = d.all_cand_acc.size(); for (size_t i = 0; i < s; ++i) d.all_cand_acc.push_back(d.all_cand_acc[i] | c); @@ -376,7 +380,7 @@ namespace spot // result. for (unsigned n = 0; n < d.cand_nacc; ++n) { - transition_acc ta(i, one, d.cand_acc[n], j); + transition_acc ta(i, one, d.cacc.mark(n), j); d.transaccid[ta] = ++d.nvars; d.revtransaccid.emplace(d.nvars, ta); } @@ -389,7 +393,7 @@ namespace spot for (unsigned n = 0; n < d.cand_nacc; ++n) { ++d.nvars; - for (unsigned j = 1; j < d.cand_size; ++j) + for (unsigned j = 0; j < d.cand_size; ++j) { bdd all = bddtrue; while (all != bddfalse) @@ -397,7 +401,7 @@ namespace spot bdd one = bdd_satoneset(all, ap, bddfalse); all -= one; - transition_acc ta(i, one, d.cand_acc[n], j); + transition_acc ta(i, one, d.cacc.mark(n), j); d.transaccid[ta] = d.nvars; d.revtransaccid.emplace(d.nvars, ta); } @@ -427,6 +431,9 @@ namespace spot sat_stats dtgba_to_sat(std::ostream& out, const_twa_graph_ptr ref, dict& d, bool state_based) { +#if DEBUG + debug_dict = ref->get_dict(); +#endif clause_counter nclauses; // Compute the AP used in the hard way. @@ -447,6 +454,7 @@ namespace spot } scc_info sm(ref); + sm.determine_unknown_acceptance(); d.is_weak_scc = sm.weak_sccs(); // Number all the SAT variables we may need. @@ -463,7 +471,6 @@ namespace spot out << " \n"; #if DEBUG - debug_dict = ref->get_dict(); debug_ref_acc = &ref->acc(); debug_cand_acc = &d.cacc; dout << "ref_size: " << ref_size << '\n'; @@ -586,7 +593,7 @@ namespace spot if (sm.scc_of(q2p) != q1p_scc) continue; bool is_weak = d.is_weak_scc[q1p_scc]; - bool is_acc = sm.is_accepting_scc(q1p_scc); + bool is_rej = sm.is_rejecting_scc(q1p_scc); for (unsigned q1 = 0; q1 < d.cand_size; ++q1) for (unsigned q2 = 0; q2 < d.cand_size; ++q2) @@ -624,88 +631,69 @@ namespace spot if (dp == q1p && q3 == q1) // (11,12) loop { - if ((!is_acc) || - (!is_weak && - !racc.accepting - (curacc | d.all_ref_acc[fp]))) + bool rejloop = + (is_rej || + !racc.accepting + (curacc | d.all_ref_acc[fp])); + + auto missing = + d.cand_acc. + missing(d.all_cand_acc[f], + !rejloop); + + for (auto& v: missing) { #if DEBUG - dout << "(11) " << p << " ∧ " - << t << "δ → ¬("; - - bool notfirst = false; - acc_cond::mark_t all_ = - d.all_cand_acc.back() - - d.all_cand_acc[f]; - for (auto m: d.cacc.sets(all_)) + dout << (rejloop ? + "(11) " : "(12) ") + << p << " ∧ " + << t << "δ → ("; + const char* orsep = ""; + for (int s: v) { - transition_acc - ta(q2, l, - d.cacc.mark(m), q1); - if (notfirst) - out << " ∧ "; + if (s < 0) + { + transition_acc + ta(q2, l, + d.cacc.mark(-s - 1), + q1); + out << orsep << "¬" << ta; + } else - notfirst = true; - out << ta << "FC"; + { + transition_acc + ta(q2, l, + d.cacc.mark(s), q1); + out << orsep << ta; + } + orsep = " ∨ "; } out << ")\n"; #endif // DEBUG out << -pid << ' ' << -ti; - - // 11 - acc_cond::mark_t all_f = - d.all_cand_acc.back() - - d.all_cand_acc[f]; - for (auto m: d.cacc.sets(all_f)) - { - transition_acc - ta(q2, l, - d.cacc.mark(m), q1); - int tai = d.transaccid[ta]; - assert(tai != 0); - out << ' ' << -tai; - } + for (int s: v) + if (s < 0) + { + transition_acc + ta(q2, l, + d.cacc.mark(-s - 1), + q1); + int tai = d.transaccid[ta]; + assert(tai != 0); + out << ' ' << -tai; + } + else + { + transition_acc + ta(q2, l, + d.cacc.mark(s), q1); + int tai = d.transaccid[ta]; + assert(tai != 0); + out << ' ' << tai; + } out << " 0\n"; ++nclauses; } - else - { -#if DEBUG - dout << "(12) " << p << " ∧ " - << t << "δ → ("; - bool notfirst = false; - // 11 - acc_cond::mark_t all_ = - d.cacc.comp(d.all_cand_acc[f]); - for (auto m: d.cacc.sets(all_)) - { - transition_acc - ta(q2, l, - d.cacc.mark(m), q1); - if (notfirst) - out << " ∧ "; - else - notfirst = true; - out << ta << "FC"; - } - out << ")\n"; -#endif // DEBUG - // 12 - acc_cond::mark_t all_f = - d.cacc.comp(d.all_cand_acc[f]); - for (auto m: d.cacc.sets(all_f)) - { - transition_acc - ta(q2, l, - d.cacc.mark(m), q1); - int tai = d.transaccid[ta]; - assert(tai != 0); - - out << -pid << ' ' << -ti - << ' ' << tai << " 0\n"; - ++nclauses; - } - } } // (13) augmenting paths (always). { @@ -779,9 +767,9 @@ namespace spot auto autdict = aut->get_dict(); auto a = make_twa_graph(autdict); a->copy_ap_of(aut); - a->set_generalized_buchi(satdict.cand_nacc); if (state_based) a->prop_state_based_acc(); + a->set_acceptance(satdict.cand_nacc, satdict.cand_acc); a->new_states(satdict.cand_size); // Last transition set in the automaton. @@ -876,20 +864,20 @@ namespace spot twa_graph_ptr dtgba_sat_synthetize(const const_twa_graph_ptr& a, unsigned target_acc_number, + const acc_cond::acc_code& target_acc, int target_state_number, bool state_based) { - if (!a->acc().is_generalized_buchi()) - throw std::runtime_error - ("dtgba_sat() can only work with generalized Büchi acceptance"); if (target_state_number == 0) return nullptr; - trace << "dtgba_sat_synthetize(..., acc = " << target_acc_number - << ", states = " << target_state_number + trace << "dtgba_sat_synthetize(..., nacc = " << target_acc_number + << ", acc = \"" << target_acc + << "\", states = " << target_state_number << ", state_based = " << state_based << ")\n"; dict d(a); d.cand_size = target_state_number; d.cand_nacc = target_acc_number; + d.cand_acc = target_acc; satsolver solver; satsolver::solution_pair solution; @@ -948,6 +936,7 @@ namespace spot twa_graph_ptr dtgba_sat_minimize(const const_twa_graph_ptr& a, unsigned target_acc_number, + const acc_cond::acc_code& target_acc, bool state_based) { int n_states = stats_reachable(a).states; @@ -957,7 +946,7 @@ namespace spot { auto next = dtgba_sat_synthetize(prev ? prev : a, target_acc_number, - --n_states, state_based); + target_acc, --n_states, state_based); if (!next) return prev; else @@ -970,6 +959,7 @@ namespace spot twa_graph_ptr dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, unsigned target_acc_number, + const acc_cond::acc_code& target_acc, bool state_based) { int max_states = stats_reachable(a).states - 1; @@ -980,8 +970,8 @@ namespace spot { int target = (max_states + min_states) / 2; auto next = - dtgba_sat_synthetize(prev ? prev : a, target_acc_number, target, - state_based); + dtgba_sat_synthetize(prev ? prev : a, target_acc_number, + target_acc, target, state_based); if (!next) { min_states = target + 1; @@ -995,4 +985,69 @@ namespace spot return prev; } + twa_graph_ptr + sat_minimize(twa_graph_ptr a, const char* opt) + { + option_map om; + auto err = om.parse_options(opt); + if (err) + { + std::string e = "failed to parse option near "; + e += err; + throw std::runtime_error(e); + } + + if (!is_deterministic(a)) + throw std::runtime_error + ("SAT-based minimization only work with deterministic automata"); + + bool sb = om.get("state-based", 0); + bool dicho = om.get("dichotomy", 0); + int states = om.get("states", -1); + int nacc = om.get("gba", -1); + + acc_cond::acc_code target_acc = a->get_acceptance(); + if (nacc != -1) + target_acc = acc_cond::generalized_buchi(nacc); + else + nacc = a->acc().num_sets(); + + bool target_is_buchi = + (nacc == 1 && target_acc.size() == 2 && + target_acc[1].op == acc_cond::acc_op::Inf + && target_acc[0].mark.has(0)); + + tgba_complete_here(a); + + if (sb) + a = sbacc(a); + + if (states == -1) + { + if (!target_is_buchi || !a->acc().is_buchi()) + a = (dicho ? dtgba_sat_minimize_dichotomy : dtgba_sat_minimize) + (a, nacc, target_acc, sb); + else + a = (dicho ? dtba_sat_minimize_dichotomy : dtba_sat_minimize) + (a, sb); + } + else + { + if (!target_is_buchi || !a->acc().is_buchi()) + a = dtgba_sat_synthetize(a, nacc, target_acc, states, sb); + else + a = dtba_sat_synthetize(a, states, sb); + } + + if (a) + { + if (a->acc().is_generalized_buchi()) + a = scc_filter(a); + else + a->purge_dead_states(); + } + + return a; + } + } diff --git a/src/twaalgos/dtgbasat.hh b/src/twaalgos/dtgbasat.hh index b0ce7a2d5..35a4ad68f 100644 --- a/src/twaalgos/dtgbasat.hh +++ b/src/twaalgos/dtgbasat.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -31,6 +31,8 @@ namespace spot /// \param target_acc_number is the number of acceptance sets wanted /// in the result. /// + /// \param target_acc the target acceptance condition + /// /// \param target_state_number is the desired number of states in /// the result. The output may have less than \a /// target_state_number reachable states. @@ -46,6 +48,7 @@ namespace spot SPOT_API twa_graph_ptr dtgba_sat_synthetize(const const_twa_graph_ptr& a, unsigned target_acc_number, + const acc_cond::acc_code& target_acc, int target_state_number, bool state_based = false); @@ -58,6 +61,7 @@ namespace spot SPOT_API twa_graph_ptr dtgba_sat_minimize(const const_twa_graph_ptr& a, unsigned target_acc_number, + const acc_cond::acc_code& target_acc, bool state_based = false); /// \brief Attempt to minimize a deterministic TGBA with a SAT solver. @@ -69,5 +73,21 @@ namespace spot SPOT_API twa_graph_ptr dtgba_sat_minimize_dichotomy(const const_twa_graph_ptr& a, unsigned target_acc_number, + const acc_cond::acc_code& target_acc, bool state_based = false); + + /// \brief High-level interface to SAT-based minimization + /// + /// Minimize the automaton \a aut, using options \a opt. + /// These options are given a comma-separated list of + /// assignments of the form: + /// + /// state-based = 1 + /// states = 10 + /// acc = generalized-Buchi 2 + /// acc = Rabin 3 + /// acc = same /* default */ + /// + SPOT_API twa_graph_ptr + sat_minimize(twa_graph_ptr aut, const char* opt); } diff --git a/src/twaalgos/postproc.cc b/src/twaalgos/postproc.cc index bd445ce62..fd762adbe 100644 --- a/src/twaalgos/postproc.cc +++ b/src/twaalgos/postproc.cc @@ -355,8 +355,8 @@ namespace spot else // Take the number of acceptance conditions from the input // automaton, not from dba, because dba often has been - // degeneralized to beform tba_determinize_check(). MAke - // sure it is at least 1. + // degeneralized by tba_determinize_check(). Make sure it + // is at least 1. target_acc = original_acc > 0 ? original_acc : 1; const_twa_graph_ptr in = 0; @@ -390,12 +390,17 @@ namespace spot else { if (sat_states_ != -1) - res = dtgba_sat_synthetize(res, target_acc, sat_states_, - state_based_); + res = dtgba_sat_synthetize + (res, target_acc, acc_cond::generalized_buchi(target_acc), + sat_states_, state_based_); else if (sat_minimize_ == 1 || sat_minimize_ == -1) - res = dtgba_sat_minimize(res, target_acc, state_based_); + res = dtgba_sat_minimize + (res, target_acc, acc_cond::generalized_buchi(target_acc), + state_based_); else // sat_minimize_ == 2 - res = dtgba_sat_minimize_dichotomy(res, target_acc, state_based_); + res = dtgba_sat_minimize_dichotomy + (res, target_acc, acc_cond::generalized_buchi(target_acc), + state_based_); } if (res) diff --git a/src/twaalgos/sbacc.cc b/src/twaalgos/sbacc.cc index e3eb05165..158a6b1a3 100644 --- a/src/twaalgos/sbacc.cc +++ b/src/twaalgos/sbacc.cc @@ -24,7 +24,7 @@ namespace spot { - twa_graph_ptr sbacc(twa_graph_ptr& old) + twa_graph_ptr sbacc(twa_graph_ptr old) { if (old->has_state_based_acc()) return old; diff --git a/src/twaalgos/sbacc.hh b/src/twaalgos/sbacc.hh index bb9a0d112..65a2aade5 100644 --- a/src/twaalgos/sbacc.hh +++ b/src/twaalgos/sbacc.hh @@ -26,5 +26,5 @@ namespace spot /// \brief Transform an automaton to use state-based acceptance /// /// This is independent on the acceptance condition used. - SPOT_API twa_graph_ptr sbacc(twa_graph_ptr& aut); + SPOT_API twa_graph_ptr sbacc(twa_graph_ptr aut); }