From 721d5695ec73ca234dce7a45fa0fd76519cb2013 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 25 May 2022 17:02:38 +0200 Subject: [PATCH] add a newer version of the generic emptiness check MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit As discussed with Jan Strejček. * spot/twa/acc.cc, spot/twa/acc.hh (fin_unit_one_split): New function. (fin_one_extract): Return the simplified acceptance condition as an optimization. * python/spot/impl.i: Bind this new function. * tests/python/acc.py: New file, to test it. * tests/Makefile.am: Add acc.py. * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Implement the spot211 variant of the emptiness check. * tests/python/genem.py: Test it. * tests/python/acc_cond.ipynb: Adjust test for fin_one_extract. --- python/spot/impl.i | 11 +++++ spot/twa/acc.cc | 99 ++++++++++++++++++++++++++++++++++++- spot/twa/acc.hh | 75 +++++++++++++++++++++++----- spot/twaalgos/genem.cc | 27 ++++++++-- spot/twaalgos/genem.hh | 10 +++- tests/Makefile.am | 1 + tests/python/acc.py | 65 ++++++++++++++++++++++++ tests/python/acc_cond.ipynb | 41 ++++++++++++--- tests/python/genem.py | 9 ++-- 9 files changed, 308 insertions(+), 30 deletions(-) create mode 100644 tests/python/acc.py diff --git a/python/spot/impl.i b/python/spot/impl.i index b7f116201..a07709005 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -551,6 +551,17 @@ namespace std { } %apply std::vector &OUTPUT {std::vector& pairs} %apply std::vector &OUTPUT {std::vector& pairs} +// Must occur before the twa declaration +%typemap(out) SWIGTYPE spot::acc_cond::fin_unit_one_split %{ + { + auto& v = static_cast>($1); + $result = PyTuple_Pack(3, + swig::from(std::get<0>(v)), + swig::from(std::get<1>(v)), + swig::from(std::get<2>(v))); + } +%} + %include %template(pair_bool_mark) std::pair; diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index ce5d463aa..07aac36f9 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -2707,6 +2707,35 @@ namespace spot return false; } + // Check wheter pos looks like Fin(f) or Fin(f)&rest + bool is_conj_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: + --pos; + break; + case acc_cond::acc_op::Or: + pos -= pos->sub.size + 1; + 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) { @@ -2716,7 +2745,7 @@ namespace spot case acc_cond::acc_op::And: case acc_cond::acc_op::Fin: case acc_cond::acc_op::Inf: - return pos; + return strip_rec(pos, f, true, false); case acc_cond::acc_op::Or: { --pos; @@ -2725,7 +2754,7 @@ namespace spot { if (uses_fin(pos, f)) { - acc_cond::acc_code tmp(pos); + auto tmp = strip_rec(pos, f, true, false); tmp |= std::move(res); std::swap(tmp, res); } @@ -2742,6 +2771,52 @@ namespace spot SPOT_UNREACHABLE(); return {}; } + + std::pair + split_top_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: + if (is_conj_fin(pos, f)) + return {pos, acc_cond::acc_code::f()}; + SPOT_FALLTHROUGH; + case acc_cond::acc_op::Inf: + return {acc_cond::acc_code::f(), pos}; + case acc_cond::acc_op::Or: + { + --pos; + auto left = acc_cond::acc_code::f(); + auto right = acc_cond::acc_code::f(); + do + { + if (is_conj_fin(pos, f)) + { + auto tmp = strip_rec(pos, f, true, false); + tmp |= std::move(left); + std::swap(tmp, left); + } + else + { + acc_cond::acc_code tmp(pos); + tmp |= std::move(right); + std::swap(tmp, right); + } + pos -= pos->sub.size + 1; + } + while (pos > start); + return {std::move(left), std::move(right)}; + } + case acc_cond::acc_op::FinNeg: + case acc_cond::acc_op::InfNeg: + SPOT_UNREACHABLE(); + return {acc_cond::acc_code::f(), acc_cond::acc_code::f()}; + } + SPOT_UNREACHABLE(); + return {acc_cond::acc_code::f(), acc_cond::acc_code::f()}; + } } std::pair @@ -2756,6 +2831,26 @@ namespace spot return {selected_fin, extract_fin(pos, {(unsigned) selected_fin})}; } + std::tuple + acc_cond::acc_code::fin_unit_one_split() const + { + if (SPOT_UNLIKELY(is_t() || is_f())) + err: + throw std::runtime_error("fin_unit_one_split(): no Fin"); + const acc_cond::acc_word* pos = &back(); + int selected_fin = has_top_fin(pos); + if (selected_fin >= 0) + { + auto [left, right] = split_top_fin(pos, {(unsigned) selected_fin}); + return {selected_fin, std::move(left), std::move(right)}; + } + selected_fin = fin_one(); + if (selected_fin < 0) + goto err; + acc_cond::mark_t fo_m = {(unsigned) selected_fin}; + return {selected_fin, extract_fin(pos, fo_m), force_inf(fo_m)}; + } + namespace { bool diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index 455850f35..905f5c40a 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -26,6 +26,7 @@ #include #include #include +#include #include #include #include @@ -1271,7 +1272,8 @@ namespace spot int fin_one() const; /// \brief Return one acceptance set i that appears as `Fin(i)` - /// in the condition, and all disjuncts containing it. + /// in the condition, and all disjuncts containing it with + /// Fin(i) changed to true and Inf(i) to false. /// /// If the condition is a disjunction and one of the disjunct /// has the shape `...&Fin(i)&...`, then `i` will be prefered @@ -1282,13 +1284,34 @@ namespace spot /// `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. + /// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` the + /// output would be the pair, we would select `Fin(1)` over + /// `Fin(7)` because it appears at the top-level. Then we would + /// collect the disjuncts containing `Fin(1)`, that is, + /// `Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. Finally we would + /// replace `Fin(1)` by true and `Inf(1)` by false. The return + /// value would then be `(1, Inf(2)|Inf(5))`. std::pair fin_one_extract() const; + /// \brief Split an acceptance condition, trying to select one + /// unit-Fin. + /// + /// If the condition is a disjunction and one of the disjunct as + /// has the shape `...&Fin(i)&...`, then this will return + /// (i, left, right), where left is all disjunct of this form, and + /// right are all the others. + /// + /// If the input formula has the shape `...&Fin(i)&...` then left + /// is set to the entire formula, and right is empty. + /// + /// If no disjunct has the right shape, then a random Fin(i) is + /// searched in the formula, and the output (i, left, right). + /// is such that left contains all disjuncts containing Fin(i) + /// (at any depth), and right contains the original formlula + /// where Fin(i) has been replaced by false. + std::tuple + fin_unit_one_split() const; + /// \brief Help closing accepting or rejecting cycle. /// /// Assuming you have a partial cycle visiting all acceptance @@ -2203,7 +2226,8 @@ namespace spot } /// \brief Return one acceptance set i that appears as `Fin(i)` - /// in the condition, and all disjuncts containing it. + /// in the condition, and all disjuncts containing it with + /// Fin(i) changed to true and Inf(i) to false. /// /// If the condition is a disjunction and one of the disjunct /// has the shape `...&Fin(i)&...`, then `i` will be prefered @@ -2214,17 +2238,42 @@ namespace spot /// `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. + /// `Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))` the + /// output would be the pair, we would select `Fin(1)` over + /// `Fin(7)` because it appears at the top-level. Then we would + /// collect the disjuncts containing `Fin(1)`, that is, + /// `Fin(1)&Inf(2)|Inf(5)&(Fin(1)|Fin(7)))`. Finally we would + /// replace `Fin(1)` by true and `Inf(1)` by false. The return + /// value would then be `(1, Inf(2)|Inf(5))`. std::pair fin_one_extract() const { auto [f, c] = code_.fin_one_extract(); return {f, {num_sets(), std::move(c)}}; } + /// \brief Split an acceptance condition, trying to select one + /// unit-Fin. + /// + /// If the condition is a disjunction and one of the disjunct as + /// has the shape `...&Fin(i)&...`, then this will return + /// (i, left, right), where left is all disjunct of this form, and + /// right are all the others. + /// + /// If the input formula has the shape `...&Fin(i)&...` then left + /// is set to the entire formula, and right is empty. + /// + /// If no disjunct has the right shape, then a random Fin(i) is + /// searched in the formula, and the output (i, left, right). + /// is such that left contains all disjuncts containing Fin(i) + /// (at any depth), and right contains the original formlula + /// where Fin(i) has been replaced by false. + std::tuple + fin_unit_one_split() const + { + auto [f, l, r] = code_.fin_unit_one_split(); + return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}}; + } + /// \brief Return the top-level disjuncts. /// /// For instance, if the formula is diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index e49f5b07c..51b2ea903 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2021 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2022 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -25,7 +25,7 @@ namespace spot { namespace { - enum genem_version_t { spot28, atva19, spot29, spot210 }; + enum genem_version_t { spot28, atva19, spot29, spot210, spot211 }; static genem_version_t genem_version = spot29; } @@ -33,6 +33,8 @@ namespace spot { if (emversion == nullptr || !strcasecmp(emversion, "spot29")) genem_version = spot29; + else if (!strcasecmp(emversion, "spot211")) + genem_version = spot211; else if (!strcasecmp(emversion, "spot210")) genem_version = spot210; else if (!strcasecmp(emversion, "spot28")) @@ -41,7 +43,8 @@ namespace spot genem_version = atva19; else throw std::invalid_argument("generic_emptiness_check version should be " - "one of {spot28, atva19, spot29, spot210}"); + "one of {spot28, atva19, spot29, spot210, " + "spot211}"); } namespace @@ -84,6 +87,8 @@ namespace spot scc_split_check(const scc_info& si, unsigned scc, const acc_cond& acc, Extra extra, acc_cond::mark_t tocut) { + if (genem_version == spot211 || genem_version == spot210) + tocut |= acc.fin_unit(); scc_and_mark_filter filt(si, scc, tocut); filt.override_acceptance(acc); scc_info upper_si(filt, EarlyStop @@ -118,13 +123,27 @@ namespace spot // Try to accept when Fin(fo) == true acc_cond::mark_t fo_m = {(unsigned) fo}; if (!scc_split_check - (si, scc, fpart.remove(fo_m, true), extra, fo_m)) + (si, scc, fpart, extra, fo_m)) if constexpr (EarlyStop) return false; // Try to accept when Fin(fo) == false acc = acc.force_inf(fo_m); } while (!acc.is_f()); + else if (genem_version == spot211) + { + do + { + auto [fo, fpart, rest] = acc.fin_unit_one_split(); + acc_cond::mark_t fo_m = {(unsigned) fo}; + if (!scc_split_check + (si, scc, fpart, extra, fo_m)) + if constexpr (EarlyStop) + return false; + acc = rest; + } + while (!acc.is_f()); + } else if (genem_version == spot29) do { diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index 2d1ded4c7..3c3e5de51 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2021 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2022 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -100,7 +100,13 @@ namespace spot /// - "spot29" improves upon the worst case of atva19. This is /// the default. /// - "spot210" improves upon "spot29" in a few cases where a Fin - /// is shared by multiple disjuncts. + /// is shared by multiple disjuncts. This improve the worst + /// case complexity of EL-automata in the general case, but worsen + /// the complexity of Hyper-Rabin in particular. + /// - "spot211" is another attempt at fixing worst case complexities. + /// Compared to atva19, this improves the complexities for Rabin, + /// GeneralizedRabin, and EL without worsening the complexity of + /// Hyper-Rabin. SPOT_API void generic_emptiness_check_select_version(const char* emversion = nullptr); diff --git a/tests/Makefile.am b/tests/Makefile.am index 3582a8493..b4627f3e6 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -391,6 +391,7 @@ TESTS_python = \ python/_altscc.ipynb \ python/_autparserr.ipynb \ python/_aux.ipynb \ + python/acc.py \ python/accparse2.py \ python/alarm.py \ python/aliases.py \ diff --git a/tests/python/acc.py b/tests/python/acc.py new file mode 100644 index 000000000..8a23dcd46 --- /dev/null +++ b/tests/python/acc.py @@ -0,0 +1,65 @@ +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2022 Laboratoire de Recherche et Développement +# de l'Epita +# +# 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 . + +import spot +from unittest import TestCase +tc = TestCase() + +a = spot.acc_cond('parity min odd 5') +tc.assertEqual(str(a.fin_unit_one_split()), + '(0, {}, spot.acc_cond(5, "f"))'.format(repr(a))) + +a.set_acceptance('Rabin 3') +tc.assertEqual(str(a.fin_unit_one_split()), + '(0, spot.acc_cond(5, "Inf(1)"), ' + 'spot.acc_cond(5, "(Fin(2) & Inf(3)) | (Fin(4) & Inf(5))"))') + +a.set_acceptance('(Fin(0)|Inf(3))&(Fin(1)|Inf(4))&(Fin(2)|Inf(5)) |\ +(Fin(0)|Inf(4))&(Fin(1)|Inf(5))&(Fin(2)|Inf(3)) |\ +(Fin(0)|Inf(5))&(Fin(1)|Inf(3))&(Fin(2)|Inf(4))') + +tc.maxDiff = None +tc.assertEqual(str(a.fin_unit_one_split()), + '(0, spot.acc_cond(5, ' + '"((Fin(1) | Inf(4)) & (Fin(2) | Inf(5))) | ' + '((Fin(1) | Inf(5)) & (Fin(2) | Inf(3))) | ' + '((Fin(1) | Inf(3)) & (Fin(2) | Inf(4)))"), ' + 'spot.acc_cond(5, ' + '"(Inf(3) & (Fin(1) | Inf(4)) & (Fin(2) | Inf(5))) | ' + '(Inf(4) & (Fin(1) | Inf(5)) & (Fin(2) | Inf(3))) | ' + '(Inf(5) & (Fin(1) | Inf(3)) & (Fin(2) | Inf(4)))"))') + +a = a.remove([4], True) +tc.assertEqual(str(a.fin_unit_one_split()), + '(1, spot.acc_cond(5, ' + '"(Fin(0) | Inf(3)) & (Fin(2) | Inf(5))"), ' + 'spot.acc_cond(5, ' + '"(Fin(0) & (Fin(1) | Inf(5)) & (Fin(2) | Inf(3))) | ' + '((Fin(0) | Inf(5)) & (Fin(1) | Inf(3)) & Fin(2))"))') + +def report_missing_exception(): + raise RuntimeError("missing exception") + +a.set_acceptance("Inf(0)") +try: + a.fin_unit_one_split() +except RuntimeError as e: + tc.assertIn('no Fin', str(e)) +else: + report_missing_exception() diff --git a/tests/python/acc_cond.ipynb b/tests/python/acc_cond.ipynb index 76580fcdd..492c416ca 100644 --- a/tests/python/acc_cond.ipynb +++ b/tests/python/acc_cond.ipynb @@ -1416,7 +1416,7 @@ "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." + "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)` used to appear but where `Fin(x)` have been replaced by `true`, and `Inf(x)` by `false`. 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." ] }, { @@ -1430,7 +1430,7 @@ "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" + "(0, spot.acc_cond(4, \"Fin(2) | Inf(3)\"))\n" ] } ], @@ -1451,7 +1451,7 @@ "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" + "(0, spot.acc_cond(6, \"Inf(1)\"))\n" ] } ], @@ -1473,7 +1473,7 @@ "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" + "(5, spot.acc_cond(6, \"Inf(4)\"))\n" ] } ], @@ -1483,11 +1483,40 @@ "print(acc3.fin_one())\n", "print(acc3.fin_one_extract())" ] + }, + { + "cell_type": "code", + "execution_count": 58, + "metadata": {}, + "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "(8, (Fin(1) & Inf(2)) | (Inf(3)&Inf(4)) | (Inf(5) & (Fin(1)|Fin(7))))\n", + "1\n", + "(1, spot.acc_cond(8, \"Inf(2) | Inf(5)\"))\n" + ] + } + ], + "source": [ + "acc4 = spot.acc_cond('Fin(1)&Inf(2)|Inf(3)&Inf(4)|Inf(5)&(Fin(1)|Fin(7))')\n", + "print(acc4)\n", + "print(acc4.fin_one())\n", + "print(acc4.fin_one_extract())" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { "kernelspec": { - "display_name": "Python 3", + "display_name": "Python 3 (ipykernel)", "language": "python", "name": "python3" }, @@ -1501,7 +1530,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.7.3" + "version": "3.10.5" } }, "nbformat": 4, diff --git a/tests/python/genem.py b/tests/python/genem.py index 0c9d0809a..962112ac0 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -305,14 +305,17 @@ def run_bench(automata): res3c = spot.generic_emptiness_check(aut) spot.generic_emptiness_check_select_version("spot210") res3d = spot.generic_emptiness_check(aut) + spot.generic_emptiness_check_select_version("spot211") + res3e = spot.generic_emptiness_check(aut) + spot.generic_emptiness_check_select_version("spot29") res2 = spot.remove_fin(aut).is_empty() res1 = generic_emptiness2(aut) res = (str(res1)[0] + str(res2)[0] + str(res3a)[0] + str(res3b)[0] + str(res3c)[0] + str(res3d)[0] - + str(res4)[0] + str(res5)[0]) + + str(res3e)[0] + str(res4)[0] + str(res5)[0]) print(res) - tc.assertIn(res, ('TTTTTTTT', 'FFFFFFFF')) - if res == 'FFFFFFFF': + tc.assertIn(res, ('TTTTTTTTT', 'FFFFFFFFF')) + if res == 'FFFFFFFFF': run3 = spot.generic_accepting_run(aut) tc.assertTrue(run3.replay(spot.get_cout()))