From 7f0ef7ad59d8cb01eb2284866dd21a040ac77f96 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 6 Mar 2020 09:56:16 +0100 Subject: [PATCH] genem: improve the worst case * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Improve the worst case by not recurring twice into each disjunct individually. Keep the previous two implementation available and add a function generic_emptiness_check_select_version() so we can benchmark the difference. * tests/python/genem.py: Test the three versions. --- spot/twaalgos/genem.cc | 88 ++++++++++++++++++++++++++++++++---------- spot/twaalgos/genem.hh | 21 +++++++++- tests/python/genem.py | 19 +++++---- 3 files changed, 100 insertions(+), 28 deletions(-) diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 5760b6d02..80d096533 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -23,6 +23,25 @@ namespace spot { + namespace + { + enum genem_version_t { spot28, atva19, spot29 }; + static genem_version_t genem_version = spot29; + } + + void generic_emptiness_check_select_version(const char* emversion) + { + if (emversion == nullptr || !strcasecmp(emversion, "spot29")) + genem_version = spot29; + else if (!strcasecmp(emversion, "spot28")) + genem_version = spot28; + else if (!strcasecmp(emversion, "atva19")) + genem_version = atva19; + else + throw std::invalid_argument("generic_emptiness_check version should" + " be one of {spot28, atva19, spot29}"); + } + namespace { static bool @@ -65,26 +84,55 @@ namespace spot acc_cond acc = autacc.restrict_to(sets); acc = acc.remove(si.common_sets_of(scc), false); - for (const acc_cond& disjunct: acc.top_disjuncts()) - if (acc_cond::mark_t fu = disjunct.fin_unit()) - { - if (!scc_split_check - (si, scc, disjunct.remove(fu, true), run, fu)) - return false; - } - else - { - int fo = disjunct.fin_one(); - assert(fo >= 0); - // Try to accept when Fin(fo) == true - acc_cond::mark_t fo_m = {(unsigned) fo}; - if (!scc_split_check - (si, scc, disjunct.remove(fo_m, true), run, fo_m)) - return false; - // Try to accept when Fin(fo) == false - if (!is_scc_empty(si, scc, disjunct.force_inf(fo_m), run, tocut)) - return false; - } + auto generic_recurse = + [&] (const acc_cond& subacc) + { + int fo = (SPOT_UNLIKELY(genem_version == spot28) + ? acc.fin_one() : subacc.fin_one()); + assert(fo >= 0); + // Try to accept when Fin(fo) == true + acc_cond::mark_t fo_m = {(unsigned) fo}; + if (!scc_split_check + (si, scc, subacc.remove(fo_m, true), run, fo_m)) + return false; + // Try to accept when Fin(fo) == false + if (!is_scc_empty(si, scc, subacc.force_inf(fo_m), run, tocut)) + return false; + return true; + }; + + if (SPOT_LIKELY(genem_version == spot29)) + { + acc_cond::acc_code rest = acc_cond::acc_code::f(); + for (const acc_cond& disjunct: acc.top_disjuncts()) + if (acc_cond::mark_t fu = disjunct.fin_unit()) + { + if (!scc_split_check + (si, scc, disjunct.remove(fu, true), run, fu)) + return false; + } + else + { + rest |= disjunct.get_acceptance(); + } + if (!rest.is_f() && !generic_recurse(acc_cond(acc.num_sets(), rest))) + return false; + } + else + { + for (const acc_cond& disjunct: acc.top_disjuncts()) + if (acc_cond::mark_t fu = disjunct.fin_unit()) + { + if (!scc_split_check + (si, scc, disjunct.remove(fu, true), run, fu)) + return false; + } + else + { + if (!generic_recurse(disjunct)) + return false; + } + } return true; } diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index c6b3d55a2..700a52b44 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2020 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -61,4 +61,23 @@ namespace spot SPOT_API bool generic_emptiness_check_for_scc(const scc_info& si, unsigned scc, const acc_cond& forced_acc); + + + /// \ingroup emptiness_check_algorithms + /// + /// Select the version of the generic-emptiness check to use, this + /// is mainly for benchmarking purpose. + /// + /// We currently have three versions: + /// - "spot28" is similar to the algorithm described our ATVA'19 paper + /// \cite baier.19.atva , however it has an implementation bug + /// that cause superfluous recursive calls to be performed (the + /// result is still correct. + /// - "atva19" is similar to the algorithm described our ATVA'19 paper + /// \cite baier.19.atva , with the above bug fixed. + /// - "spot29" improves upon the worst case of atva19. This is + /// the default. + SPOT_API void + generic_emptiness_check_select_version(const char* emversion = nullptr); + } diff --git a/tests/python/genem.py b/tests/python/genem.py index 01f98344d..e32656976 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2019 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -283,17 +283,22 @@ def is_scc_empty2(si, scc_num, acc=None): def run_bench(automata): for aut in automata: - # Make sure our three implementation behave identically + # Make sure all our implementations behave identically res5 = is_empty2(aut) res4 = is_empty1(aut) - res3 = spot.generic_emptiness_check(aut) + spot.generic_emptiness_check_select_version("spot28") + res3a = spot.generic_emptiness_check(aut) + spot.generic_emptiness_check_select_version("atva19") + res3b = spot.generic_emptiness_check(aut) + spot.generic_emptiness_check_select_version("spot29") + res3c = spot.generic_emptiness_check(aut) res2 = spot.remove_fin(aut).is_empty() res1 = generic_emptiness2(aut) - res = (str(res1)[0] + str(res2)[0] + str(res3)[0] - + str(res4)[0] + str(res5)[0]) + res = (str(res1)[0] + str(res2)[0] + str(res3a)[0] + + str(res3b)[0] + str(res3c)[0] + str(res4)[0] + str(res5)[0]) print(res) - assert res in ('TTTTT', 'FFFFF') - if res == 'FFFFF': + assert res in ('TTTTTTT', 'FFFFFFF') + if res == 'FFFFFFF': run3 = spot.generic_accepting_run(aut) assert run3.replay(spot.get_cout()) is True