ltlmix: learn option -R for random conjuncts

* bin/ltlmix.cc: Implement this option.
* doc/org/ltlmix.org: Illustrate it.
* tests/core/ltlmix.test: Add a test.

bin/ltlmix.cc

@@ -68,26 +68,31 @@ static const argp_option options[] = {
     // Keep this alphabetically sorted (expect for aliases).
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Generation parameters:", 2 },
+    { "allow-dups", OPT_DUPS, nullptr, 0,
+      "allow duplicate formulas to be output", 0 },
     { "ap-count", 'A', "N", 0,
       "rename the atomic propositions in each selected formula by drawing "
       "randomly from N atomic propositions (the rewriting is bijective "
       "if N is larger than the original set)", 0 },
-    { "polarized-ap", 'P', "N", 0,
-      "similar to -A N, but randomize the polarity of the new atomic "
-      "proposition", 0 },
     { "boolean", 'B', nullptr, 0,
-      "generate Boolean combination of formulas (default)", 0 },
-    { "allow-dups", OPT_DUPS, nullptr, 0,
-      "allow duplicate formulas to be output", 0 },
-    { "ltl", 'L', nullptr, 0, "generate LTL combinations of subformulas", 0 },
+      "generate Boolean combinations of formulas (default)", 0 },
     { "formulas", 'n', "INT", 0,
       "number of formulas to generate (default: 1);\n"
       "use a negative value for unbounded generation", 0 },
+    { "ltl", 'L', nullptr, 0, "generate LTL combinations of subformulas", 0 },
+    { "polarized-ap", 'P', "N", 0,
+      "similar to -A N, but randomize the polarity of the new atomic "
+      "propositions", 0 },
+    { "random-conjuncts", 'C', "N", 0,
+      "generate random-conjunctions of N conjuncts; "
+      "shorthand for --tree-size {2N-1} -B "
+      "--boolean-priorities=[disable everything but 'and']", 0 },
     { "seed", OPT_SEED, "INT", 0,
       "seed for the random number generator (default: 0)", 0 },
     { "tree-size", OPT_TREE_SIZE, "RANGE", 0,
       "tree size of main pattern generated (default: 5);\n"
       "input formulas count as size 1.", 0 },
+    RANGE_DOC,
     /**************************************************/
     { nullptr, 0, nullptr, 0, "Adjusting probabilities:", 4 },
     { "dump-priorities", OPT_DUMP_PRIORITIES, nullptr, 0,
@@ -129,6 +134,7 @@ static spot::randltlgenerator::output_type output =
   spot::randltlgenerator::Bool;
 static char* opt_pL = nullptr;
 static char* opt_pB = nullptr;
+static char random_conj[] = "not=0,implies=0,equiv=0,xor=0,or=0";
 static bool opt_dump_priorities = false;
 static int opt_seed = 0;
 static range opt_tree_size = { 5, 5 };
@@ -178,6 +184,14 @@ parse_opt(int key, char* arg, struct argp_state*)
     case 'B':
       output = spot::randltlgenerator::Bool;
       break;
+    case 'C':
+      {
+        int s = 2 * to_int(arg, "-C/--random-conjuncs") - 1;
+        opt_tree_size = {s, s};
+        output = spot::randltlgenerator::Bool;
+        opt_pB = random_conj;
+        break;
+      }
     case 'L':
       output = spot::randltlgenerator::LTL;
       break;

doc/org/ltlmix.org

@@ -324,10 +324,10 @@ so is uses atomic propositions $\{p_0,p_1,...\}$ starting at 0 and without gap.
 
 ** Random conjunctions
 
-Some benchmark (e.g., [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][for LTL satisfiability]]) are built by conjunction
-of $L$ random formulas picked from a set of basic formulas.  Each
-picked formula has its atomic proposition mapped to random literals
-built from a subset of $m$ atomic variables.
+Some benchmarks (e.g., [[https://www.cs.rice.edu/~vardi/papers/time13.pdf][for LTL satisfiability]]) are built by
+conjunction of $L$ random formulas picked from a set of basic
+formulas.  Each picked formula has its atomic proposition mapped to
+random literals built from a subset of $m$ atomic variables.
 
 Given a value for $m$, option =-P m= will achieve the second part of
 the above description.  To build a conjunction of $L$ formulas, we
@@ -359,7 +359,30 @@ Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12
 Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31
 #+end_example
 
+In fact building random conjunctions is common enough to have its own
+flag.  Using =-C N= will see the tree size to $2N-1$ and disable all
+operators but =and=.  The above command can therefore be reduced to
+
+#+BEGIN_SRC sh :exports both
+  ltlmix -fGa -fFa -fXa -n10 -P50 -C10
+#+END_SRC
+
+#+RESULTS:
+#+begin_example
+Xp27 & F!p21 & G!p19 & X!p26 & Fp4 & Gp43 & Fp39 & Fp7
+G!p28 & G!p30 & X!p34 & Fp21 & Gp3 & Fp6 & F!p18 & Xp5 & Fp8 & F!p12
+X!p32 & Xp9 & Gp4 & Xp48 & F!p48 & X!p6 & Fp5 & Xp20 & Fp28 & Fp26
+G!p46 & X!p14 & Fp29 & X!p36 & Fp12 & Xp47 & Fp42 & Gp14 & Fp19
+G!p28 & Fp21 & Fp36 & F!p0 & G!p14 & Xp21 & F!p28 & G!p21 & Gp21 & Gp40
+Gp3 & F!p48 & F!p28 & Xp7 & Gp8 & Xp42 & Gp0 & Xp36 & F!p2 & G!p0
+Xp36 & Xp46 & F!p31 & Xp11 & Xp26 & G!p9 & F!p36 & X!p12 & Fp15 & Xp18
+Xp9 & X!p33 & Fp44 & X!p13 & Gp37 & Xp19 & G!p43 & F!p34 & Gp36 & Gp10
+Xp27 & Xp5 & Fp28 & Xp18 & G!p13 & Gp35 & Gp38 & G!p45 & G!p48 & Gp12
+Xp7 & G!p48 & Xp14 & Fp24 & Xp43 & Fp47 & Fp14 & Gp30 & Xp23 & G!p31
+#+end_example
+
+
 Selecting 10 random conjuncts out of 3×50×2=300 possibilities has a
 13.7% chance that at least 2 conjuncts will be identical (see [[https://en.wikipedia.org/wiki/Birthday_problem][Birthday
-paradox]]), so because of Spot's trivial rewritings, some hove the above
+paradox]]), so because of Spot's trivial rewritings, some of the above
 formulas may have fewer than 10 conjuncts.

tests/core/ltlmix.test

@@ -91,3 +91,6 @@ diff out.txt expected
 
 ltlmix -fa -A500 $P,or=0 -n10 | tee out
 test 10 -eq `grep '&.*&' < out | wc -l`
+
+ltlmix -fa -A500 -C3 -n10 | tee out2
+diff out out2