diff --git a/NEWS b/NEWS index 39d078500..8554b7225 100644 --- a/NEWS +++ b/NEWS @@ -20,9 +20,9 @@ New in spot 2.7.2.dev (not yet released) 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 state instead of 4.) - - acc_cond::acc_code::top_disjuncts() and - acc_cond::acc_code::top_conjuncts() can be used to split an - acceptance condition on the top-level & or |. + - acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be + used to split an acceptance condition on the top-level & or |. + These methods also exist in acc_cond::acc_code. - minimize_obligation() learned to work on very weak automata even if the formula or negated automaton are not supplied. (This diff --git a/python/spot/impl.i b/python/spot/impl.i index 8cad8aaf9..f8597d528 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -473,6 +473,7 @@ namespace std { %template(vectorformula) vector; %template(vectorunsigned) vector; %template(vectorpairunsigned) vector>; + %template(vectoracccond) vector; %template(vectoracccode) vector; %template(vectorbool) vector; %template(vectorbdd) vector; diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index 2d9f71309..177b6bda9 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1234,12 +1234,12 @@ namespace spot namespace { - static std::vector + template + static void top_clauses(const acc_cond::acc_code& code, - acc_cond::acc_op connect, acc_cond::acc_op inf_fin) + acc_cond::acc_op connect, acc_cond::acc_op inf_fin, + Fun store) { - std::vector res; - if (!code.empty()) { auto pos = &code.back(); @@ -1259,17 +1259,17 @@ namespace spot tmp[0].mark = {d}; tmp[1].sub.op = inf_fin; tmp[1].sub.size = 1; - res.emplace_back(tmp); + store(tmp); } } else { - res.emplace_back(pos); + store(pos); } pos -= pos->sub.size; } while (pos > start); - return res; + return; } if (pos->sub.op == inf_fin) { @@ -1280,24 +1280,48 @@ namespace spot tmp[0].mark = {d}; tmp[1].sub.op = inf_fin; tmp[1].sub.size = 1; - res.emplace_back(tmp); + store(tmp); } - return res; + return; } } - res.emplace_back(code); - return res; + store(code); + return; } } std::vector acc_cond::acc_code::top_disjuncts() const { - return top_clauses(*this, acc_cond::acc_op::Or, acc_cond::acc_op::Fin); + std::vector res; + top_clauses(*this, acc_cond::acc_op::Or, acc_cond::acc_op::Fin, + [&](const acc_cond::acc_code& c) { res.emplace_back(c); }); + return res; } std::vector acc_cond::acc_code::top_conjuncts() const { - return top_clauses(*this, acc_cond::acc_op::And, acc_cond::acc_op::Inf); + std::vector res; + top_clauses(*this, acc_cond::acc_op::And, acc_cond::acc_op::Inf, + [&](const acc_cond::acc_code& c) { res.emplace_back(c); }); + return res; + } + + std::vector acc_cond::top_disjuncts() const + { + std::vector res; + top_clauses(code_, acc_cond::acc_op::Or, acc_cond::acc_op::Fin, + [&](const acc_cond::acc_code& c) + { res.emplace_back(num_, c); }); + return res; + } + + std::vector acc_cond::top_conjuncts() const + { + std::vector res; + top_clauses(code_, acc_cond::acc_op::And, acc_cond::acc_op::Inf, + [&](const acc_cond::acc_code& c) + { res.emplace_back(num_, c); }); + return res; } std::pair diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 3a7f2db6f..05747a29e 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1978,6 +1978,26 @@ namespace spot return code_.fin_one(); } + /// \brief Return the top-level disjuncts. + /// + /// For instance, if the formula is + /// (5, Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4)))), this returns + /// [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)|Fin(4)))]. + /// + /// If the formula is not a disjunction, this returns + /// a vector with the formula as only element. + std::vector top_disjuncts() const; + + /// \brief Return the top-level conjuncts. + /// + /// For instance, if the formula is + /// (5, Fin(0)|Fin(1)|(Fin(2)&(Inf(3)|Fin(4)))), this returns + /// [(5, Fin(0)), (5, Fin(1)), (5, Fin(2)&(Inf(3)|Fin(4)))]. + /// + /// If the formula is not a conjunction, this returns + /// a vector with the formula as only element. + std::vector top_conjuncts() const; + protected: mark_t all_sets_() const { diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index c406ebdc3..245ab3e07 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -1383,6 +1383,32 @@ "print(acc)\n", "print(acc.unsat_mark())" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "`top_conjuncts` and `top_disjuncts` also work on `acc_cond`. In this case they return tuple of `acc_cond` with the same number of sets." + ] + }, + { + "cell_type": "code", + "execution_count": 54, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\"),)\n", + "(spot.acc_cond(4, \"Fin(0) | Inf(1)\"), spot.acc_cond(4, \"Fin(2) | Inf(3)\"))\n" + ] + } + ], + "source": [ + "print(acc.top_disjuncts())\n", + "print(acc.top_conjuncts())" + ] } ], "metadata": {