From b3b22388c917880703010868732ddda516230988 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 13 Sep 2022 13:53:59 +0200 Subject: [PATCH] postproc: introduce -x merge-states-min * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Introduce a merge-states-min option. * bin/spot-x.cc: Document it. * spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Add option to generate cyclist test cases. * NEWS: Document the above. * tests/core/included.test: Add test cases that used to be too slow. --- NEWS | 11 ++++++++++ bin/genaut.cc | 7 +++++- bin/spot-x.cc | 6 +++++- spot/gen/automata.cc | 45 +++++++++++++++++++++++++++++++++++++-- spot/gen/automata.hh | 20 ++++++++++++++++- spot/twaalgos/postproc.cc | 4 ++++ spot/twaalgos/postproc.hh | 3 ++- tests/core/included.test | 11 ++++++++-- 8 files changed, 99 insertions(+), 8 deletions(-) diff --git a/NEWS b/NEWS index 38beaa062..93708c0d0 100644 --- a/NEWS +++ b/NEWS @@ -36,6 +36,11 @@ New in spot 2.10.6.dev (not yet released) - ltlsynt has a new option --from-pgame that takes a parity game in extended HOA format, as used in the Synthesis Competition. + - genaut learned the --cyclist-trace-nba and --cyclist-proof-dba + options. Those are used to generate pairs of automata that should + include each other, and are used to show a regression (in speed) + present in Spot 2.10.x and fixed in 2.11. + Library: - The new function suffix_operator_normal_form() implements @@ -121,6 +126,12 @@ New in spot 2.10.6.dev (not yet released) is a co-Büchi automaton. And product_or() learned that the "or"-product of two Büchi automata is a Büchi automaton. + - spot::postprocessor has a new extra option merge-states-min that + indicate above how many states twa_graph::merge_states(), which + perform a very cheap pass to fuse states with identicall + succesors, should be called before running simulation-based + reductions. + - spot::parallel_policy is an object that can be passed to some algorithm to specify how many threads can be used if Spot has been compiled with --enable-pthread. Currently, only diff --git a/bin/genaut.cc b/bin/genaut.cc index eb2163cab..d7db04d98 100644 --- a/bin/genaut.cc +++ b/bin/genaut.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019, 2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -62,6 +62,11 @@ static const argp_option options[] = { "m-nba", gen::AUT_M_NBA, "RANGE", 0, "An NBA with N+1 states whose determinization needs at least " "N! states", 0}, + { "cyclist-trace-nba", gen::AUT_CYCLIST_TRACE_NBA, "RANGE", 0, + "An NBA with N+2 states that should include cyclist-proof-dba=B.", 0}, + { "cyclist-proof-dba", gen::AUT_CYCLIST_PROOF_DBA, "RANGE", 0, + "A DBA with N+2 states that should be included " + "in cyclist-trace-nba=B.", 0}, RANGE_DOC, /**************************************************/ { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 }, diff --git a/bin/spot-x.cc b/bin/spot-x.cc index c4905c2e9..a653fc926 100644 --- a/bin/spot-x.cc +++ b/bin/spot-x.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2013-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -164,6 +164,10 @@ 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 the value of parameter \"simul\" in --high mode, and 0 \ therwise.") }, + { DOC("merge-states-min", "Number of states above which states are \ +merged using a cheap approximation of a bisimulation quotient before \ +attempting simulation-based reductions. Defaults to 128. Set to 0 to \ +never merge states.") }, { DOC("simul-max", "Number of states above which simulation-based \ reductions are skipped. Defaults to 4096. Set to 0 to disable. This \ applies to all simulation-based optimization, including thoses of the \ diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc index 165ab8c98..73c057a00 100644 --- a/spot/gen/automata.cc +++ b/spot/gen/automata.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2019, 2021 Laboratoire de Recherche et +// Copyright (C) 2017-2019, 2021-2022 Laboratoire de Recherche et // Developpement de l'EPITA (LRDE). // // This file is part of Spot, a model checking library. @@ -220,13 +220,48 @@ namespace spot return aut; } + static twa_graph_ptr + cyclist_trace_or_proof(unsigned n, bool trace, bdd_dict_ptr dict) + { + auto aut = make_twa_graph(dict); + acc_cond::mark_t m = aut->set_buchi(); + aut->new_states(n + 2); + aut->set_init_state(0); + if (trace) + m = {}; + aut->prop_state_acc(true); + + // How many AP to we need to represent n letters + unsigned nap = ulog2(n + 1); + std::vector apvars(nap); + for (unsigned a = 0; a < nap; ++a) + apvars[a] = aut->register_ap("p" + std::to_string(a)); + + if (trace) + aut->new_edge(0, 0, bddtrue); // the only non-deterministic edge + else + aut->prop_universal(true); + + bdd zero = bdd_ibuildcube(0, nap, apvars.data()); + aut->new_edge(0, 1, zero, m); + for (unsigned letter = 1; letter <= n; ++letter) + { + bdd cond = bdd_ibuildcube(letter, nap, apvars.data()); + aut->new_acc_edge(1, letter + 1, cond); + aut->new_edge(letter + 1, 1, zero, m); + } + + return aut; + } + + twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict) { if (n < 0) { std::ostringstream err; err << "pattern argument for " << aut_pattern_name(pattern) - << " should be positive"; + << " should be non-negative"; throw std::runtime_error(err.str()); } @@ -241,6 +276,10 @@ namespace spot return l_dsa(n, dict); case AUT_M_NBA: return m_nba(n, dict); + case AUT_CYCLIST_TRACE_NBA: + return cyclist_trace_or_proof(n, true, dict); + case AUT_CYCLIST_PROOF_DBA: + return cyclist_trace_or_proof(n, false, dict); case AUT_END: break; } @@ -255,6 +294,8 @@ namespace spot "l-nba", "l-dsa", "m-nba", + "cyclist-trace-nba", + "cyclist-proof-dba", }; // Make sure we do not forget to update the above table every // time a new pattern is added. diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh index d0c43d5f5..a54f75ac1 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2019 Laboratoire de Recherche et Developpement de +// Copyright (C) 2017, 2019, 2022 Laboratoire de Recherche et Developpement de // l'EPITA (LRDE). // // This file is part of Spot, a model checking library. @@ -79,6 +79,24 @@ namespace spot /// propositions to encode the $n+1$ letters used in the /// original alphabet. AUT_M_NBA, + /// \brief An NBA with (n+2) states derived from a Cyclic test + /// case. + /// + /// This familly of automata is derived from a couple of + /// examples supplied by Reuben Rowe. The task is to + /// check that the automaton generated with AUT_CYCLIST_TRACE_NBA + /// for a given n contain the automaton generated with + /// AUT_CYCLIST_PROOF_DBA for the same n. + AUT_CYCLIST_TRACE_NBA, + /// \brief A DBA with (n+2) states derived from a Cyclic test + /// case. + /// + /// This familly of automata is derived from a couple of + /// examples supplied by Reuben Rowe. The task is to + /// check that the automaton generated with AUT_CYCLIST_TRACE_NBA + /// for a given n contain the automaton generated with + /// AUT_CYCLIST_PROOF_DBA for the same n. + AUT_CYCLIST_PROOF_DBA, AUT_END }; diff --git a/spot/twaalgos/postproc.cc b/spot/twaalgos/postproc.cc index 39a6c0926..55feeb295 100644 --- a/spot/twaalgos/postproc.cc +++ b/spot/twaalgos/postproc.cc @@ -89,6 +89,7 @@ namespace spot wdba_minimize_ = opt->get("wdba-minimize", -1); gen_reduce_parity_ = opt->get("gen-reduce-parity", 1); simul_max_ = opt->get("simul-max", 4096); + merge_states_min_ = opt->get("merge-states-min", 128); wdba_det_max_ = opt->get("wdba-det-max", 4096); simul_trans_pruning_ = opt->get("simul-trans-pruning", 512); @@ -118,6 +119,9 @@ namespace spot { if (opt == 0) return a; + if (merge_states_min_ > 0 + && static_cast(merge_states_min_) < a->num_states()) + a->merge_states(); if (simul_max_ > 0 && static_cast(simul_max_) < a->num_states()) return a; diff --git a/spot/twaalgos/postproc.hh b/spot/twaalgos/postproc.hh index 080cb831f..96128c531 100644 --- a/spot/twaalgos/postproc.hh +++ b/spot/twaalgos/postproc.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2021 Laboratoire de Recherche et Développement +// Copyright (C) 2012-2022 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -268,6 +268,7 @@ namespace spot bool state_based_ = false; int wdba_minimize_ = -1; int simul_max_ = 4096; + int merge_states_min_ = 128; int wdba_det_max_ = 4096; }; /// @} diff --git a/tests/core/included.test b/tests/core/included.test index 9f39fef20..3574af9e3 100755 --- a/tests/core/included.test +++ b/tests/core/included.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement +# Copyright (C) 2016, 2022 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -60,5 +60,12 @@ ltl2tgba true | autfilt out.hoa --equivalent-to - ltl2tgba '!(a U c)' | autfilt --product-or a1.hoa > out.hoa ltl2tgba true | autfilt out.hoa --equivalent-to - && exit 1 -: +# In Spot 2.10, the following was very slow. +for n in 1 2 4 8 16 512 1024 2048 4096 8192; do + genaut --cyclist-trace-nba=$n > trace.hoa + genaut --cyclist-proof-dba=$n > proof.hoa + autfilt -q --included-in=trace.hoa proof.hoa || exit 1 + autfilt -q --included-in=proof.hoa trace.hoa && exit 1 +done +: