random_graph: add option to generate complete deterministic automaton

* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh:
Add option to generate a complete deterministic automaton.
* src/tgbatest/randtgba.cc: Test it.

src/tgbaalgos/randomgraph.cc

@@ -23,6 +23,7 @@
 #include "randomgraph.hh"
 #include "tgba/tgbagraph.hh"
 #include "misc/random.hh"
+#include "misc/bddlt.hh"
 #include "ltlast/atomic_prop.hh"
 #include <sstream>
 #include <list>
@@ -35,12 +36,59 @@ namespace spot
 
   namespace
   {
-    void
+    unsigned
-    random_labels(tgba_digraph_ptr aut,
+    random_deterministic_labels_rec(std::vector<bdd>& labels, int *props,
-		  unsigned src,
+				    int props_n, bdd current, unsigned n)
-		  unsigned dest,
+    {
-		  int* props, int props_n, float t,
+      if (n >  1 && props_n >= 1)
-		  unsigned n_accs, float a)
+        {
+	  bdd ap = bdd_ithvar(*props);
+          ++props;
+	  --props_n;
+
+	  // There are m labels generated from "current & ap"
+	  // and n - m labels generated from "current & !ap"
+          unsigned m = rrand(1, n - 1);
+	  if (2 * m < n)
+	    {
+	      m = n - m;
+	      ap = !ap;
+	    }
+
+	  unsigned res = random_deterministic_labels_rec(labels, props,
+							 props_n,
+							 current & ap, m);
+	  res += random_deterministic_labels_rec(labels, props, props_n,
+						 current & !ap, n - res);
+          return res;
+        }
+      else
+        {
+	  labels.push_back(current);
+          return 1;
+        }
+    }
+
+    std::vector<bdd>
+    random_deterministic_labels(int *props, int props_n, unsigned n)
+    {
+      std::vector<bdd> bddvec;
+      random_deterministic_labels_rec(bddvec, props, props_n, bddtrue, n);
+      return bddvec;
+    }
+
+    acc_cond::mark_t
+    random_acc_cond(tgba_digraph_ptr aut, unsigned n_accs, float a)
+    {
+      acc_cond::mark_t m = 0U;
+      for (unsigned i = 0U; i < n_accs; ++i)
+	if (drand() < a)
+	  m |= aut->acc().mark(i);
+      return m;
+    }
+
+    bdd
+    random_labels(int* props, int props_n, float t)
     {
       int val = 0;
       int size = 0;
@@ -62,18 +110,14 @@ namespace spot
       if (size > 0)
 	p &= bdd_ibuildcube(val, size, props);
 
-      acc_cond::mark_t m = 0U;
+      return p;
-      for (unsigned i = 0U; i < n_accs; ++i)
-	if (drand() < a)
-	  m |= aut->acc().mark(i);
-      aut->new_transition(src, dest, p, m);
     }
   }
 
   tgba_digraph_ptr
   random_graph(int n, float d,
 	       const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict,
-	       unsigned n_accs, float a, float t)
+	       unsigned n_accs, float a, float t, bool deterministic)
   {
     assert(n > 0);
     auto res = make_tgba_digraph(dict);
@@ -117,20 +161,35 @@ namespace spot
 
 	// Choose a random number of successors (at least one), using
 	// a binomial distribution.
-	int nsucc = 1 + bin.rand();
+	unsigned nsucc = 1 + bin.rand();
 
-	// Connect to NSUCC randomly chosen successors.  We want at
-	// least one unreachable successors among these if there are
-	// some.
 	bool saw_unreachable = false;
-	int possibilities = n;
+
-	while (nsucc--)
+	// Create NSUCC random labels.
+	std::vector<bdd> labels;
+	if (deterministic)
 	  {
+	    labels = random_deterministic_labels(props, props_n, nsucc);
+
+	    // if nsucc > 2^props_n, we cannot produce nsucc deterministic
+	    // transitions so we set it to labels.size()
+	    nsucc = labels.size();
+	  }
+	else
+	  for (unsigned i = 0; i < nsucc; ++i)
+	    labels.push_back(random_labels(props, props_n, t));
+
+        int possibilities = n;
+	unsigned dst;
+	for (auto& l: labels)
+	  {
+	    acc_cond::mark_t m = random_acc_cond(res, n_accs, a);
+
 	    // No connection to unreachable successors so far.  This
 	    // is our last chance, so force it now.
-	    if (nsucc == 0
+	    if (--nsucc == 0
-		&& !saw_unreachable
+		&& !unreachable_nodes.empty()
-		&& !unreachable_nodes.empty())
+		&& !saw_unreachable)
 	      {
 		// Pick a random unreachable node.
 		int index = mrand(unreachable_nodes.size());
@@ -138,32 +197,29 @@ namespace spot
 		std::advance(i, index);
 
 		// Link it from src.
-		random_labels(res, src, *i, props, props_n, t, n_accs, a);
+		res->new_transition(src, *i, l, m);
 		nodes_to_process.insert(*i);
-		unreachable_nodes.erase(i);
+		unreachable_nodes.erase(*i);
 		break;
 	      }
-	    else
-	      {
-		// Pick the index of a random node.
-		int index = mrand(possibilities--);
 
-		// Permute it with state_randomizer[possibilities], so
+            // Pick the index of a random node.
-		// we cannot pick it again.
+            int index = mrand(possibilities--);
-		auto x = state_randomizer[index];
-		state_randomizer[index] = state_randomizer[possibilities];
-		state_randomizer[possibilities] = x;
 
-		random_labels(res, src, x, props, props_n, t, n_accs, a);
+            // Permute it with state_randomizer[possibilities], so
+            // we cannot pick it again.
+            dst = state_randomizer[index];
+            state_randomizer[index] = state_randomizer[possibilities];
+            state_randomizer[possibilities] = dst;
 
-		auto j = unreachable_nodes.find(x);
+            res->new_transition(src, dst, l, m);
-		if (j != unreachable_nodes.end())
+            auto j = unreachable_nodes.find(dst);
-		  {
+            if (j != unreachable_nodes.end())
-		    nodes_to_process.insert(x);
+              {
-		    unreachable_nodes.erase(j);
+                nodes_to_process.insert(dst);
-		    saw_unreachable = true;
+                unreachable_nodes.erase(j);
-		  }
+                saw_unreachable = true;
-	      }
+              }
 	  }
 
 	// The node must have at least one successor.

src/tgbaalgos/randomgraph.hh

@@ -78,7 +78,8 @@ namespace spot
   SPOT_API tgba_digraph_ptr
   random_graph(int n, float d,
 	       const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict,
-	       unsigned n_accs = 0, float a = 0.1, float t = 0.5);
+	       unsigned n_accs = 0, float a = 0.1, float t = 0.5,
+	       bool deterministic = false);
 }
 
 #endif // SPOT_TGBAALGOS_RANDOMGRAPH_HH

