From 110b052b7d9ba1cc198af7b3a827cef2adf9564c Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Mon, 28 Aug 2023 22:45:44 +0200 Subject: [PATCH] translate: add a new relabel-overlap option Fixes issue #536. Also a part of issue #500. * spot/twaalgos/translate.hh, spot/twaalgos/translate.cc: Implement this new option. * bin/spot-x.cc, NEWS: Mention it. * tests/core/ltl2tgba2.test: Add the test case from issue #536. --- NEWS | 23 ++++++++++++++++ bin/spot-x.cc | 11 +++++++- spot/twaalgos/translate.cc | 54 +++++++++++++++++++++++++++++++------- spot/twaalgos/translate.hh | 5 ++-- tests/core/ltl2tgba2.test | 13 ++++++++- 5 files changed, 92 insertions(+), 14 deletions(-) diff --git a/NEWS b/NEWS index af455e012..251f5feb3 100644 --- a/NEWS +++ b/NEWS @@ -37,6 +37,29 @@ New in spot 2.11.6.dev (not yet released) replace boolean subformulas by fresh atomic propositions even if those subformulas share atomic propositions. + - spot::translate() has a new -x option "relabel-overlap=M" that + augments the existing "relabel-bool=N". By default, N=4, M=8. + When the formula to translate has more than N atomic propositions, + relabel_bse() is first called to attempt to rename non-overlaping + boolean subexpressions (i.e., no shared atomic proposition) in + order to reduce the number of atomic proposition, a source of + explonential explosion in several places of the translation + pipeline. This relabel-bool optimization exists since Spot 2.4. + The new feature is that if, after relabel-bool, the formula still + has more than M atomic propositions, then spot::translate() now + attempts to relabel boolean subexpressions even if they have + overlapping atomic propositions, in an attempt to reduce the + number of atomic proposition even more. Doing so has the slightly + unfortunate side effect of hindering some simplifications (because + the new atomic propositions hide their interactions), but it + usually incures a large speedup. (See Issue #500, Issue #536.) + + For instance on Alexandre's laptop, running + 'ltlsynt --tlsf SPIReadManag.tlsf --aiger' + with Spot 2.11.6 used to produce an AIG circuit with 48 nodes in + 36 seconds; it now produce an AIG circuit with 53 nodes in only + 0.1 second. + New in spot 2.11.6 (2023-08-01) Bug fixes: diff --git a/bin/spot-x.cc b/bin/spot-x.cc index 964710dc1..19721daeb 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -196,7 +196,16 @@ disabled, it is just an upper bound otherwise.") }, with N atomic propositions or more will have its Boolean subformulas \ abstracted as atomic propositions during the translation to automaton. \ This relabeling can speeds the translation if a few Boolean subformulas \ -use a large number of atomic propositions. By default N=4. Setting \ +use a large number of atomic propositions. This relabeling make sure \ +the subexpression that are replaced do not share atomic propositions. \ +By default N=4. Setting this value to 0 will disable the rewriting.") }, + { DOC("relabel-overlap", "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. \ +This version does not care about overlapping atomic propositions, so \ +it can cause the created temporary automata to have incompatible \ +combinations of atomic propositions that will be eventually be removed. \ +This relabeling is attempted after relabel-bool. By default N=8. Setting \ this value to 0 will disable the rewriting.") }, { DOC("wdba-minimize", "Set to 0 to disable WDBA-minimization, to 1 to \ always try it, or 2 to attempt it only on syntactic obligations or on automata \ diff --git a/spot/twaalgos/translate.cc b/spot/twaalgos/translate.cc index 339463426..7ad57347f 100644 --- a/spot/twaalgos/translate.cc +++ b/spot/twaalgos/translate.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018, 2020-2022 Laboratoire de Recherche et +// Copyright (C) 2013-2018, 2020-2023 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -38,6 +38,7 @@ namespace spot { comp_susp_ = early_susp_ = skel_wdba_ = skel_simul_ = 0; relabel_bool_ = 4; + relabel_overlap_ = 8; tls_impl_ = -1; ltl_split_ = true; exprop_ = -1; @@ -47,6 +48,7 @@ namespace spot return; relabel_bool_ = opt->get("relabel-bool", 4); + relabel_overlap_ = opt->get("relabel-overlap", 6); comp_susp_ = opt->get("comp-susp", 0); if (comp_susp_ == 1) { @@ -480,15 +482,23 @@ namespace spot // 2) has some Boolean subformula // 3) relabel_bse() actually reduces the number of atomic // propositions. + // + // If the formula still has more than relabel_overlap_ APs after + // the above, we try the more aggressive relabel_overlapping_bse() + // function. However after applying this function, we might have + // false edges. relabeling_map m; formula to_work_on = *f; - if (relabel_bool_ > 0) + if (relabel_bool_ > 0 || relabel_overlap_ > 0) { std::set aps; atomic_prop_collect(to_work_on, &aps); unsigned atomic_props = aps.size(); - if (atomic_props >= (unsigned) relabel_bool_) + if ((relabel_bool_ + && atomic_props >= (unsigned) relabel_bool_) + || (relabel_overlap_ + && atomic_props >= (unsigned) relabel_overlap_)) { // Make a very quick simplification path before for // Boolean subformulas, only only syntactic rules. This @@ -507,14 +517,15 @@ namespace spot 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); + formula simplified = 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()) + if (f.is_boolean() + && !f.is(op::ap, op::Not)) { has_boolean_sub = true; return true; @@ -524,11 +535,34 @@ namespace spot 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(); + if (relabel_bool_ + && atomic_props >= (unsigned) relabel_bool_) + { + formula relabeled = relabel_bse(to_work_on, Pnn, &m); + if (m.size() < atomic_props) + { + atomic_props = m.size(); + to_work_on = relabeled; + } + else + { + m.clear(); + } + } + if (relabel_overlap_ + && atomic_props >= (unsigned) relabel_overlap_) + { + relabeling_map m2; + formula relabeled = + relabel_overlapping_bse(simplified, Pnn, &m2); + if (m2.size() < atomic_props) + { + atomic_props = m2.size(); + to_work_on = relabeled; + std::swap(m, m2); + } + m2.clear(); + } } } } diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 8428a2f22..4e534b1f7 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018, 2020, 2022 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2013-2018, 2020, 2022, 2023 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -150,6 +150,7 @@ namespace spot int skel_wdba_; int skel_simul_; int relabel_bool_; + int relabel_overlap_; int tls_impl_; bool gf_guarantee_ = true; bool gf_guarantee_set_ = false; diff --git a/tests/core/ltl2tgba2.test b/tests/core/ltl2tgba2.test index 8397bbc85..6e64e7081 100755 --- a/tests/core/ltl2tgba2.test +++ b/tests/core/ltl2tgba2.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2009-2022 Laboratoire de Recherche et Développement de +# Copyright (C) 2009-2023 Laboratoire de Recherche et Développement de # l'Epita (LRDE). # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), # département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -516,3 +516,14 @@ f='G((a -> X((!a U b) | G!a)) & (a -> X(G!a | (!a U c))) & (a -> X(G!a (a -> X(G!a | (!a U g))) & (a -> X(G!a | (!a U h)))) & (GFa <-> (GFb & GFc & GFd & GFe & GFf & GFg & GFh))' test 128 = `ltl2tgba -G -D "$f" --stats=%s` + +# This used to die from out of memory after 5 minutes. See issue #536. +f='(TRUE & (G F ~v21)& (( G F v39 -> G F v23))) -> (TRUE & +(G F (v1 -> (v41 & v29)))& (G F (v3 -> (v42 & v29)))& (G F (v5 +-> (v43 & v29)))& (G F (v7 -> (v44 & v29)))& (G F (v9 -> (v45 & +v29)))& (G F (v11 -> (v46 & v29)))& (G F (v13 -> (v47 & v29)))& +(G F (v15 -> (v48 & v29)))& (G F (v17 -> (v49 & v29)))& (G F (v19 +-> (v50 & v29)))& (G F (v41 | (v1 | (v3 | (v5 | (v7 | (v9 | +(v11 | (v13 | (v15 | (v17 | v19))))))))))))' +ltl2tgba -p'min even' -D -C "$f" --stats='%s %e'>out +test '22 288' = "`cat out`"