genaut: introduce --m-nba

* bin/genaut.cc: Implement the --m-nba option.
* spot/gen/automata.hh, spot/gen/automata.cc: Add the generation code.
* NEWS, bin/man/genaut.x: Document it.
* doc/org/genaut.org: Update.
* tests/core/genaut.test, tests/core/parity2.test: Add some tests.

NEWS

@@ -21,6 +21,9 @@ New in spot 2.7.5.dev (not yet released)
     consistency-checks (they are unnecessary when all automata
     could be complemented and statistics were not required).
 
+  - genaut learned --m-nba=N to generate Max Michel's NBA familly.
+    (NBAs with N+1 states whose determinized have at least N! states.)
+
   Library:
 
   - Add generic_accepting_run() as a variant of generic_emptiness_check() that

bin/genaut.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -59,6 +59,9 @@ static const argp_option options[] =
     { "l-dsa", gen::AUT_L_DSA, "RANGE", 0,
       "A deterministic Streett automaton with 4N states with no "
       "equivalent deterministic Rabin automaton of less than N! states.", 0},
+    { "m-nba", gen::AUT_M_NBA, "RANGE", 0,
+      "An NBA with N+1 states whose determinization needs at least "
+      "N! states", 0},
     RANGE_DOC,
   /**************************************************/
     { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },

bin/man/genaut.x

@@ -12,6 +12,10 @@ Automata.  Proceedings of ICALP'15.
 l
 C. Löding: Optimal Bounds for Transformations of ω-Automata.
 Proceedings of FSTTCS'99.
+.TP
+m
+M. Michel: Complementation is more difficult with automata on
+infinite words.  CNET, Paris (1988).  Unpublished manuscript.
 
 [SEE ALSO]
 .BR autfilt (1),

doc/org/genaut.org

@@ -15,15 +15,19 @@ genaut --help | sed -n '/Pattern selection:/,/^$/p' | sed '1d;$d'
 #+END_SRC
 
 #+RESULTS:
-:       --ks-nca=RANGE         A co-Büchi automaton with 2N+1 states for which
-:                              any equivalent deterministic co-Büchi automaton
-:                              has at least 2^N/(2N+1) states.
-:       --l-dsa=RANGE          A deterministic Streett automaton with 4N states
-:                              with no equivalent deterministic Rabin automaton
-:                              of less than N! states.
-:       --l-nba=RANGE          A Büchi automaton with 3N+1 states whose
-:                              complementary Streett automaton needs at least N!
-:                              states.
+#+begin_example
+      --ks-nca=RANGE         A co-Büchi automaton with 2N+1 states for which
+                             any equivalent deterministic co-Büchi automaton
+                             has at least 2^N/(2N+1) states.
+      --l-dsa=RANGE          A deterministic Streett automaton with 4N states
+                             with no equivalent deterministic Rabin automaton
+                             of less than N! states.
+      --l-nba=RANGE          A Büchi automaton with 3N+1 states whose
+                             complementary Streett automaton needs at least N!
+                             states.
+      --m-nba=RANGE          An NBA with N+1 states whose determinization needs
+                             at least N! states
+#+end_example
 
 
 By default, the output format is [[file:hoa.org][HOA]], but this can be controlled using

spot/gen/automata.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2018 Laboratoire de Recherche et Developpement
+// Copyright (C) 2017-2019 Laboratoire de Recherche et Developpement
 // de l'EPITA (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -32,7 +32,7 @@ namespace spot
       ks_nca(unsigned n, bdd_dict_ptr dict)
       {
         if (n == 0)
-          throw std::runtime_error("ks_nca expects a positive argument");
+          throw std::runtime_error("ks-nca expects a positive argument");
         // the alphabet has four letters:
         // i, s (for sigma), p (for pi), h (for hash)
         // we encode this four letters alphabet thanks to two AP a and b
@@ -99,7 +99,7 @@ namespace spot
       l_nba(unsigned n, bdd_dict_ptr dict)
       {
         if (n == 0)
-          throw std::runtime_error("l_nba expects a positive argument");
+          throw std::runtime_error("l-nba expects a positive argument");
 
         auto aut = make_twa_graph(dict);
 
@@ -138,7 +138,7 @@ namespace spot
       l_dsa(unsigned n, bdd_dict_ptr dict)
       {
         if (n < 1 || n > 16)
-          throw std::runtime_error("l_dsa expects 1 <= n <= 16");
+          throw std::runtime_error("l-dsa expects 1 <= n <= 16");
 
         auto aut = make_twa_graph(dict);
 
@@ -173,6 +173,62 @@ namespace spot
       }
     }
 
+    static unsigned ulog2(unsigned n)
+    {
+      assert(n>0);
+      --n;
+#ifdef __GNUC__
+      return 8*sizeof(unsigned) - __builtin_clz(n);
+#else
+      unsigned res = 0;
+      while (n)
+        {
+          ++res;
+          n >>= 1;
+        }
+      return res;
+#endif
+    }
+
+    static twa_graph_ptr
+    m_nba(unsigned n, bdd_dict_ptr dict)
+    {
+      if (n == 0)
+        throw std::runtime_error
+          ("l-nba expects a positive argument");
+
+      auto aut = make_twa_graph(dict);
+      aut->set_buchi();
+      aut->new_states(n + 1);
+      aut->set_init_state(0);
+
+      // How many AP to we need to represent n+1 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));
+
+      bdd all = bdd_ibuildcube(0, nap, apvars.data());
+      for (unsigned letter = n; letter > 0; --letter)
+        {
+          bdd cond = bdd_ibuildcube(letter, nap, apvars.data());
+          aut->new_acc_edge(0, letter, cond);
+          aut->new_edge(letter, 0, cond);
+          all |= cond;
+        }
+      for (unsigned letter = n; letter > 0; --letter)
+        aut->new_edge(letter, letter, all);
+
+      aut->prop_state_acc(true);
+      aut->prop_universal(false);
+      aut->prop_complete(false);
+      aut->prop_inherently_weak(false);
+      aut->prop_stutter_invariant(false);
+      aut->prop_semi_deterministic(false);
+
+      return aut;
+    }
+
     twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict)
     {
       if (n < 0)
@@ -192,6 +248,8 @@ namespace spot
           return l_nba(n, dict);
         case AUT_L_DSA:
           return l_dsa(n, dict);
+        case AUT_M_NBA:
+          return m_nba(n, dict);
         case AUT_END:
           break;
         }
