genaut: add two families of cyclic automata

These are meant to test the optimization implemented in issue #568.

* spot/gen/automata.hh, spot/gen/automata.cc, bin/genaut.cc: Add
support for --cycle-log-nba and --cycle-onehot-nba.
* tests/core/genaut.test: Add some tests.
* tests/python/gen.ipynb: Illustrate them.
* NEWS: Mention them.

NEWS

@@ -55,6 +55,11 @@ New in spot 2.11.6.dev  (not yet released)
     patching the game a posteriori is cumbersome if the equivalence
     concerns different players).
 
+  - genaut learned two new familes of automata, --cycle-log-nba and
+    --cycle-onehot-nba.  They both create a cycle of n^2 states that
+    can be reduced to a cycle of n states using reduction based on
+    direct simulation.
+
   Library:
 
   - The following new trivial simplifications have been implemented for SEREs:

bin/genaut.cc

@@ -67,6 +67,12 @@ static const argp_option options[] =
     { "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},
+    { "cycle-log-nba", gen::AUT_CYCLE_LOG_NBA, "RANGE", 0,
+      "A cyclic NBA with N*N states and log(N) atomic propositions, that "
+      "should be simplifiable to a cyclic NBA with N states.", 0 },
+    { "cycle-onehot-nba", gen::AUT_CYCLE_ONEHOT_NBA, "RANGE", 0,
+      "A cyclic NBA with N*N states and N atomic propositions, that "
+      "should be simplifiable to a cyclic NBA with N states.", 0 },
     RANGE_DOC,
   /**************************************************/
     { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },

spot/gen/automata.cc

@@ -172,9 +172,10 @@ namespace spot
       }
     }
 
+    // Return the smallest integer k such that 2^k ≥ n > 1.
     static unsigned ulog2(unsigned n)
     {
-      assert(n>0);
+      assert(n>1); // clz() is undefined for n==0
       --n;
       return CHAR_BIT*sizeof(unsigned) - clz(n);
     }
@@ -229,7 +230,7 @@ namespace spot
           m = {};
       aut->prop_state_acc(true);
 
-      // How many AP to we need to represent n letters
+      // 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)
@@ -252,6 +253,76 @@ namespace spot
       return aut;
     }
 
+    static twa_graph_ptr
+    cycle_nba(unsigned n, bool onehot, bdd_dict_ptr dict)
+    {
+      if (n == 0)
+        throw std::runtime_error
+          (onehot
+           ? "cycle-onehot-nba expects a positive argument"
+           : "cycle-log-nba expects a positive argument");
+
+      auto aut = make_twa_graph(dict);
+      acc_cond::mark_t isacc = aut->set_buchi();
+      aut->new_states(n * n);
+      aut->set_init_state(0);
+      aut->prop_state_acc(true);
+      aut->prop_weak(n == 1);
+      aut->prop_universal(n == 1);
+      aut->prop_complete(false);
+
+      std::vector<bdd> letters;
+      letters.reserve(n);
+
+      if (!onehot)
+        {
+          // How many AP to we need to represent n letters
+          unsigned nap = n == 1 ? 1 : ulog2(n);
+          std::vector<int> apvars(nap);
+          for (unsigned a = 0; a < nap; ++a)
+            apvars[a] = aut->register_ap("p" + std::to_string(a));
+
+          for (unsigned letter = 0; letter < n; ++letter)
+            {
+              bdd cond = bdd_ibuildcube(letter, nap, apvars.data());
+              letters.push_back(cond);
+            }
+        }
+      else
+        {
+          std::vector<bdd> apvars(n);
+          bdd allneg = bddtrue;
+          for (unsigned a = 0; a < n; ++a)
+            {
+              int v = aut->register_ap("p" + std::to_string(a));
+              apvars[a] = bdd_ithvar(v);
+              allneg &= bdd_nithvar(v);
+            }
+          for (unsigned a = 0; a < n; ++a)
+            letters.push_back(bdd_exist(allneg, apvars[a]) & apvars[a]);
+        }
+
+      unsigned n2 = n * n;
+      for (unsigned s = 0; s < n; ++s)
+        {
+          bdd label = letters[s];
+          for (unsigned copy = 0; copy < n; ++copy)
+            {
+              unsigned q = s + copy * n;
+              if (s != 0)
+                {
+                  aut->new_edge(q, q, bddtrue);
+                  aut->new_edge(q, (q + 1) % n2, label);
+                }
+              else
+                {
+                  aut->new_edge(q, (q + 1) % n2, label, isacc);
+                }
+            }
+        }
+      return aut;
+    }
+
 
     twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict)
     {
@@ -278,6 +349,10 @@ namespace spot
           return cyclist_trace_or_proof(n, true, dict);
         case AUT_CYCLIST_PROOF_DBA:
           return cyclist_trace_or_proof(n, false, dict);
+        case AUT_CYCLE_LOG_NBA:
+          return cycle_nba(n, false, dict);
+        case AUT_CYCLE_ONEHOT_NBA:
+          return cycle_nba(n, true, dict);
         case AUT_END:
           break;
         }
@@ -294,6 +369,8 @@ namespace spot
           "m-nba",
           "cyclist-trace-nba",
           "cyclist-proof-dba",
+          "cycle-log-nba",
+          "cycle-onehot-nba",
         };
       // Make sure we do not forget to update the above table every
       // time a new pattern is added.

spot/gen/automata.hh

@@ -96,6 +96,27 @@ namespace spot
       /// for a given n contain the automaton generated with
       /// AUT_CYCLIST_PROOF_DBA for the same n.
       AUT_CYCLIST_PROOF_DBA,
+      /// \brief cycles of n letters repeated n times
+      ///
+      /// This is a Büchi automaton with n^2 states, in which each
+      /// state i has a true self-loop and a successor labeled by the
+      /// (i%n)th letter.  Only the states that are multiple of n have
+      /// no self-loop and are accepting.
+      ///
+      /// This version uses log(n) atomic propositions to
+      /// encore the n letters as minterms.
+      AUT_CYCLE_LOG_NBA,
+      /// \brief cycles of n letters repeated n times
+      ///
+      /// This is a Büchi automaton with n^2 states, in which each
+      /// state i has a true self-loop and a successor labeled by the
+      /// (i%n)th letter.  Only the states that are multiple of n have
+      /// no self-loop and are accepting.
+      ///
+      /// This version uses one-hot encoding of letters, i.e, n atomic
+      /// propositions are used, but only one is positive (except on
+      /// true self-loops).
+      AUT_CYCLE_ONEHOT_NBA,
       AUT_END
     };
 

tests/core/genaut.test

@@ -29,6 +29,7 @@ res=`genaut $opts --stats="--%F=%L"`
 test "$opts" = "$res"
 
 genaut --ks-nca=..3 --l-nba=..3 --l-dsa=..3 --m-nba=..3 \
+       --cycle-log-nba=..3 --cycle-onehot-nba=..3 \
        --stats=%s,%e,%t,%c,%g >out
 cat >expected <<EOF
 3,7,16,1,Fin(0)
@@ -43,6 +44,12 @@ cat >expected <<EOF
 2,3,4,1,Inf(0)
 3,6,10,1,Inf(0)
 4,9,18,1,Inf(0)
+1,1,1,1,Inf(0)
+4,6,8,1,Inf(0)
+9,15,33,1,Inf(0)
+1,1,1,1,Inf(0)
+4,6,12,1,Inf(0)
+9,15,57,1,Inf(0)
 EOF
 diff out expected