From 469d8067e03b96b5188a09a76c5839185ae765e7 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 28 Apr 2017 12:02:54 +0200
Subject: [PATCH] gen: another automaton family

* spot/gen/automata.hh, spot/gen/automata.cc,
bin/genaut.cc: Introduce L_DSA.
* tests/core/genaut.test: Add quick test.
---
 NEWS                   |  1 -
 bin/genaut.cc          |  3 +++
 spot/gen/automata.cc   | 41 +++++++++++++++++++++++++++++++++++++++++
 spot/gen/automata.hh   | 28 ++++++++++++++++++++++++++++
 tests/core/genaut.test |  5 ++++-
 5 files changed, 76 insertions(+), 2 deletions(-)

diff --git a/NEWS b/NEWS
index f40b14548..b069c2153 100644
--- a/NEWS
+++ b/NEWS
@@ -13,7 +13,6 @@ New in spot 2.3.3.dev (not yet released)
 
   - genaut is a binary to produce families of automata defined in the
     literature (in the same way as we have genltl for LTL formulas).
-    It currently features only two classes of automata.
 
   Library:
 
diff --git a/bin/genaut.cc b/bin/genaut.cc
index 9eff69223..d19b26abe 100644
--- a/bin/genaut.cc
+++ b/bin/genaut.cc
@@ -56,6 +56,9 @@ static const argp_option options[] =
     { "l-nba", gen::AUT_L_NBA, "RANGE", 0,
       "A Büchi automaton with 3N+1 states whose complementary Streett "
       "automaton needs at least n! states.", 0},
+    { "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},
     RANGE_DOC,
   /**************************************************/
     { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
diff --git a/spot/gen/automata.cc b/spot/gen/automata.cc
index ceca18e15..8818090e0 100644
--- a/spot/gen/automata.cc
+++ b/spot/gen/automata.cc
@@ -132,6 +132,44 @@ namespace spot
         aut->prop_semi_deterministic(false);
         return aut;
       }
+
+      static twa_graph_ptr
+      l_dsa(unsigned n, bdd_dict_ptr dict)
+      {
+        if (n < 1 || n > 16)
+          throw std::runtime_error("l_dsa expects 1 <= n <= 16");
+
+        auto aut = make_twa_graph(dict);
+
+        bdd a = bdd_ithvar(aut->register_ap("a"));
+        bdd b = !a;
+
+        aut->set_acceptance(2 * n, acc_cond::acc_code::streett(n));
+        aut->new_states(4 * n);
+        aut->set_init_state(0);
+
+        for (unsigned s = 0; s < n; ++s)
+          {
+            unsigned col1 = 4 * s;
+            unsigned col2 = 4 * s + 1;
+            unsigned col3 = 4 * s + 2;
+            unsigned col4 = 4 * s + 3;
+            aut->new_edge(col1, 2, a, {2 * s});
+            aut->new_edge(col2, col1, b);
+            aut->new_edge(col2, std::min(col2 + 4, 4 * n - 3), a);
+            aut->new_edge(col3, col4, b);
+            aut->new_edge(col3, std::min(col3 + 4, 4 * n - 2), a);
+            aut->new_edge(col4, 1, a, {2 * s + 1});
+          }
+
+        aut->prop_state_acc(true);
+        aut->prop_universal(true);
+        aut->prop_complete(false);
+        aut->prop_inherently_weak(false);
+        aut->prop_stutter_invariant(false);
+        aut->prop_semi_deterministic(true);
+        return aut;
+      }
     }
 
     twa_graph_ptr aut_pattern(aut_pattern_id pattern, int n, bdd_dict_ptr dict)
@@ -151,6 +189,8 @@ namespace spot
           return ks_cobuchi(n, dict);
         case AUT_L_NBA:
           return l_nba(n, dict);
+        case AUT_L_DSA:
+          return l_dsa(n, dict);
         case AUT_END:
           break;
         }
@@ -163,6 +203,7 @@ namespace spot
         {
           "ks-cobuchi",
           "l-nba",
+          "l-dsa",
         };
       // 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 d1f96f421..fc7018f85 100644
--- a/spot/gen/automata.hh
+++ b/spot/gen/automata.hh
@@ -81,6 +81,34 @@ namespace spot
           }
           \endverbatim */
       AUT_L_NBA,
+      /// \brief DSA hard to convert to DRA.
+      ///
+      /// Build a deterministic Streett automaton 4n states, and n
+      /// acceptance pairs, such that an equivalent deterministic Rabin
+      /// automaton would require at least n! states.
+      ///
+      /// Only defined for 1<n<=16 because Spot does not support more
+      /// than 32 acceptance pairs.
+      ///
+      /// This automaton corresponds to the right part of Fig.2 in the
+      /// following paper.
+      /** \verbatim
+          @InProceedings{loding.99.fstts,
+            author	= {Christof L{\"o}ding},
+            title	= {Optimal Bounds for Transformations of
+                           $\omega$-Automata},
+            booktitle	= {Proceedings of the 19th Conference on Foundations of
+                           Software Technology and Theoretical Computer Science
+                           (FSTTCS'99)},
+            year        = 1999,
+            publisher	= {Springer},
+            pages       = {97--109},
+            series	= {Lecture Notes in Computer Science},
+            volume	= 1738,
+            doi		= {10.1007/3-540-46691-6_8}
+          }
+          \endverbatim */
+      AUT_L_DSA,
       AUT_END
     };
 
diff --git a/tests/core/genaut.test b/tests/core/genaut.test
index 22d51b078..35027d85a 100644
--- a/tests/core/genaut.test
+++ b/tests/core/genaut.test
@@ -29,7 +29,7 @@ s/[=[].*/=1/p
 res=`genaut $opts --stats="--%F=%L"`
 test "$opts" = "$res"
 
-genaut --ks-cobuchi=..3 --l-nba=..3 --stats=%s,%e,%t,%c,%g >out
+genaut --ks-cobuchi=..3 --l-nba=..3 --l-dsa=..3 --stats=%s,%e,%t,%c,%g >out
 cat >expected <<EOF
 3,7,16,1,Fin(0)
 5,14,32,1,Fin(0)
@@ -37,6 +37,9 @@ cat >expected <<EOF
 4,7,9,1,Inf(0)
 7,12,16,1,Inf(0)
 10,17,23,1,Inf(0)
+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))
 EOF
 diff out expected