From 0ba6949f7dd5d0cff778672ec5eb15de2416a5b5 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 20 Oct 2022 10:48:01 +0200 Subject: [PATCH] use bdd_restrict more Doing so reduced the number of GC passes tested in bdd.test, which is good. * spot/twaalgos/ltl2tgba_fm.cc: Simplify minato loops with bdd_restrict. * spot/twaalgos/synthesis.cc (split_2step): Use bdd_restrict instead of bdd_appex. * tests/core/bdd.test, tests/core/ltlf.test: Adjust test cases. --- spot/twaalgos/ltl2tgba_fm.cc | 35 +++++++++++++---------------------- spot/twaalgos/synthesis.cc | 4 +--- tests/core/bdd.test | 14 +++++++------- tests/core/ltlf.test | 12 ++++++------ 4 files changed, 27 insertions(+), 38 deletions(-) diff --git a/spot/twaalgos/ltl2tgba_fm.cc b/spot/twaalgos/ltl2tgba_fm.cc index 3566abc97..a354aaddd 100644 --- a/spot/twaalgos/ltl2tgba_fm.cc +++ b/spot/twaalgos/ltl2tgba_fm.cc @@ -900,8 +900,7 @@ namespace spot for (bdd label: minterms_of(all_props, var_set)) { formula dest = - dict_.bdd_to_sere(bdd_appex(res_ndet, label, bddop_and, - dict_.var_set)); + dict_.bdd_to_sere(bdd_restrict(res_ndet, label)); dest = formula::first_match(dest); if (to_concat_) dest = formula::Concat({dest, to_concat_}); @@ -995,9 +994,7 @@ namespace spot bdd all_props = bdd_existcomp(res, dict_.var_set); for (bdd label: minterms_of(all_props, var_set)) { - formula dest = - dict_.bdd_to_sere(bdd_appex(res, label, bddop_and, - dict_.var_set)); + formula dest = dict_.bdd_to_sere(bdd_restrict(res, label)); f2a_t::const_iterator i = f2a_.find(dest); if (i != f2a_.end() && i->second.first == nullptr) continue; @@ -1471,9 +1468,7 @@ namespace spot for (bdd label: minterms_of(all_props, var_set)) { formula dest = - dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and, - dict_.var_set)); - + dict_.bdd_to_sere(bdd_restrict(f1, label)); formula dest2 = formula::binop(o, dest, node[1]); bool unamb = dict_.unambiguous; if (!dest2.is_ff()) @@ -1552,9 +1547,7 @@ namespace spot for (bdd label: minterms_of(all_props, var_set)) { formula dest = - dict_.bdd_to_sere(bdd_appex(f1, label, bddop_and, - dict_.var_set)); - + dict_.bdd_to_sere(bdd_restrict(f1, label)); formula dest2 = formula::binop(o, dest, node[1]); bdd udest = @@ -1787,16 +1780,15 @@ namespace spot var_set = bdd_existcomp(bdd_support(t.symbolic), d_.var_set); all_props = bdd_existcomp(t.symbolic, d_.var_set); } - for (bdd one_prop_set: minterms_of(all_props, var_set)) + for (bdd label: minterms_of(all_props, var_set)) { - minato_isop isop(t.symbolic & one_prop_set); + minato_isop isop(t.symbolic & label); bdd cube; while ((cube = isop.next()) != bddfalse) { bdd label = bdd_exist(cube, d_.next_set); bdd dest_bdd = bdd_existcomp(cube, d_.next_set); - formula dest = - d_.conj_bdd_to_formula(dest_bdd); + formula dest = d_.conj_bdd_to_formula(dest_bdd); // Handle a Miyano-Hayashi style unrolling for // rational operators. Marked nodes correspond to @@ -1818,8 +1810,7 @@ namespace spot dest = d_.mt.mark_concat_ops(dest); } // Note that simplify_mark may have changed dest. - dest_bdd = bdd_ithvar(d_.register_next_variable(dest)); - res |= label & dest_bdd; + res |= label & bdd_ithvar(d_.register_next_variable(dest)); } } t.symbolic = res; @@ -2120,16 +2111,15 @@ namespace spot // // FIXME: minato_isop is quite expensive, and I (=adl) // don't think we really care that much about getting the - // smalled sum of products that minato_isop strives to + // smallest sum of products that minato_isop strives to // compute. Given that Next and Acc variables should // always be positive, maybe there is a faster way to // compute the successors? E.g. using bdd_satone() and // ignoring negated Next and Acc variables. - minato_isop isop(res & one_prop_set); + minato_isop isop(bdd_restrict(res, one_prop_set)); bdd cube; while ((cube = isop.next()) != bddfalse) { - bdd label = bdd_exist(cube, d.next_set); bdd dest_bdd = bdd_existcomp(cube, d.next_set); formula dest = d.conj_bdd_to_formula(dest_bdd); @@ -2147,8 +2137,9 @@ namespace spot if (symb_merge) dest = fc.canonicalize(dest); - bdd conds = bdd_existcomp(label, d.var_set); - bdd promises = bdd_existcomp(label, d.a_set); + bdd conds = + exprop ? one_prop_set : bdd_existcomp(cube, d.var_set); + bdd promises = bdd_existcomp(cube, d.a_set); dests.emplace_back(transition(dest, conds, promises)); } } diff --git a/spot/twaalgos/synthesis.cc b/spot/twaalgos/synthesis.cc index e1e4e1780..88e22ff04 100644 --- a/spot/twaalgos/synthesis.cc +++ b/spot/twaalgos/synthesis.cc @@ -574,9 +574,7 @@ namespace spot // implies is faster than and if (bdd_implies(one_letter, e_info.einsup.first)) { - e_info.econdout = - bdd_appex(e_info.econd, one_letter, - bddop_and, input_bdd); + e_info.econdout = bdd_restrict(e_info.econd, one_letter); dests.push_back(&e_info); assert(e_info.econdout != bddfalse); } diff --git a/tests/core/bdd.test b/tests/core/bdd.test index ba2e11232..db03dbad5 100755 --- a/tests/core/bdd.test +++ b/tests/core/bdd.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2018, 2020 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2017, 2018, 2020, 2022 Laboratoire de Recherche et +# Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -23,7 +23,7 @@ set -e # Make sure that setting the SPOT_BDD_TRACE envvar actually does # something. -genltl --kr-nlogn=2 | +genltl --kr-n=3 | SPOT_BDD_TRACE=1 ltl2tgba -x tls-max-states=0 -D >out 2>err cat err grep spot: out && exit 1 @@ -31,14 +31,14 @@ 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 11 = `grep -c 'spot: BDD GC' err` +test 2 = `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` +test "2240,4214" = `autfilt --stats=%s,%e out` # With the default value of tls-max-states, no GC is needed -genltl --kr-nlogn=2 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err +genltl --kr-n=3 | SPOT_BDD_TRACE=1 ltl2tgba -D --stats=%s,%e >out 2>err cat err grep 'spot: BDD package initialized' err test 0 = `grep -c 'spot: BDD GC' err` -test "147,207" = `cat out` +test "2240,4214" = `cat out` diff --git a/tests/core/ltlf.test b/tests/core/ltlf.test index a1979bc8d..11f2132ac 100755 --- a/tests/core/ltlf.test +++ b/tests/core/ltlf.test @@ -57,7 +57,7 @@ State: 3 HOA: v1 name: "a & X(A & a) & (A U G!A)" States: 4 -Start: 2 +Start: 3 AP: 2 "A" "a" acc-name: Buchi Acceptance: 1 Inf(0) @@ -70,9 +70,9 @@ State: 1 [!0] 0 [0] 1 State: 2 -[0&1] 3 -State: 3 [0&1] 1 +State: 3 +[0&1] 2 --END-- HOA: v1 name: "(a U (A & b)) & (A U G!A) & F((A & c) | (A & d & X!A))" @@ -124,7 +124,7 @@ State: 2 {0} --END-- HOA: v1 States: 3 -Start: 1 +Start: 2 AP: 1 "a" acc-name: Buchi Acceptance: 1 Inf(0) @@ -133,9 +133,9 @@ properties: trans-labels explicit-labels state-acc deterministic State: 0 {0} [t] 0 State: 1 -[0] 2 -State: 2 [0] 0 +State: 2 +[0] 1 --END-- HOA: v1 States: 5