From 69c821154cbe91b7846a5d760acd4c2b001d7af5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 15 Sep 2020 16:57:33 +0200 Subject: [PATCH] postproc: add simul-max and wdba-det-max options * NEWS, bin/spot-x.cc: Document them. * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement them. * tests/python/stutter-inv.ipynb: Adjust result. * tests/core/minusx.test: Add test case. --- NEWS | 25 ++++++++ bin/spot-x.cc | 12 +++- spot/twaalgos/postproc.cc | 29 ++++++++- spot/twaalgos/postproc.hh | 2 + tests/core/minusx.test | 7 ++- tests/python/stutter-inv.ipynb | 110 ++++++++++++++++----------------- 6 files changed, 125 insertions(+), 60 deletions(-) diff --git a/NEWS b/NEWS index 1e87d29fc..261418295 100644 --- a/NEWS +++ b/NEWS @@ -79,6 +79,31 @@ New in spot 2.9.4.dev (not yet released) - print_dot() will display states from player 1 using a diamond shape. + - spot::postproc has two extra configuration variables that are meant + to speedup the processing of large automata. + + simul-max Number of states above which simulation-based + reductions are skipped. Defaults to 512. Set to 0 + to disable. This also applies to the + simulation-based optimization of the + determinization algorithm. + wdba-det-max Maximum number of additional states allowed in + intermediate steps of WDBA-minimization. If the + number of additional states reached in the + powerset construction or in the followup products + exceeds this value, WDBA-minimization is aborted. + Defaults to 4096. Set to 0 to disable. This limit + is ignored when -D used or when det-max-states is + set. + + The reason for disabling simulation-based reduction above 512 + states is that the current implementation uses one BDD variable + per state, and makes a number of BDD operations that is quadratic + in the number of states. Similarly, WDBA-mininimization is used + with --small in the off chance that it might produce a smaller + automaton, but we should not waste too much space and time trying + that. + Python: - Bindings for functions related to parity games. diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 007e23233..ce15fed27 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -140,12 +140,16 @@ The default is 3, except when option --low is specified, in which case \ the default is 1.") }, { DOC("ba-simul", "Set to 0 to disable simulation-based reductions \ on automata where state-based acceptance must be preserved (e.g., \ -after degeneralization has been performed). The name suggests this applies \ +after degeneralization has been performed). The name suggests this applies \ only to Büchi automata for historical reasons; it really applies to any \ state-based acceptance nowadays. \ Set to 1 to use only direct simulation. Set to 2 to use only reverse \ simulation. Set to 3 to iterate both direct and reverse simulations. \ The default is 3 in --high mode, and 0 otherwise.") }, + { DOC("simul-max", "Number of states above which simulation-based \ +reductions are skipped. Defaults to 512. Set to 0 to disable. This also \ +applies to the simulation-based optimization of the determinization \ +algorithm.") }, { DOC("relabel-bool", "If set to a positive integer N, a formula \ with N atomic propositions or more will have its Boolean subformulas \ abstracted as atomic propositions during the translation to automaton. \ @@ -156,6 +160,12 @@ this value to 0 will disable the rewriting.") }, always try it, or 2 to attempt it only on syntactic obligations or on automata \ that are weak and deterministic. The default is 1 in --high mode, else 2 in \ --medium or --deterministic modes, else 0 in --low mode.") }, + { DOC("wdba-det-max", "Maximum number of additional states allowed \ +in intermediate steps of WDBA-minimization. If the number of additional \ +states reached in the powerset construction or in the followup products \ +exceeds this value, WDBA-minimization is aborted. \ +Defaults to 4096. Set to 0 to disable. This limit is ignored when -D used \ +or when det-max-states is set.") }, { DOC("tba-det", "Set to 1 to attempt a powerset determinization \ if the TGBA is not already deterministic. Doing so will degeneralize \ the automaton. This is disabled by default, unless sat-minimize is set.") }, diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 36d0345bf..36c6af003 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -85,6 +85,8 @@ namespace spot state_based_ = opt->get("state-based", 0); wdba_minimize_ = opt->get("wdba-minimize", -1); gen_reduce_parity_ = opt->get("gen-reduce-parity", 1); + simul_max_ = opt->get("simul-max", 512); + wdba_det_max_ = opt->get("wdba-det-max", 4096); if (sat_acc_ && sat_minimize_ == 0) sat_minimize_ = 1; // Dicho. @@ -110,6 +112,11 @@ namespace spot twa_graph_ptr postprocessor::do_simul(const twa_graph_ptr& a, int opt) const { + if (simul_max_ > 0 && static_cast(simul_max_) < a->num_states()) + return a; + + // FIXME: simulation-based reduction how have work-arounds for + // non-separated sets, so we can probably try them. if (!has_separate_sets(a)) return a; switch (opt) @@ -131,6 +138,8 @@ namespace spot { if (ba_simul_ <= 0) return a; + if (simul_max_ > 0 && static_cast(simul_max_) < a->num_states()) + return a; switch (opt) { case 0: @@ -386,7 +395,16 @@ namespace spot if (wdba_minimize) { bool reject_bigger = (PREF_ == Small) && (level_ <= Medium); - dba = minimize_obligation(a, f, nullptr, reject_bigger, aborter); + output_aborter* ab = aborter; + output_aborter wdba_aborter(wdba_det_max_ > 0 ? + (static_cast(wdba_det_max_) + + a->num_states()) : -1U); + if (!ab && PREF_ != Deterministic) + ab = &wdba_aborter; + dba = minimize_obligation(a, f, nullptr, reject_bigger, ab); + if (!dba) + std::cerr << "DBA aborted\n"; + if (dba && dba->prop_inherently_weak().is_true() && dba->prop_universal().is_true()) @@ -502,8 +520,13 @@ namespace spot if ((PREF_ == Deterministic && (type_ == Generic || want_parity)) && !dba) { - dba = tgba_determinize(to_generalized_buchi(sim), - false, det_scc_, det_simul_, det_stutter_, + bool det_simul = det_simul_; + auto tba = to_generalized_buchi(sim); + if (simul_max_ > 0 + && static_cast(simul_max_) < tba->num_states()) + det_simul = false; + dba = tgba_determinize(tba, + false, det_scc_, det_simul, det_stutter_, aborter); // Setting det-max-states or det-max-edges may cause tgba_determinize // to fail. diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 3fbd07060..c084078fa 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -254,6 +254,8 @@ namespace spot int gen_reduce_parity_ = 1; bool state_based_ = false; int wdba_minimize_ = -1; + int simul_max_ = 512; + int wdba_det_max_ = 4096; }; /// @} } diff --git a/tests/core/minusx.test b/tests/core/minusx.test index 96a518034..2ac9ec155 100755 --- a/tests/core/minusx.test +++ b/tests/core/minusx.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# Copyright (C) 2016, 2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -34,3 +34,8 @@ grep -- "- 'bar'" error ltl2tgba -f FGa | autfilt -D | autfilt --sat-minimize='acc="co-Buchi",other' 2>error && exit 1 grep "autfilt: option 'other' was not used" error + +# Make sure wdba-det-max has an effect +f='G(!p0 | (!p2 U (p1 | (!p2 & p3 & X(!p2 U p4)))) | G!p1)' +test 4,1 = `ltl2tgba --stats=%s,%d "$f"` +test 6,0 = `ltl2tgba -x wdba-det-max=4 --stats=%s,%d "$f"` diff --git a/tests/python/stutter-inv.ipynb b/tests/python/stutter-inv.ipynb index 863a71e26..4e0f142f1 100644 --- a/tests/python/stutter-inv.ipynb +++ b/tests/python/stutter-inv.ipynb @@ -302,7 +302,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdf9af30> >" + " *' at 0x7faad816be40> >" ] }, "metadata": {}, @@ -603,7 +603,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdfa3f60> >" + " *' at 0x7faad816be70> >" ] }, "metadata": {}, @@ -812,7 +812,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdfa3f60> >" + " *' at 0x7faad816be70> >" ] }, "metadata": {}, @@ -964,7 +964,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdfa9210> >" + " *' at 0x7faad8057690> >" ] }, "metadata": {}, @@ -1062,7 +1062,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdf8e900> >" + " *' at 0x7faad8253210> >" ] }, "metadata": {}, @@ -1272,7 +1272,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdfa97b0> >" + " *' at 0x7faad8057ea0> >" ] }, "metadata": {}, @@ -1401,7 +1401,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdfaed20> >" + " *' at 0x7faad8247a20> >" ] }, "metadata": {}, @@ -1452,87 +1452,87 @@ "\n", "\n", - "\n", - "\n", - "\n", - "Inf(\n", - "⓿\n", - ")\n", - "[Büchi]\n", + "\n", + "\n", + "\n", + "Inf(\n", + "⓿\n", + ")\n", + "[Büchi]\n", "\n", "\n", "\n", "3\n", - "\n", - "3\n", + "\n", + "3\n", "\n", "\n", "\n", "I->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "0\n", - "\n", - "0\n", - "⓿\n", + "\n", + "0\n", "\n", "\n", "\n", "3->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "!b\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", + "⓿\n", "\n", "\n", "\n", "3->1\n", - "\n", - "\n", - "!b\n", - "\n", - "\n", - "\n", - "0->0\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "2\n", - "⓿\n", + "\n", + "2\n", + "⓿\n", "\n", - "\n", - "\n", - "1->2\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "0->2\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", + "\n", + "\n", + "\n", + "1->1\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7fb4fdf45d80> >" + " *' at 0x7faad8057450> >" ] }, "metadata": {}, @@ -1792,7 +1792,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdf457e0> >" + " *' at 0x7faad816b390> >" ] }, "metadata": {}, @@ -2106,7 +2106,7 @@ "\n" ], "text/plain": [ - " *' at 0x7fb4fdf457e0> >" + " *' at 0x7faad816b390> >" ] }, "metadata": {}, @@ -2347,7 +2347,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.2" + "version": "3.8.6rc1" } }, "nbformat": 4,