diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 603b5eed6..e49f5b07c 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -25,7 +25,7 @@ namespace spot { namespace { - enum genem_version_t { spot28, atva19, spot29 }; + enum genem_version_t { spot28, atva19, spot29, spot210 }; static genem_version_t genem_version = spot29; } @@ -33,13 +33,15 @@ namespace spot { if (emversion == nullptr || !strcasecmp(emversion, "spot29")) genem_version = spot29; + else if (!strcasecmp(emversion, "spot210")) + genem_version = spot210; 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}"); + throw std::invalid_argument("generic_emptiness_check version should be " + "one of {spot28, atva19, spot29, spot210}"); } namespace @@ -108,34 +110,39 @@ namespace spot acc_cond acc = autacc.restrict_to(sets); acc = acc.remove(si.common_sets_of(scc), false); - if (SPOT_LIKELY(genem_version == spot29 || !EarlyStop)) + if (SPOT_LIKELY(genem_version == spot210 || !EarlyStop)) + do + { + auto [fo, fpart] = acc.fin_one_extract(); + assert(fo >= 0); + // 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)) + 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 == spot29) do { acc_cond::acc_code rest = acc_cond::acc_code::f(); - if (EarlyStop) - { - 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), extra, fu)) - if constexpr (EarlyStop) - return false; - } - else - { - rest |= disjunct.get_acceptance(); - } - if (rest.is_f()) - break; - } - else - { - rest = acc.get_acceptance(); - if (acc_cond::mark_t fu = rest.fin_unit()) - return scc_split_check - (si, scc, rest.remove(fu, true), extra, fu); - } + 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), extra, fu)) + if constexpr (EarlyStop) + return false; + } + else + { + rest |= disjunct.get_acceptance(); + } + if (rest.is_f()) + break; acc_cond subacc(acc.num_sets(), std::move(rest)); int fo = subacc.fin_one(); assert(fo >= 0); diff --git a/spot/twaalgos/genem.hh b/spot/twaalgos/genem.hh index 3ffd795b9..2d1ded4c7 100644 --- a/spot/twaalgos/genem.hh +++ b/spot/twaalgos/genem.hh @@ -99,6 +99,8 @@ namespace spot /// \cite baier.19.atva , with the above bug fixed. /// - "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. SPOT_API void generic_emptiness_check_select_version(const char* emversion = nullptr); diff --git a/spot/twaalgos/zlktree.cc b/spot/twaalgos/zlktree.cc index c58a34e6a..fba8e2039 100644 --- a/spot/twaalgos/zlktree.cc +++ b/spot/twaalgos/zlktree.cc @@ -92,15 +92,15 @@ namespace spot { max_models(cond.remove(fu, true), colors - fu, out); } - // Otherwise, we simply have to pick a random Fin(x) and see if - // we can satisfy the condition when x is present or absent. In - // this case, we do not know whether the generated models will - // be maximal, so this justifies the inclusion checks between - // models at the top of this function. - else if (int fo = cond.fin_one(); fo >= 0) + // Otherwise, we simply have to pick some arbitrary Fin(x) and + // see if we can satisfy the condition when x is present or + // absent. In this case, we do not know whether the generated + // models will be maximal, so this justifies the inclusion + // checks between models at the top of this function. + else if (auto [fo, fpart] = cond.fin_one_extract(); fo >= 0) { acc_cond::mark_t fo_m = {(unsigned) fo}; - max_models(cond.remove(fo_m, true), colors - fo_m, out); + max_models(fpart.remove(fo_m, true), colors - fo_m, out); max_models(cond.remove(fo_m, false), colors, out); } } diff --git a/tests/python/genem.py b/tests/python/genem.py index e32656976..efc0a84a8 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2020 Laboratoire de Recherche et Développement de l'Epita +# Copyright (C) 2018-2021 Laboratoire de Recherche et Développement de l'Epita # (LRDE). # # This file is part of Spot, a model checking library. @@ -292,13 +292,16 @@ def run_bench(automata): res3b = spot.generic_emptiness_check(aut) spot.generic_emptiness_check_select_version("spot29") res3c = spot.generic_emptiness_check(aut) + spot.generic_emptiness_check_select_version("spot210") + res3d = spot.generic_emptiness_check(aut) 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(res4)[0] + str(res5)[0]) + + str(res3b)[0] + str(res3c)[0] + str(res3d)[0] + + str(res4)[0] + str(res5)[0]) print(res) - assert res in ('TTTTTTT', 'FFFFFFF') - if res == 'FFFFFFF': + assert res in ('TTTTTTTT', 'FFFFFFFF') + if res == 'FFFFFFFF': run3 = spot.generic_accepting_run(aut) assert run3.replay(spot.get_cout()) is True