From 174b531f82c3cfc03648424f7d7623dcaf557511 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 6 Jan 2005 12:29:56 +0000
Subject: [PATCH] * src/ltltest/randltl.cc: Add options -r and -u. *
 src/ltltest/reduc.test: Use randltl -u, and run it through valgrind.

---
 ChangeLog              |  5 +++
 src/ltltest/randltl.cc | 84 ++++++++++++++++++++++++++++++++++++++----
 src/ltltest/reduc.test |  4 +-
 3 files changed, 84 insertions(+), 9 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index f980b5f0c..cbec05642 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,8 @@
+2005-01-06  Alexandre Duret-Lutz  <adl@src.lip6.fr>
+
+	* src/ltltest/randltl.cc: Add options -r and -u.
+	* src/ltltest/reduc.test: Use randltl -u, and run it through valgrind.
+
 2005-01-05  Alexandre Duret-Lutz  <adl@src.lip6.fr>
 
 	* src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh: New files.
diff --git a/src/ltltest/randltl.cc b/src/ltltest/randltl.cc
index 2e74df34e..ea9d7aee9 100644
--- a/src/ltltest/randltl.cc
+++ b/src/ltltest/randltl.cc
@@ -20,11 +20,14 @@
 // 02111-1307, USA.
 
 #include <iostream>
+#include <set>
+#include <string>
 #include "ltlast/atomic_prop.hh"
 #include "ltlvisit/randomltl.hh"
 #include "ltlvisit/tostring.hh"
 #include "ltlvisit/destroy.hh"
 #include "ltlvisit/length.hh"
+#include "ltlvisit/reduce.hh"
 #include "ltlenv/defaultenv.hh"
 #include "misc/random.hh"
 
@@ -39,6 +42,11 @@ syntax(char* prog)
 	    << "  -f N    the size of the formula [15]" << std::endl
 	    << "  -F N    number of formulae to generate [1]" << std::endl
 	    << "  -p S    priorities to use" << std::endl
+	    << "  -r N    simplify formulae using all available reductions"
+	    << " and reject those" << std::endl
+	    << "            strictly smaller than N" << std::endl
+	    << "  -u      generate unique formulae"
+	    << std::endl
 	    << "  -s N    seed for the random number generator" << std::endl
 	    << std::endl
 	    << "Where:" << std::endl
@@ -72,6 +80,8 @@ main(int argc, char** argv)
   int opt_f = 15;
   int opt_F = 1;
   char* opt_p = 0;
+  int opt_r = 0;
+  bool opt_u = false;
 
   spot::ltl::environment& env(spot::ltl::default_environment::instance());
   spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;
@@ -105,12 +115,22 @@ main(int argc, char** argv)
 	    syntax(argv[0]);
 	  opt_p = argv[++argn];
 	}
+      else if (!strcmp(argv[argn], "-r"))
+	{
+	  if (argc < argn + 2)
+	    syntax(argv[0]);
+	  opt_r = to_int(argv[++argn]);
+	}
       else if (!strcmp(argv[argn], "-s"))
 	{
 	  if (argc < argn + 2)
 	    syntax(argv[0]);
 	  opt_s = to_int(argv[++argn]);
 	}
+      else if (!strcmp(argv[argn], "-u"))
+	{
+	  opt_u = true;
+	}
       else
 	{
 	  ap->insert(static_cast<spot::ltl::atomic_prop*>
@@ -118,10 +138,7 @@ main(int argc, char** argv)
 	}
     }
 
-  spot::srand(opt_s);
-
   spot::ltl::random_ltl rl(ap);
-
   const char* tok = rl.parse_options(opt_p);
   if (tok)
     {
@@ -130,18 +147,71 @@ main(int argc, char** argv)
       exit(2);
     }
 
+  if (opt_r > opt_F)
+    {
+      std::cerr << "-r's argument (" << opt_r << ") should not be larger than "
+		<< "-F's (" << opt_F << ")" << std::endl;
+      exit(2);
+    }
+
   if (opt_d)
     {
       rl.dump_priorities(std::cout);
     }
   else
     {
+      std::set<std::string> unique;
+
       while (opt_F--)
 	{
-	  spot::ltl::formula* f = rl.generate(opt_f);
-	  std::cout << spot::ltl::to_string(f) << std::endl;
-	  assert(spot::ltl::length(f) <= opt_f);
-	  spot::ltl::destroy(f);
+	  int max_tries_u = 1000;
+	  while (max_tries_u--)
+	    {
+	      spot::srand(opt_s++);
+	      spot::ltl::formula* f;
+	      int max_tries_r = 1000;
+	      while (max_tries_r--)
+		{
+		  f = rl.generate(opt_f);
+		  if (opt_r)
+		    {
+		      spot::ltl::formula* g = reduce(f);
+		      spot::ltl::destroy(f);
+		      if (spot::ltl::length(g) < opt_r)
+			{
+			  spot::ltl::destroy(g);
+			  continue;
+			}
+		      f = g;
+		    }
+		  else
+		    {
+		      assert(spot::ltl::length(f) <= opt_f);
+		    }
+		  break;
+		}
+	      if (max_tries_r < 0)
+		{
+		  assert(opt_r);
+		  std::cerr << "Failed to generate non-reducible formula "
+			    << "of size " << opt_r << " or more." << std::endl;
+		  exit(2);
+		}
+	      std::string txt = spot::ltl::to_string(f);
+	      spot::ltl::destroy(f);
+	      if (!opt_u || unique.insert(txt).second)
+		{
+		  std::cout << txt << std::endl;
+		  break;
+		}
+	    }
+	  if (max_tries_u < 0)
+	    {
+	      assert(opt_u);
+	      std::cerr << "Failed to generate another unique formula."
+			<< std::endl;
+	      exit(2);
+	    }
 	}
     }
   delete ap;
diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test
index cbc152a2c..f50a7fcaf 100755
--- a/src/ltltest/reduc.test
+++ b/src/ltltest/reduc.test
@@ -29,8 +29,8 @@ set -e
 FILE=formulae
 : > $FILE
 for i in 10 11 12 13 14 15 16 17 18 19 20; do
-  ./randltl -s 0   -f $i a b c -F 100 >> $FILE
-  ./randltl -s 100 -f $i a b c d e f -F 100 >> $FILE
+  run 0 ./randltl -u -s 0   -f $i a b c -F 100 >> $FILE
+  run 0 ./randltl -u -s 100 -f $i a b c d e f -F 100 >> $FILE
 done
 
 for opt in 0 1 2 3; do