randltl: accept a number of atomic propositions

Suggested by Joachim Klein.

* src/bin/randltl.cc: Implement it.
* src/ltltest/rand.test: Test it.
* doc/org/randltl.org, NEWS: Document it.

NEWS

@@ -12,6 +12,8 @@ New in spot 1.2.4a (not yet released)
       The corresponding C++ function is spot::hoaf_reachable() in
       tgbaalgos/hoaf.hh.
 
+    - 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'.
+
   * Documentation:
 
     - The man page for ltl2tgba has some new notes and references

doc/org/randltl.org

@@ -19,6 +19,15 @@ randltl a b c
 
 Note that the result does not always use all atomic propositions.
 
+If you do not care about how the atomic propositions are named,
+you can give a nonnegative number instead:
+
+#+BEGIN_SRC sh :results verbatim :exports both
+randltl 3
+#+END_SRC
+#+RESULTS:
+: G(Gp1 W (Gp1 M p2))
+
 The syntax of the formula output can be changed using the
 [[file:ioltl.org][common output options]]:
 
@@ -40,16 +49,16 @@ like =p0=, =p1=, etc... (Atomic proposition named differently will be
 output by Spot in double-quotes, but this is not supported by LBT.)
 
 #+BEGIN_SRC sh :results verbatim :exports both
-randltl -l p1 p2 p3
+randltl -l 3
-randltl -8 p1 p2 p3
+randltl -8 3
-randltl -s p1 p2 p3
+randltl -s 3
-randltl --wring p1 p2 p3
+randltl --wring 3
 #+END_SRC
 #+RESULTS:
-: G W G p2 M G p2 p3
+: G W G p1 M G p1 p2
-: □(□p2 W (□p2 M p3))
+: □(□p1 W (□p1 M p2))
-: []((p3 U (p3 && []p2)) V ([]p2 || (p3 U (p3 && []p2))))
+: []((p2 U (p2 && []p1)) V ([]p1 || (p2 U (p2 && []p1))))
-: (G(((p3=1) U ((p3=1) * (G(p2=1)))) R ((G(p2=1)) + ((p3=1) U ((p3=1) * (G(p2=1)))))))
+: (G(((p2=1) U ((p2=1) * (G(p1=1)))) R ((G(p1=1)) + ((p2=1) U ((p2=1) * (G(p1=1)))))))
 
 As you might guess from the above result, for a given set of atomic
 propositions (and on the same computer) the generated formula will

src/bin/randltl.cc

@@ -44,13 +44,19 @@
 #include "misc/hash.hh"
 
 const char argp_program_doc[] ="\
-Generate random temporal logic formulas.\v\
+Generate random temporal logic formulas.\n\n\
+The formulas are built over the atomic propositions named by PROPS...\n\
+or, if N is a nonnegative number, using N arbitrary names.\v\
 Examples:\n\
 \n\
 The following generates 10 random LTL formulas over the propositions a, b,\n\
 and c, with the default tree-size, and all available operators.\n\
   % randltl -n10 a b c\n\
 \n\
+If you do not mind about the name of the atomic propositions, just give\n\
+a number instead:\n\
+  % ./randltl -n10 3\n\
+\n\
 You can disable or favor certain operators by changing their priority.\n\
 The following disables xor, implies, and equiv, and multiply the probability\n\
 of X to occur by 10.\n\
@@ -139,6 +145,7 @@ static int opt_seed = 0;
 static range opt_tree_size = { 15, 15 };
 static bool opt_unique = true;
 static bool opt_wf = false;
+static bool ap_count_given = false;
 
 void
 remove_some_props(spot::ltl::atomic_prop_set& s)
@@ -185,7 +192,7 @@ to_int(const char* s)
 }
 
 static int
-parse_opt(int key, char* arg, struct argp_state*)
+parse_opt(int key, char* arg, struct argp_state* as)
 {
   // This switch is alphabetically-ordered.
   switch (key)
@@ -236,6 +243,32 @@ parse_opt(int key, char* arg, struct argp_state*)
       opt_wf = true;
       break;
     case ARGP_KEY_ARG:
+      // If this is the unique non-option argument, it can
+      // be a number of atomic propositions to build.
+      //
+      // argp reorganizes argv[] so that options always come before
+      // non-options.  So if as->argc == as->next we know this is the
+      // last non-option argument, and if aprops.empty() we know this
+      // is the also the first one.
+      if (aprops.empty() && as->argc == as->next)
+	{
+	  char* endptr;
+	  int res = strtol(arg, &endptr, 10);
+	  if (!*endptr && res >= 0) // arg is a number
+	    {
+	      ap_count_given = true;
+	      spot::ltl::default_environment& e =
+		spot::ltl::default_environment::instance();
+	      for (int i = 0; i < res; ++i)
+		{
+		  std::ostringstream p;
+		  p << 'p' << i;
+		  aprops.insert(static_cast<const spot::ltl::atomic_prop*>
+				(e.require(p.str())));
+		}
+	      break;
+	    }
+	}
       aprops.insert(static_cast<const spot::ltl::atomic_prop*>
 		    (spot::ltl::default_environment::instance().require(arg)));
       break;
@@ -250,7 +283,7 @@ main(int argc, char** argv)
 {
   setup(argv);
 
-  const argp ap = { options, parse_opt, "PROP...", argp_program_doc,
+  const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
 		    children, 0, 0 };
 
   if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
@@ -340,7 +373,9 @@ main(int argc, char** argv)
       exit(0);
     }
 
-  if (aprops.empty())
+  // running 'randltl 0' is one way to generate formulas using no
+  // atomic propositions so do not complain in that case.
+  if (aprops.empty() && !ap_count_given)
     error(2, 0, "No atomic proposition supplied?   Run '%s --help' for usage.",
 	  program_name);
 

src/ltltest/rand.test

@@ -97,3 +97,29 @@ c
 EOF
 
 diff expected out2
+
+
+# atomic proposition can be implicitly specified using a number
+$randltl -n 1000 3 --tree-size=10..20 > out
+grep -q p0 out
+grep -q p1 out
+grep -q p2 out
+grep p3 out && exit 1
+
+
+# We should be able to generate exactly two formulas with 0 atomic
+# propositions.
+run 0 $randltl -n2 0 | sort > out
+cat >expected <<EOF
+0
+1
+EOF
+diff out expected
+
+# requesting more formulas should fail
+run 2 $randltl -n3 0
+
+# If more numbers are given, there are interpreted as atomic propositions
+run 0 $randltl -n1000 0 1 > out
+grep -q '"0"' out
+grep -q '"1"' out