From b17376879d82b84b9a55a934706dbb8d7f0247aa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 22 Jul 2020 16:31:53 +0200 Subject: [PATCH] translate: add a quick syntactic simplification before relabeling This fixes #412. * spot/twaalgos/translate.cc: Add the quick syntactic simplification. * spot/twaalgos/relabel.cc: Do not register old unused APs. * tests/core/ltl2tgba2.test: Add test case. * tests/core/bdd.test, tests/python/automata.ipynb: Adjust. * NEWS: Mention this. --- NEWS | 3 ++ spot/twaalgos/relabel.cc | 5 ++ spot/twaalgos/translate.cc | 64 +++++++++++++++++------- tests/core/bdd.test | 4 +- tests/core/ltl2tgba2.test | 4 +- tests/python/automata.ipynb | 98 ++++++++++++++++++------------------- 6 files changed, 108 insertions(+), 70 deletions(-) diff --git a/NEWS b/NEWS index 65a99887b..718118058 100644 --- a/NEWS +++ b/NEWS @@ -45,6 +45,9 @@ New in spot 2.9.3.dev (not yet released) file. With this refactoring, we can retrieve both a kripke or a kripkecube from a PINS file. + - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which + used to take ages are now instantaneous. (See issue #412.) + Bugs fixed: - Handle xor and <-> in a more natural way when translating diff --git a/spot/twaalgos/relabel.cc b/spot/twaalgos/relabel.cc index 5f3e78f62..22eddd893 100644 --- a/spot/twaalgos/relabel.cc +++ b/spot/twaalgos/relabel.cc @@ -32,6 +32,7 @@ namespace spot std::set newvars; vars.reserve(relmap->size()); bool bool_subst = false; + auto aplist = aut->ap(); for (auto& p: *relmap) { @@ -42,6 +43,10 @@ namespace spot throw std::runtime_error ("relabel_here: new labels should be Boolean formulas"); + // Don't attempt to rename APs that are not used. + if (std::find(aplist.begin(), aplist.end(), p.first) == aplist.end()) + continue; + int oldv = aut->register_ap(p.first); vars.emplace_back(oldv); if (p.second.is(op::ap)) diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 5ada74631..4415a6439 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -418,7 +418,7 @@ namespace spot if (simpl_owned_) { // Modify the options according to set_pref() and set_type(). - // We do it for all translation, but really only the first one + // We do it for all translations, but really only the first one // matters. auto& opt = simpl_owned_->options(); if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic)) @@ -436,33 +436,61 @@ namespace spot // sub-formulas that are Boolean but do not have common terms. // // This rewriting is enabled only if the formula - // 1) has some Boolean subformula - // 2) has more than relabel_bool_ atomic propositions (the default + // 1) has more than relabel_bool_ atomic propositions (the default // is 4, but this can be changed) + // 2) has some Boolean subformula // 3) relabel_bse() actually reduces the number of atomic // propositions. relabeling_map m; formula to_work_on = *f; if (relabel_bool_ > 0) { - bool has_boolean_sub = false; // that is not atomic std::set aps; - to_work_on.traverse([&](const formula& f) - { - if (f.is(op::ap)) - aps.insert(f); - else if (f.is_boolean()) - has_boolean_sub = true; - return false; - }); + atomic_prop_collect(to_work_on, &aps); unsigned atomic_props = aps.size(); - if (has_boolean_sub && (atomic_props >= (unsigned) relabel_bool_)) + + if (atomic_props >= (unsigned) relabel_bool_) { - formula relabeled = relabel_bse(to_work_on, Pnn, &m); - if (m.size() < atomic_props) - to_work_on = relabeled; - else - m.clear(); + // Make a very quick simplification path before for + // Boolean subformulas, only only syntactic rules. This + // is to help getting formulas of the form + // FGp1 & FGp2 & ... & FGp32 + // into the shape + // FG(p1 & p2 & ... & p32) + // where relabeling will be much more efficient. + // + // We reuse all options of simpl_ (to preserve things + // like keep_top_xor or favor_event_univ). + tl_simplifier_options options = simpl_->options(); + options.synt_impl = false; + options.containment_checks = false; + options.containment_checks_stronger = false; + options.nenoform_stop_on_boolean = true; + options.boolean_to_isop = false; + tl_simplifier simpl(options, simpl_->get_dict()); + to_work_on = simpl.simplify(to_work_on); + + // Do we have Boolean subformulas that are not atomic + // propositions? + bool has_boolean_sub = false; + to_work_on.traverse([&](const formula& f) + { + if (f.is_boolean()) + { + has_boolean_sub = true; + return true; + } + return false; + }); + + if (has_boolean_sub) + { + formula relabeled = relabel_bse(to_work_on, Pnn, &m); + if (m.size() < atomic_props) + to_work_on = relabeled; + else + m.clear(); + } } } diff --git a/tests/core/bdd.test b/tests/core/bdd.test index 0b17fb586..e70216a11 100755 --- a/tests/core/bdd.test +++ b/tests/core/bdd.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de +# Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -30,7 +30,7 @@ grep 'spot: BDD package initialized' err # This value below, which is the number of time we need to garbage # collect might change if we improve the tool or change the way BuDDy # is initialized. -test 63 = `grep -c 'spot: BDD GC' err` +test 11 = `grep -c 'spot: BDD GC' err` # Minimal size for this automaton. # See also https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf test "147,207" = `autfilt --stats=%s,%e out` diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 1878e3efd..227ee5b99 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -27,7 +27,7 @@ # commonly use as benchmark change, we want to notice it. set -e -genltl --dac --eh --sb --hkrss --p --format=%F,%L,%f >pos +genltl --dac --eh --sb --hkrss --p --and-fg=32 --format=%F,%L,%f >pos (cat pos; ltlfilt --negate pos/3 --format='!%<,%f') | ltlfilt -u -F-/3 >formulas @@ -201,6 +201,7 @@ p-patterns,16, 2,16, 2,16, 2,16, 2,16 p-patterns,17, 3,20, 3,20, 3,20, 3,20 p-patterns,18, 5,36, 5,36, 5,36, 5,36 p-patterns,20, 1,8, 1,8, 3,24, 3,24 +and-fg,32, 2,4294967298, 2,4294967298, 2,4294967298, 2,4294967298 !dac-patterns,1, 2,4, 2,4, 2,4, 2,4 !dac-patterns,2, 3,10, 3,10, 3,10, 3,10 !dac-patterns,3, 3,12, 3,12, 3,12, 3,12 @@ -357,6 +358,7 @@ p-patterns,20, 1,8, 1,8, 3,24, 3,24 !p-patterns,17, 4,31, 4,31, 4,31, 4,31 !p-patterns,18, 6,43, 6,43, 6,43, 6,43 !p-patterns,20, 3,16, 3,16, 3,16, 3,16 +!and-fg,32, 1,4294967296, 1,4294967296, 2,8589934592, 2,8589934592 EOF diff output expected diff --git a/tests/python/automata.ipynb b/tests/python/automata.ipynb index 8c039830a..c903015cc 100644 --- a/tests/python/automata.ipynb +++ b/tests/python/automata.ipynb @@ -178,7 +178,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7cbd50> >" + " *' at 0x7f37382c04b0> >" ] }, "execution_count": 2, @@ -657,7 +657,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7cf480> >" + " *' at 0x7f37382c09f0> >" ] }, "execution_count": 6, @@ -733,7 +733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7cfc00> >" + " *' at 0x7f37382c00f0> >" ] }, "execution_count": 7, @@ -816,7 +816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7cf3f0> >" + " *' at 0x7f37382c0c00> >" ] }, "execution_count": 8, @@ -1026,30 +1026,30 @@ "\n", "\n", "1\n", - "\n", - "\n", - "1\n", + "\n", + "\n", + "1\n", "\n", "\n", "\n", "6->1\n", - "\n", - "\n", - "a & !b & !c\n", + "\n", + "\n", + "!a & b & !c\n", "\n", "\n", "\n", "2\n", - "\n", - "\n", - "2\n", + "\n", + "\n", + "2\n", "\n", "\n", "\n", "6->2\n", - "\n", - "\n", - "!a & b & !c\n", + "\n", + "\n", + "a & !b & !c\n", "\n", "\n", "\n", @@ -1103,16 +1103,16 @@ "\n", "\n", "1->1\n", - "\n", - "\n", - "a\n", + "\n", + "\n", + "b\n", "\n", "\n", "\n", "2->2\n", - "\n", - "\n", - "b\n", + "\n", + "\n", + "a\n", "\n", "\n", "\n", @@ -1121,9 +1121,9 @@ "\n", "!b & c\n", "\n", - "\n", + "\n", "\n", - "3->2\n", + "3->1\n", "\n", "\n", "b & !c\n", @@ -1142,9 +1142,9 @@ "\n", "!a & c\n", "\n", - "\n", + "\n", "\n", - "4->1\n", + "4->2\n", "\n", "\n", "a & !c\n", @@ -1159,16 +1159,16 @@ "\n", "\n", "5->1\n", - "\n", - "\n", - "a & !b\n", + "\n", + "\n", + "!a & b\n", "\n", "\n", "\n", "5->2\n", - "\n", - "\n", - "!a & b\n", + "\n", + "\n", + "a & !b\n", "\n", "\n", "\n", @@ -1349,7 +1349,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4930> >" + " *' at 0x7f37382c05a0> >" ] }, "execution_count": 12, @@ -1463,7 +1463,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4cc0> >" + " *' at 0x7f37382c0ab0> >" ] }, "execution_count": 13, @@ -1594,7 +1594,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4990> >" + " *' at 0x7f37382df240> >" ] }, "execution_count": 14, @@ -1816,7 +1816,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4b70> >" + " *' at 0x7f37382dfc90> >" ] }, "metadata": {}, @@ -2012,7 +2012,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4e40> >" + " *' at 0x7f37382dfc30> >" ] }, "metadata": {}, @@ -2191,7 +2191,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4c00> >" + " *' at 0x7f37382dfed0> >" ] }, "metadata": {}, @@ -2339,7 +2339,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f658bbc90> >" + " *' at 0x7f37382dfa80> >" ] }, "metadata": {}, @@ -2528,7 +2528,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4c00> >" + " *' at 0x7f37382df1b0> >" ] }, "execution_count": 19, @@ -2604,7 +2604,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7e2f90> >" + " *' at 0x7f37382dfae0> >" ] }, "execution_count": 20, @@ -3154,7 +3154,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7f18d0> >" + " *' at 0x7f37382dfe10> >" ] }, "metadata": {}, @@ -3254,7 +3254,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7d4b70> >" + " *' at 0x7f37382c0e10> >" ] }, "execution_count": 24, @@ -3327,7 +3327,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7f1330> >" + " *' at 0x7f37382dfba0> >" ] }, "execution_count": 25, @@ -3498,7 +3498,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7f1450> >" + " *' at 0x7f37382dfc00> >" ] }, "execution_count": 27, @@ -3581,7 +3581,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7f18d0> >" + " *' at 0x7f37382dfe10> >" ] }, "metadata": {}, @@ -3646,7 +3646,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7f18d0> >" + " *' at 0x7f37382dfe10> >" ] }, "metadata": {}, @@ -3733,7 +3733,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f9f5d7f18d0> >" + " *' at 0x7f37382dfe10> >" ] }, "execution_count": 29, @@ -3766,7 +3766,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.3" + "version": "3.8.4" } }, "nbformat": 4,