From 44fc323e7b83e3994e2b8992beb6fb8d251fc57f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Aug 2014 13:17:18 +0200 Subject: [PATCH] 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 | 2 ++ doc/org/randltl.org | 25 +++++++++++++++++-------- src/bin/randltl.cc | 43 +++++++++++++++++++++++++++++++++++++++---- src/ltltest/rand.test | 26 ++++++++++++++++++++++++++ 4 files changed, 84 insertions(+), 12 deletions(-) diff --git a/NEWS b/NEWS index 5d4844a5e..c1956b8fe 100644 --- a/NEWS +++ b/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 diff --git a/doc/org/randltl.org b/doc/org/randltl.org index 7faa12176..a795331f5 100644 --- a/doc/org/randltl.org +++ b/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 -8 p1 p2 p3 -randltl -s p1 p2 p3 -randltl --wring p1 p2 p3 +randltl -l 3 +randltl -8 3 +randltl -s 3 +randltl --wring 3 #+END_SRC #+RESULTS: -: G W G p2 M G p2 p3 -: □(□p2 W (□p2 M p3)) -: []((p3 U (p3 && []p2)) V ([]p2 || (p3 U (p3 && []p2)))) -: (G(((p3=1) U ((p3=1) * (G(p2=1)))) R ((G(p2=1)) + ((p3=1) U ((p3=1) * (G(p2=1))))))) +: G W G p1 M G p1 p2 +: □(□p1 W (□p1 M p2)) +: []((p2 U (p2 && []p1)) V ([]p1 || (p2 U (p2 && []p1)))) +: (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 diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc index b3730f31d..d32cd7d19 100644 --- a/src/bin/randltl.cc +++ b/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 + (e.require(p.str()))); + } + break; + } + } aprops.insert(static_cast (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); diff --git a/src/ltltest/rand.test b/src/ltltest/rand.test index b7750582c..59a0ad660 100755 --- a/src/ltltest/rand.test +++ b/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 < out +grep -q '"0"' out +grep -q '"1"' out