diff --git a/bin/ltlmix.cc b/bin/ltlmix.cc index 9e6ada1c1..1e36eeeb2 100644 --- a/bin/ltlmix.cc +++ b/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; diff --git a/doc/org/ltlmix.org b/doc/org/ltlmix.org index 338122d41..341c64833 100644 --- a/doc/org/ltlmix.org +++ b/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. diff --git a/tests/core/ltlmix.test b/tests/core/ltlmix.test index dd279e4fa..232c1f76c 100755 --- a/tests/core/ltlmix.test +++ b/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