src/tgbatest/randtgba.cc

@@ -122,6 +122,7 @@ syntax(char* prog)
 	    << "  -n N    number of nodes of the graph [20]" << std::endl
 	    << "  -t F    probability of the atomic propositions to be true"
 	    << " [0.5]" << std::endl
+	    << "  -det    generate a deterministic and complete graph [false]"
 	    << std::endl
 	    << "LTL Formula Generation Options:" << std::endl
 	    << "  -dp     dump priorities, do not generate any formula"
@@ -560,6 +561,7 @@ main(int argc, char** argv)
   float opt_d = 0.2;
   int opt_n = 20;
   float opt_t = 0.5;
+  bool opt_det = false;
 
   bool opt_0 = false;
   bool opt_z = false;
@@ -668,6 +670,10 @@ main(int argc, char** argv)
 	  if (!opt_ec)
 	    opt_ec = 1;
 	}
+      else if (!strcmp(argv[argn], "-det"))
+	{
+	  opt_det = true;
+	}
       else if (!strcmp(argv[argn], "-e"))
 	{
 	  if (argc < argn + 2)
@@ -908,7 +914,7 @@ main(int argc, char** argv)
 
 	      spot::tgba_digraph_ptr a =
 		spot::random_graph(opt_n, opt_d, apf, dict,
-				   opt_n_acc, opt_a, opt_t);
+				   opt_n_acc, opt_a, opt_t, opt_det);
 	      if (formula)
 		a = spot::product(formula, a);