From 7fedb3dc61327a87a965924c78fd7f7dc7d5019f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 10 Sep 2021 18:17:17 +0200 Subject: [PATCH] acc: introduce fin_one_extract() * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::fin_one_extract, acc_code::acc_cond::fin_one_extract): New methods. * python/spot/impl.i: Add support for the return type. * tests/python/acc_cond.ipynb: Test them. --- python/spot/impl.i | 2 + spot/twa/acc.cc | 112 ++++++++++++++++++++++++++++++++++++ spot/twa/acc.hh | 72 ++++++++++++++++++----- tests/python/acc_cond.ipynb | 76 +++++++++++++++++++++++- 4 files changed, 246 insertions(+), 16 deletions(-) diff --git a/python/spot/impl.i b/python/spot/impl.i index d20722fc2..dbe2ccf48 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -468,6 +468,8 @@ namespace std { %template(liststr) list; %template(pairunsigned) pair; %template(pairmark_t) pair; + %template(pairintacccode) pair; + %template(pairintacccond) pair; %template(vectorformula) vector; %template(vectorunsigned) vector; %template(vectorpairunsigned) vector>; diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index b1ec3335c..5b7985d70 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -2644,6 +2644,118 @@ namespace spot return -1; } + namespace + { + int has_top_fin(const acc_cond::acc_word* pos, bool top = true) + { + if (pos->sub.op == acc_cond::acc_op::Fin) + { + acc_cond::mark_t m = pos[-1].mark; + if (top || m.is_singleton()) + return m.min_set() - 1; + } + else if (pos->sub.op == acc_cond::acc_op::And) + { + auto sub = pos - pos->sub.size; + do + { + --pos; + if (int f = has_top_fin(pos, false); f >= 0) + return f; + pos -= pos->sub.size; + } + while (sub < pos); + } + else if (top && pos->sub.op == acc_cond::acc_op::Or) + { + auto sub = pos - pos->sub.size; + do + { + --pos; + if (int f = has_top_fin(pos); f >= 0) + return f; + pos -= pos->sub.size; + } + while (sub < pos); + } + return -1; + } + + bool uses_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f) + { + auto sub = pos - pos->sub.size; + do + { + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Or: + --pos; + break; + case acc_cond::acc_op::Fin: + if (pos[-1].mark & f) + return true; + SPOT_FALLTHROUGH; + case acc_cond::acc_op::Inf: + case acc_cond::acc_op::InfNeg: + case acc_cond::acc_op::FinNeg: + pos -= 2; + break; + } + } + while (sub < pos); + return false; + } + + acc_cond::acc_code extract_fin(const acc_cond::acc_word* pos, + acc_cond::mark_t f) + { + auto start = pos - pos->sub.size; + switch (pos->sub.op) + { + case acc_cond::acc_op::And: + case acc_cond::acc_op::Fin: + case acc_cond::acc_op::Inf: + return pos; + case acc_cond::acc_op::Or: + { + --pos; + auto res = acc_cond::acc_code::f(); + do + { + if (uses_fin(pos, f)) + { + acc_cond::acc_code tmp(pos); + tmp |= std::move(res); + std::swap(tmp, res); + } + pos -= pos->sub.size + 1; + } + while (pos > start); + return res; + } + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + return {}; + } + SPOT_UNREACHABLE(); + return {}; + } + } + + std::pair + acc_cond::acc_code::fin_one_extract() const + { + if (is_t() || is_f()) + return {-1, *this}; + const acc_cond::acc_word* pos = &back(); + int selected_fin = has_top_fin(pos); + if (selected_fin < 0) + selected_fin = fin_one(); + return {selected_fin, extract_fin(pos, {(unsigned) selected_fin})}; + } + namespace { bool diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 684b4b576..761433f54 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1251,12 +1251,6 @@ namespace spot /// `Fin(0)&Fin(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. mark_t fin_unit() const; - /// \brief Return one acceptance set i that appear as `Fin(i)` - /// in the condition. - /// - /// Return -1 if no such set exist. - int fin_one() const; - /// \brief Find a `Inf(i)` that is a unit clause. /// /// This return a mark_t `{i}` such that `Inf(i)` appears as a @@ -1270,6 +1264,31 @@ namespace spot /// `Inf(0)&Inf(1)&(Inf(2)|Fin(3))`, this will return `{0,1}`. mark_t inf_unit() const; + /// \brief Return one acceptance set i that appears as `Fin(i)` + /// in the condition. + /// + /// Return -1 if no such set exist. + int fin_one() const; + + /// \brief Return one acceptance set i that appears as `Fin(i)` + /// in the condition, and all disjuncts containing it. + /// + /// If the condition is a disjunction and one of the disjunct + /// has the shape `...&Fin(i)&...`, then `i` will be prefered + /// over any arbitrary Fin. + /// + /// The second element of the pair, is the same acceptance + /// condition in which all top-level disjunct not featuring + /// `Fin(i)` have been removed. + /// + /// For example on + /// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` + /// the output would be the pair + /// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. + /// On that example `Fin(1)` is prefered to `Fin(7)` because + /// it appears at the top-level. + std::pair fin_one_extract() const; + /// \brief Help closing accepting or rejecting cycle. /// /// Assuming you have a partial cycle visiting all acceptance @@ -2157,15 +2176,6 @@ namespace spot return code_.fin_unit(); } - /// \brief Return one acceptance set i that appear as `Fin(i)` - /// in the condition. - /// - /// Return -1 if no such set exist. - int fin_one() const - { - return code_.fin_one(); - } - /// \brief Find a `Inf(i)` that is a unit clause. /// /// This return a mark_t `{i}` such that `Inf(i)` appears as a @@ -2182,6 +2192,38 @@ namespace spot return code_.inf_unit(); } + /// \brief Return one acceptance set i that appear as `Fin(i)` + /// in the condition. + /// + /// Return -1 if no such set exist. + int fin_one() const + { + return code_.fin_one(); + } + + /// \brief Return one acceptance set i that appears as `Fin(i)` + /// in the condition, and all disjuncts containing it. + /// + /// If the condition is a disjunction and one of the disjunct + /// has the shape `...&Fin(i)&...`, then `i` will be prefered + /// over any arbitrary Fin. + /// + /// The second element of the pair, is the same acceptance + /// condition in which all top-level disjunct not featuring + /// `Fin(i)` have been removed. + /// + /// For example on + /// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` + /// the output would be the pair + /// `(1, Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. + /// On that example `Fin(1)` is prefered to `Fin(7)` because + /// it appears at the top-level. + std::pair fin_one_extract() const + { + auto [f, c] = code_.fin_one_extract(); + return {f, {num_sets(), std::move(c)}}; + } + /// \brief Return the top-level disjuncts. /// /// For instance, if the formula is diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index 245ab3e07..e14b85fda 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -1409,6 +1409,80 @@ "print(acc.top_disjuncts())\n", "print(acc.top_conjuncts())" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "`fin_one()` return the number of one color `x` that appears as `Fin(x)` in the formula, or `-1` if the formula is Fin-less.\n", + "\n", + "The variant `fin_one_extract()` consider the acceptance condition as a disjunction (if the top-level operator is not a disjunction, we just assume the formula is a disjunction with only one disjunct), and return a pair `(x,c)` where `c` is the disjunction of all disjuncts of the original formula where `Fin(x)` appear. Also this function tries to choose an `x` such that one of the disjunct has the form `...&Fin(x)&...` if possible: this is visible in the third example, where 5 is prefered to 2." + ] + }, + { + "cell_type": "code", + "execution_count": 55, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(4, (Fin(0) | Inf(1)) & (Fin(2) | Inf(3)))\n", + "0\n", + "(0, spot.acc_cond(4, \"(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))\"))\n" + ] + } + ], + "source": [ + "print(acc)\n", + "print(acc.fin_one())\n", + "print(acc.fin_one_extract())" + ] + }, + { + "cell_type": "code", + "execution_count": 56, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(6, (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5)))\n", + "0\n", + "(0, spot.acc_cond(6, \"Fin(0) & Inf(1)\"))\n" + ] + } + ], + "source": [ + "acc2 = spot.acc_cond('Rabin 3')\n", + "print(acc2)\n", + "print(acc2.fin_one())\n", + "print(acc2.fin_one_extract())" + ] + }, + { + "cell_type": "code", + "execution_count": 57, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(6, (Inf(0) & (Fin(2) | Inf(3))) | (Inf(4) & Fin(5)) | ((Inf(0)&Inf(5)) & (Fin(0)|Fin(5))))\n", + "2\n", + "(5, spot.acc_cond(6, \"(Inf(4) & Fin(5)) | ((Inf(0)&Inf(5)) & (Fin(0)|Fin(5)))\"))\n" + ] + } + ], + "source": [ + "acc3 = spot.acc_cond('Inf(0)&(Fin(2)|Inf(3)) | Inf(4)&Fin(5) | Inf(0)&Inf(5)&(Fin(5)|Fin(0))')\n", + "print(acc3)\n", + "print(acc3.fin_one())\n", + "print(acc3.fin_one_extract())" + ] } ], "metadata": { @@ -1427,7 +1501,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.3rc1" + "version": "3.9.2" } }, "nbformat": 4,