@@ -205,6 +263,7 @@ namespace spot
           "ks-nca",
           "l-nba",
           "l-dsa",
+          "m-nba",
         };
       // 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 Laboratoire de Recherche et Developpement de
+// Copyright (C) 2017, 2019 Laboratoire de Recherche et Developpement de
 // l'EPITA (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -109,6 +109,29 @@ namespace spot
           }
           \endverbatim */
       AUT_L_DSA,
+      /// \brief An NBA with (n+1) states whose complement needs ≥n! states
+      ///
+      /// This automaton is usually attributed to Max Michel (1988),
+      /// who described it in some unpublished documents.  Other
+      /// descriptions of this automaton can be found in a number
+      /// of papers, like:
+      /** \verbatim
+          @InBook{thomas.97.chapter,
+            author      = {Wolfgang Thomas},
+            title       = {Languages, Automata, and Logic},
+            booktitle   = {Handbook of Formal Languages ---
+                           Volume 3 Beyond Words},
+            editor      = {Grzegorz Rozenberg and Arto Salomaa},
+            chapter     = 7,
+            publisher   = {Springer-Verlag},
+            year        = {1997}
+          }
+          \endverbatim */
+      ///
+      /// Our implementation uses $\lceil \log_2(n+1)\rceil$ atomic
+      /// propositions to encode the $n+1$ letters used in the
+      /// original alphabet.
+      AUT_M_NBA,
       AUT_END
     };
 

tests/core/genaut.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
+# Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement
 # de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -29,7 +29,8 @@ s/[=[].*/=1/p
 res=`genaut $opts --stats="--%F=%L"`
 test "$opts" = "$res"
 
-genaut --ks-nca=..3 --l-nba=..3 --l-dsa=..3 --stats=%s,%e,%t,%c,%g >out
+genaut --ks-nca=..3 --l-nba=..3 --l-dsa=..3 --m-nba=..3 \
+       --stats=%s,%e,%t,%c,%g >out
 cat >expected <<EOF
 3,7,16,1,Fin(0)
 5,14,32,1,Fin(0)
@@ -40,6 +41,9 @@ cat >expected <<EOF
 4,6,6,1,Fin(0) | Inf(1)
 8,12,12,1,(Fin(0) | Inf(1)) & (Fin(2) | Inf(3))
 12,18,18,1,(Fin(0) | Inf(1)) & (Fin(2) | Inf(3)) & (Fin(4) | Inf(5))
+2,3,4,1,Inf(0)
+3,6,10,1,Inf(0)
+4,9,18,1,Inf(0)
 EOF
 diff out expected
 

tests/core/parity2.test

@@ -1,6 +1,6 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2018 Laboratoire de Recherche et Développement de
+# Copyright (C) 2018, 2019 Laboratoire de Recherche et Développement de
 # l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -1526,3 +1526,17 @@ diff expected4 res4
 ltlcross 'ltl2tgba -P' 'ltl2tgba -P"odd max"' 'ltl2tgba -P"even min"' \
          'ltl2tgba -p' 'ltl2tgba -p"odd max"' 'ltl2tgba -p"even min"' \
          -f FGa -f 'GFa&GFb' -f 'GF(a <-> XXXb)' -f '(p0 W XXGp0) & GFp1 & FGp2'
+
+
+# Test the behavior of our determinization on Max Michel automata.
+# Any change to Spot that lowers the output.states is welcome :-)
+genaut --m-nba=1..4 | autcross --language-preserved 'autfilt -D' --csv=out.csv
+cut -d, -f4,17 out.csv > sizes.csv
+cat >expected <<EOF
+"input.states","output.states"
+2,3
+3,15
+4,129
+5,2057
+EOF
+diff sizes.csv expected