diff --git a/NEWS b/NEWS index 391522b0c..c3e32a2e8 100644 --- a/NEWS +++ b/NEWS @@ -2,7 +2,10 @@ New in spot 1.99.5a (not yet released) Command-line tools: - * autfilt has two now filters: --is-weak and --is-terminal. + * autfilt has two new filters: --is-weak and --is-terminal. + + * autfilt has a new transformation: --decompose-strength, + implementing the decomposition of our TACAS'13 paper. * All tools that output HOA files accept a --check=strength option to request automata to be marked as "weak" or "terminal" as diff --git a/src/bin/autfilt.cc b/src/bin/autfilt.cc index a37009377..83ec4ad73 100644 --- a/src/bin/autfilt.cc +++ b/src/bin/autfilt.cc @@ -75,6 +75,7 @@ enum { OPT_COMPLEMENT, OPT_COMPLEMENT_ACC, OPT_COUNT, + OPT_DECOMPOSE_STRENGTH, OPT_DESTUT, OPT_DNF_ACC, OPT_EDGES, @@ -153,6 +154,9 @@ static const argp_option options[] = { "complement-acceptance", OPT_COMPLEMENT_ACC, nullptr, 0, "complement the acceptance condition (without touching the automaton)", 0 }, + { "decompose-strength", OPT_DECOMPOSE_STRENGTH, "t|w|s", 0, + "extract the (t) terminal, (w) weak, or (s) strong part of an automaton" + " (letters may be combined to combine more strengths in the output)", 0 }, { "exclusive-ap", OPT_EXCLUSIVE_AP, "AP,AP,...", 0, "if any of those APs occur in the automaton, restrict all edges to " "ensure two of them may not be true at the same time. Use this option " @@ -279,6 +283,7 @@ static bool opt_rem_fin = false; static bool opt_clean_acc = false; static bool opt_complement = false; static bool opt_complement_acc = false; +static char* opt_decompose_strength = nullptr; static spot::acc_cond::mark_t opt_mask_acc = 0U; static std::vector opt_keep_states = {}; static unsigned int opt_keep_states_initial = 0; @@ -338,6 +343,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_COMPLEMENT_ACC: opt_complement_acc = true; break; + case OPT_DECOMPOSE_STRENGTH: + opt_decompose_strength = arg; + break; case OPT_DESTUT: opt_destut = true; break; @@ -627,6 +635,13 @@ namespace if (opt->product_or) aut = spot::product_or(std::move(aut), opt->product_or); + if (opt_decompose_strength) + { + aut = decompose_strength(aut, opt_decompose_strength); + if (!aut) + return 0; + } + if (opt_sat_minimize) { aut = spot::sat_minimize(aut, opt_sat_minimize, sbacc); diff --git a/src/bin/man/autfilt.x b/src/bin/man/autfilt.x index 593dd3878..d47b89c93 100644 --- a/src/bin/man/autfilt.x +++ b/src/bin/man/autfilt.x @@ -1,7 +1,29 @@ +.\" -*- coding: utf-8 -*- [NAME] autfilt \- filter, convert, and transform Büchi automata [DESCRIPTION] .\" Add any additional description here +[BIBLIOGRAPHY] +The following papers are related to some of the transformations implemented +in autfilt. + +.TP +\(bu +Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, and Denis Poitrenaud: +Strength-based decomposition of the property Büchi automaton for faster +model checking. Proceedings of TACAS'13. LNCS 7795. + +The \fB\-\-strength\-decompose\fR option implements the definitions +given in the above paper. +.TP +\(bu +František Blahoudek, Alexandre Duret-Lutz, Vojtčech Rujbr, and Jan Strejček: +On refinement of Büchi automata for explicit model checking. +Proceedings of SPIN'15. LNCS 9232. + +That paper gives the motivation for options \fB\-\-exclusive\-ap\fR +and \fB\-\-simplify\-exclusive\-ap\fR. + [SEE ALSO] .BR spot-x (7) .BR dstar2tgba (1) diff --git a/src/tests/strength.test b/src/tests/strength.test index 4d422a417..5417f3932 100755 --- a/src/tests/strength.test +++ b/src/tests/strength.test @@ -83,6 +83,34 @@ State: 0 {0} State: 1 [!0] 1 {0} --END-- +/* The example from the TACAS'13 paper. */ +HOA: v1 +name: "(Gb | F!a) W c" +States: 5 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[0] 0 {0} +State: 1 +[0&1&!2] 0 +[!1&!2] 1 {0} +[1&!2] 2 +[2] 3 +State: 2 +[!1&!2] 1 {0} +[1&!2] 2 +[!1&2] 3 +[1&2] 4 +State: 3 +[t] 3 {0} +State: 4 +[!1] 3 +[1] 4 +--END-- EOF run 0 $autfilt -H --check=strength in | tee out @@ -161,6 +189,400 @@ State: 0 {0} State: 1 {0} [!0] 1 --END-- +HOA: v1 +name: "(Gb | F!a) W c" +States: 5 +Start: 1 +AP: 3 "b" "a" "c" +acc-name: Buchi +Acceptance: 1 Inf(0) +properties: trans-labels explicit-labels trans-acc stutter-invariant +--BODY-- +State: 0 +[0] 0 {0} +State: 1 +[0&1&!2] 0 +[!1&!2] 1 {0} +[1&!2] 2 +[2] 3 +State: 2 +[!1&!2] 1 {0} +[1&!2] 2 +[!1&2] 3 +[1&2] 4 +State: 3 +[t] 3 {0} +State: 4 +[!1] 3 +[1] 4 +--END-- +EOF + +diff out expected + + +run 0 $autfilt -H --decompose=t in | tee out.t +run 0 $autfilt -H --decompose=w in | tee out.w +run 0 $autfilt -H --decompose=s in | tee out.s +run 0 $autfilt -H --decompose=tw in | tee out.tw +run 0 $autfilt -H --decompose=ws in | tee out.ws +run 0 $autfilt -H --decompose=tws in | tee out.tws +echo '/******************************/' > sep +cat out.t sep out.w sep out.s sep out.tw sep out.ws sep out.tws > out + +cat >expected < namespace spot @@ -113,5 +114,137 @@ namespace spot } + twa_graph_ptr + decompose_strength(const const_twa_graph_ptr& aut, const char* keep_opt) + { + if (keep_opt == nullptr || *keep_opt == 0) + throw std::runtime_error + (std::string("option for decompose_strength() should not be empty")); + enum strength { + Ignore = 0, + Terminal = 1, + WeakStrict = 2, + Weak = Terminal | WeakStrict, + Strong = 4, + Needed = 8, // Needed SCCs are those that lead to + // the SCCs we want to keep. + }; + unsigned char keep = Ignore; + while (auto c = *keep_opt++) + switch (c) + { + case 's': + keep |= Strong; + break; + case 't': + keep |= Terminal; + break; + case 'w': + keep |= WeakStrict; + break; + default: + throw std::runtime_error + (std::string("unknown option for decompose_strength(): ") + c); + } + + scc_info si(aut); + si.determine_unknown_acceptance(); + + unsigned n = si.scc_count(); + std::vector want(n, Ignore); + bool nonempty = false; + bool strong_seen = false; + + for (unsigned i = 0; i < n; ++i) // SCC are topologically ordered + { + if (si.is_accepting_scc(i)) + { + if (is_weak_scc(si, i)) + { + if (keep & Weak) + { + if ((keep & Weak) == Weak) + want[i] = Weak; + else + want[i] = keep & + (is_complete_scc(si, i) ? Terminal : WeakStrict); + } + } + else + { + want[i] = keep & Strong; + strong_seen = true; + } + nonempty |= want[i]; + } + // An SCC is needed if one of its successor is. + for (unsigned j: si.succ(i)) + if (want[j]) + { + want[i] |= Needed; + break; + } + } + + if (!nonempty) + return nullptr; + + twa_graph_ptr res = make_twa_graph(aut->get_dict()); + res->copy_ap_of(aut); + res->prop_copy(aut, { true, false, true, false }); + + acc_cond::mark_t wacc = 0U; // Acceptance for weak SCCs + acc_cond::mark_t uacc = 0U; // Acceptance for "needed" SCCs, that + // we only want to traverse. + if (keep & Strong) + { + res->copy_acceptance_of(aut); + auto& ac = res->acc(); + if (ac.uses_fin_acceptance()) + // Note that we ignore the cases where the acceptance + // condition is always satisfiable. In that case + // uacc will be set to 0U, which will be satisfiable + uacc = ac.get_acceptance().unsat_mark().second; + } + else + { + wacc = res->set_buchi(); + } + + auto fun = [&si, &want, uacc, wacc, keep] + (unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst) + { + if (want[si.scc_of(dst)] == Ignore) + { + cond = bddfalse; + return; + } + if (want[si.scc_of(src)] == Needed) + { + acc = uacc; + return; + } + if (keep & Strong) + return; + acc = wacc; + }; + + transform_accessible(aut, res, fun); + + if (!(keep & Strong)) + { + res->prop_weak(true); + if (!(keep & WeakStrict)) + { + assert(keep & Terminal); + res->prop_terminal(true); + } + } + else + { + res->prop_weak(!strong_seen); + } + return res; + } } diff --git a/src/twaalgos/strength.hh b/src/twaalgos/strength.hh index 137129f1a..657cd7f6e 100644 --- a/src/twaalgos/strength.hh +++ b/src/twaalgos/strength.hh @@ -68,4 +68,43 @@ namespace spot /// will be built otherwise). SPOT_API void check_strength(const twa_graph_ptr& aut, scc_info* sm = nullptr); + + + /// \brief Extract a sub-automaton of a given strength + /// + /// The string \a keep should be a non-empty combination of + /// the following letters: + /// - 'w': keep only weak SCCs (i.e., SCCs in which all transitions belong + /// to the same acceptance sets) that are not terminal. + /// - 't': keep terminal SCCs (i.e., weak SCCs that are complete) + /// - 's': keep strong SCCs (i.e., SCCs that are not weak). + /// + /// This algorithm returns a subautomaton that contains all SCCs of the + /// requested strength, plus any upstream SCC (but adjusted not to be + /// accepting). + /// + /** \verbatim + @inproceedings{renault.13.tacas, + author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice + Kordon and Denis Poitrenaud}, + title = {Strength-Based Decomposition of the Property {B\"u}chi + Automaton for Faster Model Checking}, + booktitle = {Proceedings of the 19th International Conference on Tools + and Algorithms for the Construction and Analysis of Systems + (TACAS'13)}, + editor = {Nir Piterman and Scott A. Smolka}, + year = {2013}, + month = mar, + pages = {580--593}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {7795}, + doi = {10.1007/978-3-642-36742-7_42} + } + \endverbatim */ + /// + /// \param aut the automaton to decompose + /// \param keep a string specifying the strengths to keep: it should + SPOT_API twa_graph_ptr + decompose_strength(const const_twa_graph_ptr& aut, const char* keep); }