diff --git a/python/spot/impl.i b/python/spot/impl.i index 502770fcb..f95270e21 100644 --- a/python/spot/impl.i +++ b/python/spot/impl.i @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2009-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -564,6 +564,16 @@ namespace std { swig::from(std::get<2>(v))); } %} +// Must occur before the twa declaration +%typemap(out) SWIGTYPE spot::acc_cond::fin_unit_one_split_improved %{ + { + 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 07aac36f9..d73af33b0 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2015-2023 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -2707,8 +2707,9 @@ 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) + // Check if pos contains Fin(f) in a substree + template + bool has_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f) { auto sub = pos - pos->sub.size; do @@ -2719,7 +2720,10 @@ namespace spot --pos; break; case acc_cond::acc_op::Or: - pos -= pos->sub.size + 1; + if constexpr (top_conjunct_only) + pos -= pos->sub.size + 1; + else + --pos; break; case acc_cond::acc_op::Fin: if (pos[-1].mark & f) @@ -2736,6 +2740,12 @@ namespace spot return false; } + // Check whether pos looks like Fin(f) or Fin(f)&rest + bool is_conj_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f) + { + return has_fin(pos, f); + } + acc_cond::acc_code extract_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f) { @@ -2772,6 +2782,7 @@ namespace spot return {}; } + template std::pair split_top_fin(const acc_cond::acc_word* pos, acc_cond::mark_t f) { @@ -2798,6 +2809,17 @@ namespace spot tmp |= std::move(left); std::swap(tmp, left); } + else if (deeper_check + && has_top_fin(pos) == -1 + && has_fin(pos, f)) + { + auto tmp = strip_rec(pos, f, true, false); + tmp |= std::move(left); + std::swap(tmp, left); + tmp = force_inf_rec(pos, f); + tmp |= std::move(right); + std::swap(tmp, right); + } else { acc_cond::acc_code tmp(pos); @@ -2851,6 +2873,27 @@ namespace spot return {selected_fin, extract_fin(pos, fo_m), force_inf(fo_m)}; } + std::tuple + acc_cond::acc_code::fin_unit_one_split_improved() const + { + if (SPOT_UNLIKELY(is_t() || is_f())) + err: + throw std::runtime_error("fin_unit_one_split_improved(): 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 1c460cfc4..1b46e4024 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2014-2023 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -1300,21 +1300,26 @@ namespace spot /// \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 condition is a disjunction and one of the disjunct has + /// the shape `...&Fin(i)&...`, then this will return (i, left, + /// right), where left is all disjunct of this form (with Fin(i) + /// replaced by true), 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. + /// is set to the entire formula (with Fin(i) replaced by true), + /// 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; + std::tuple + fin_unit_one_split_improved() const; + /// @} /// \brief Help closing accepting or rejecting cycle. /// @@ -2258,25 +2263,34 @@ namespace spot /// \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 condition is a disjunction and one of the disjunct has + /// the shape `...&Fin(i)&...`, then this will return (i, left, + /// right), where left is all disjunct of this form (with Fin(i) + /// replaced by true), 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. + /// is set to the entire formula (with Fin(i) replaced by true), + /// 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)}}; } + std::tuple + fin_unit_one_split_improved() const + { + auto [f, l, r] = code_.fin_unit_one_split_improved(); + return {f, {num_sets(), std::move(l)}, {num_sets(), std::move(r)}}; + } + /// @} /// \brief Return the top-level disjuncts. /// diff --git a/spot/twaalgos/genem.cc b/spot/twaalgos/genem.cc index 237b10118..0b0d1fd5f 100644 --- a/spot/twaalgos/genem.cc +++ b/spot/twaalgos/genem.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2022 Laboratoire de Recherche et Developpement +// Copyright (C) 2017-2023 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, spot211 }; + enum genem_version_t { spot28, atva19, spot29, spot210, spot211, spot212 }; 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, "spot212")) + genem_version = spot212; else if (!strcasecmp(emversion, "spot211")) genem_version = spot211; else if (!strcasecmp(emversion, "spot210")) @@ -44,7 +46,7 @@ namespace spot else throw std::invalid_argument("generic_emptiness_check version should be " "one of {spot28, atva19, spot29, spot210, " - "spot211}"); + "spot211, spot212}"); } namespace @@ -87,7 +89,9 @@ 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) + if (genem_version == spot211 + || genem_version == spot212 + || genem_version == spot210) tocut |= acc.fin_unit(); scc_and_mark_filter filt(si, scc, tocut); filt.override_acceptance(acc); @@ -144,6 +148,20 @@ namespace spot } while (!acc.is_f()); } + else if (genem_version == spot212) + { + do + { + auto [fo, fpart, rest] = acc.fin_unit_one_split_improved(); + 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/tests/python/genem.py b/tests/python/genem.py index 962112ac0..970fe705b 100644 --- a/tests/python/genem.py +++ b/tests/python/genem.py @@ -1,5 +1,5 @@ # -*- mode: python; coding: utf-8 -*- -# Copyright (C) 2018-2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2018-2023 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -307,15 +307,18 @@ def run_bench(automata): 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("spot212") + res3f = 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(res3e)[0] + str(res4)[0] + str(res5)[0]) + + str(res3e)[0] + str(res3f)[0] + str(res4)[0] + + str(res5)[0]) print(res) - tc.assertIn(res, ('TTTTTTTTT', 'FFFFFFFFF')) - if res == 'FFFFFFFFF': + tc.assertIn(res, ('TTTTTTTTTT', 'FFFFFFFFFF')) + if res == 'FFFFFFFFFF': run3 = spot.generic_accepting_run(aut) tc.assertTrue(run3.replay(spot.get_cout()))