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

@@ -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

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 },

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 \

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<int> 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.

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
     };
 

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<unsigned>(merge_states_min_) < a->num_states())
+      a->merge_states();
     if (simul_max_ > 0 && static_cast<unsigned>(simul_max_) < a->num_states())
       return a;
 

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;
   };
   /// @}

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
 
+: