* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh

(tgba_explicit::create_transition(state*, const state*)): New function.
* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh:
(random_graph): Revamp the algorithm to call rand() less often.
* src/tgbatest/randtgba.cc: Add option -0 to easy profiling.

ChangeLog

@@ -1,5 +1,11 @@
 2004-12-08  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
+	* src/tgba/tgbaexplicit.cc, src/tgba/tgbaexplicit.hh
+	(tgba_explicit::create_transition(state*, const state*)): New function.
+	* src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh:
+	(random_graph): Revamp the algorithm to call rand() less often.
+	* src/tgbatest/randtgba.cc: Add option -0 to easy profiling.
+
 	* src/misc/random.hh: Add include guard.
 
 2004-12-07  Alexandre Duret-Lutz  <adl@src.lip6.fr>

src/tgba/tgbaexplicit.cc

@@ -159,19 +159,22 @@ namespace spot
     init_ = s;
   }
 
+  tgba_explicit::transition*
+  tgba_explicit::create_transition(state* source, const state* dest)
+  {
+    transition* t = new transition;
+    t->dest = dest;
+    t->condition = bddtrue;
+    t->acceptance_conditions = bddfalse;
+    source->push_back(t);
+    return t;
+  }
 
   tgba_explicit::transition*
   tgba_explicit::create_transition(const std::string& source,
 				   const std::string& dest)
   {
-    tgba_explicit::state* s = add_state(source);
+    return create_transition(add_state(source), add_state(dest));
-    tgba_explicit::state* d = add_state(dest);
-    transition* t = new transition;
-    t->dest = d;
-    t->condition = bddtrue;
-    t->acceptance_conditions = bddfalse;
-    s->push_back(t);
-    return t;
   }
 
   void
@@ -243,7 +246,7 @@ namespace spot
 	for (t1 = i->second->begin(); t1 != i->second->end(); ++t1)
 	  {
 	    bdd acc = (*t1)->acceptance_conditions;
-	    state* dest = (*t1)->dest;
+	    const state* dest = (*t1)->dest;
 
 	    // Find another transition with the same destination and
 	    // acceptance conditions.

src/tgba/tgbaexplicit.hh

@@ -48,13 +48,15 @@ namespace spot
     {
       bdd condition;
       bdd acceptance_conditions;
-      state* dest;
+      const state* dest;
     };
 
     void set_init_state(const std::string& state);
 
     transition*
     create_transition(const std::string& source, const std::string& dest);
+    transition*
+    create_transition(state* source, const state* dest);
 
     void add_condition(transition* t, const ltl::formula* f);
     /// This assumes that all variables in \a f are known from dict.

src/tgbaalgos/randomgraph.cc

@@ -27,6 +27,8 @@
 #include <sstream>
 #include <list>
 #include <set>
+#include <iterator>
+#include "misc/hash.hh"
 
 namespace spot
 {
@@ -51,14 +53,29 @@ namespace spot
 
     void
     random_labels(tgba_explicit* aut,
-		  const std::string& src, const std::string& dest,
+		  tgba_explicit::state* src, const tgba_explicit::state* dest,
-		  const std::list<int>& props, float t,
+		  int* props, int props_n, float t,
 		  const std::list<bdd>& accs, float a)
     {
+      int val = 0;
+      int size = 0;
       bdd p = bddtrue;
-      for (std::list<int>::const_iterator i = props.begin();
+      while (props_n)
-	   i != props.end(); ++i)
+	{
-	p &= (drand() < t ? bdd_ithvar : bdd_nithvar)(*i);
+	  if (size == 8 * sizeof(int))
+	    {
+	      p &= bdd_ibuildcube(val, size, props);
+	      props += size;
+	      val = 0;
+	      size = 0;
+	    }
+	  val <<= 1;
+	  val |= (drand() < t);
+	  ++size;
+	  --props_n;
+	}
+      if (size > 0)
+	p &= bdd_ibuildcube(val, size, props);
 
       bdd ac = bddfalse;
       for (std::list<bdd>::const_iterator i = accs.begin();
@@ -80,10 +97,15 @@ namespace spot
   {
     tgba_explicit* res = new tgba_explicit(dict);
 
-    std::list<int> props;
+    int props_n = ap->size();
+    int* props = new int[props_n];
+
+    int pi = 0;
     for (ltl::atomic_prop_set::const_iterator i = ap->begin();
 	 i != ap->end(); ++i)
-      props.push_back(dict->register_proposition(*i, res));
+      props[pi++] = dict->register_proposition(*i, res);
+
+    std::vector<tgba_explicit::state*> states(n);
 
     std::list<bdd> accs;
     bdd allneg = bddtrue;
@@ -99,56 +121,82 @@ namespace spot
     for (std::list<bdd>::iterator i = accs.begin(); i != accs.end(); ++i)
       *i &= bdd_exist(allneg, *i);
 
-    typedef std::set<std::string> node_set;
+
+    // Using Sgi::hash_set instead of std::set for these sets is 3
+    // times slower (tested on a 50000 nodes example).
+    typedef std::set<tgba_explicit::state*> node_set;
     node_set nodes_to_process;
     node_set unreachable_nodes;
 
-    nodes_to_process.insert(st(0));
+    nodes_to_process.insert(states[0] = res->add_state(st(0)));
 
     for (int i = 1; i < n; ++i)
-      unreachable_nodes.insert(st(i));
+      unreachable_nodes.insert(states[i] = res->add_state(st(i)));
+
+    // We want to connect each node to a number of successors between
+    // 1 and n (with probability d).  This follow
+    barand<nrand> bin(n - 1, d);
 
     while (!nodes_to_process.empty())
       {
-	std::string src = *nodes_to_process.begin();
+	tgba_explicit::state* src = *nodes_to_process.begin();
 	nodes_to_process.erase(nodes_to_process.begin());
 
-	if (!unreachable_nodes.empty())
+	// Choose a random number of successors (at least one), using
+	// a binomial distribution.
+	int 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--)
 	  {
-	    // Pick a random unreachable node.
+	    if (nsucc == 0
-	    int index = mrand(unreachable_nodes.size());
+		&& !saw_unreachable
-	    node_set::const_iterator i;
+		&& !unreachable_nodes.empty())
-	    for (i = unreachable_nodes.begin(); index; ++i, --index)
-	      assert(i != unreachable_nodes.end());
-
-	    // Link it from src.
-	    random_labels(res, src, *i, props, t, accs, a);
-
-	    nodes_to_process.insert(*i);
-	    unreachable_nodes.erase(i);
-	  }
-	// Randomly link node to another node (including itself).
-	for (int i = 0; i < n; ++i)
-	  {
-	    if (drand() >= d)
-	      continue;
-
-	    std::string dest = st(i);
-
-	    random_labels(res, src, dest, props, t, accs, a);
-
-	    node_set::iterator j = unreachable_nodes.find(dest);
-	    if (j != unreachable_nodes.end())
 	      {
-		nodes_to_process.insert(dest);
+		// Pick a random unreachable node.
-		unreachable_nodes.erase(j);
+		int index = mrand(unreachable_nodes.size());
+		node_set::const_iterator i = unreachable_nodes.begin();
+		std::advance(i, index);
+
+		// Link it from src.
+		random_labels(res, src, *i, props, props_n, t, accs, a);
+
+		nodes_to_process.insert(*i);
+		unreachable_nodes.erase(i);
+		break;
+	      }
+	    else
+	      {
+		// Pick a random node.
+		int index = mrand(possibilities--);
+		tgba_explicit::state* dest = states[index];
+
+		// Permute the state with states[possibilities], so we
+		// cannot pick it again.
+		states[index] = states[possibilities];
+		states[possibilities] = dest;
+
+		random_labels(res, src, dest, props, props_n, t, accs, a);
+
+		node_set::iterator j = unreachable_nodes.find(dest);
+		if (j != unreachable_nodes.end())
+		  {
+		    nodes_to_process.insert(dest);
+		    unreachable_nodes.erase(j);
+		    saw_unreachable = true;
+		  }
 	      }
 	  }
-
+	// The node must have at least one successor.
-	// Avoid dead ends.
+	assert(!src->empty());
-	if (res->add_state(src)->empty())
-	  random_labels(res, src, src, props, t, accs, a);
       }
+    // All nodes must be reachable.
+    assert(unreachable_nodes.empty());
+    delete[] props;
     return res;
   }
 

src/tgbaalgos/randomgraph.hh

@@ -65,8 +65,15 @@ namespace spot
   ///   note	= {Reprint of Master's thesis}
   /// }
   /// \endverbatim
-  /// The only difference is that labels are on transitions, and that
+  ///
-  /// acceptance conditions are handled.  Otherwise the logic is the same.
+  /// Although the intent is similar, there are some differences with
+  /// between the above published algorithm and this implementation .
+  /// First labels are on transitions, and acceptance conditions are
+  /// generated too.  Second, the number of successors of a node is
+  /// chosen in \f$[1,n]\f$ following a normal distribution with mean
+  /// \f$1+(n-1)d\f$ and variance \f$(n-1)d(1-d)\f$.  (This is less
+  /// accurate, but faster than considering all possible \a n
+  /// successors one by one.)
   tgba*
   random_graph(int n, float d,
 	       const ltl::atomic_prop_set* ap, bdd_dict* dict,

src/tgbatest/randtgba.cc

@@ -111,6 +111,8 @@ syntax(char* prog)
   std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
 	    << std::endl
 	    << "Options:" << std::endl
+	    << "  -0      suppress default output, just generate the graph"
+	    << " in memory" << std::endl
 	    << "  -a N F  number of acceptance conditions and probability that"
 	    << " one is true" << std::endl
 	    << "            [0 0.0]" << std::endl
@@ -334,6 +336,7 @@ main(int argc, char** argv)
   int opt_n = 20;
   float opt_t = 0.5;
 
+  bool opt_0 = false;
   bool opt_z = false;
   bool opt_Z = false;
 
@@ -357,7 +360,11 @@ main(int argc, char** argv)
 
   while (++argn < argc)
     {
-      if (!strcmp(argv[argn], "-a"))
+      if (!strcmp(argv[argn], "-0"))
+	{
+	  opt_0 = true;
+	}
+      else if (!strcmp(argv[argn], "-a"))
 	{
 	  if (argc < argn + 3)
 	    syntax(argv[0]);
@@ -459,7 +466,7 @@ main(int argc, char** argv)
 	{
 	  if (opt_dot)
 	    dotty_reachable(std::cout, a);
-	  else
+	  else if (!opt_0)
 	    tgba_save_reachable(std::cout, a);
 	}
       else