From 760d75cc4410112d682d364a681ac164e4e4796e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 5 Sep 2012 12:03:24 +0200 Subject: [PATCH] randltl: first stage of the reimplementation * src/bin/common_range.cc, src/bin/common_range.hh: New files, extracted from... * src/bin/genltl.cc: ... here. * src/bin/randltl.cc, src/bin/man/randltl.x: New files. * src/bin/Makefile.am, src/bin/man/Makefile.am: Adjust. * src/bin/man/genltl.x: Point to randltl(1). --- src/bin/Makefile.am | 7 +- src/bin/common_range.cc | 75 +++++++++ src/bin/common_range.hh | 39 +++++ src/bin/genltl.cc | 58 +------ src/bin/man/Makefile.am | 7 +- src/bin/man/genltl.x | 2 + src/bin/man/randltl.x | 6 + src/bin/randltl.cc | 357 ++++++++++++++++++++++++++++++++++++++++ 8 files changed, 497 insertions(+), 54 deletions(-) create mode 100644 src/bin/common_range.cc create mode 100644 src/bin/common_range.hh create mode 100644 src/bin/man/randltl.x create mode 100644 src/bin/randltl.cc diff --git a/src/bin/Makefile.am b/src/bin/Makefile.am index f0ed4861b..a5004bf91 100644 --- a/src/bin/Makefile.am +++ b/src/bin/Makefile.am @@ -26,9 +26,10 @@ AM_CPPFLAGS = -I$(top_srcdir)/src -I$(top_builddir)/src $(BUDDY_CPPFLAGS) \ AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = $(top_builddir)/src/libspot.la $(top_builddir)/lib/libgnu.a -bin_PROGRAMS = ltlfilt genltl +bin_PROGRAMS = ltlfilt genltl randltl -noinst_HEADERS = common_output.hh +noinst_HEADERS = common_output.hh common_range.hh ltlfilt_SOURCES = ltlfilt.cc common_output.cc -genltl_SOURCES = genltl.cc common_output.cc +genltl_SOURCES = genltl.cc common_output.cc common_range.cc +randltl_SOURCES = randltl.cc common_output.cc common_range.cc diff --git a/src/bin/common_range.cc b/src/bin/common_range.cc new file mode 100644 index 000000000..052346097 --- /dev/null +++ b/src/bin/common_range.cc @@ -0,0 +1,75 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifdef HAVE_CONFIG_H +# include "config.h" +#endif + +#include "error.h" + +#include "common_range.hh" +#include +#include + +range +parse_range(const char* str) +{ + range res; + + // The range should have the form INT..INT or INT:INT, with + // "42" standing for "42..42", and "..42" meaning "1..42". + char* end; + res.min = strtol(str, &end, 10); + if (end == str) + { + // No leading number. It's OK as long as the string is not + // empty. + if (!*end) + error(1, 0, "invalid empty range"); + res.min = 1; + } + if (!*end) + { + // Only one number. + res.max = res.min; + } + else + { + // Skip : or .. + if (end[0] == ':') + ++end; + else if (end[0] == '.' && end[1] == '.') + end += 2; + + // Parse the next integer. + char* end2; + res.max = strtol(end, &end2, 10); + if (end == end2) + error(1, 0, "invalid range '%s' (missing end?)", str); + if (*end2) + error(1, 0, "invalid range '%s' (trailing garbage?)", str); + } + + if (res.min < 0 || res.max < 0) + error(1, 0, "invalid range '%s': values must be positive", str); + + return res; +} diff --git a/src/bin/common_range.hh b/src/bin/common_range.hh new file mode 100644 index 000000000..e3d1ea041 --- /dev/null +++ b/src/bin/common_range.hh @@ -0,0 +1,39 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifndef SPOT_BIN_COMMON_RANGE_HH +#define SPOT_BIN_COMMON_RANGE_HH + + +#define RANGE_DOC \ + { 0, 0, 0, 0, "RANGE may have one of the following forms: 'INT', " \ + "'INT..INT', or '..INT'.\nIn the latter case, the missing number " \ + "is assumed to be 1.", 0 } + +struct range +{ + int min; + int max; +}; + +range parse_range(const char* str); + +#endif // SPOT_BIN_COMMON_RANGE_HH diff --git a/src/bin/genltl.cc b/src/bin/genltl.cc index b7de859b0..4b912cb19 100644 --- a/src/bin/genltl.cc +++ b/src/bin/genltl.cc @@ -81,6 +81,7 @@ #include #include "common_output.hh" +#include "common_range.hh" #include "misc/_config.h" #include @@ -178,10 +179,7 @@ static const argp_option options[] = { "u-right", OPT_U_RIGHT, "RANGE", 0, "(p1 U (p2 U (... U pn)))", 0 }, OPT_ALIAS(gh-u2), OPT_ALIAS(go-phi), - { 0, 0, 0, 0, "RANGE may have one of the following forms: 'INT', " - "'INT..INT', or '..INT'.\nIn the latter case, the missing number " - "is assumed to be 1.", 0 }, - + RANGE_DOC, /**************************************************/ { 0, 0, 0, 0, "Output options:", -20 }, { 0, 0, 0, 0, "Miscellaneous options:", -1 }, @@ -191,8 +189,7 @@ static const argp_option options[] = struct job { int pattern; - int range_min; - int range_max; + struct range range; }; typedef std::vector jobs_t; @@ -211,53 +208,16 @@ const struct argp_child children[] = // char* endptr; // int res = strtol(s, &endptr, 10); // if (*endptr) -// error(1, 0, "failed to parse '%s' as an integer.", s); +// error(2, 0, "failed to parse '%s' as an integer.", s); // return res; // } static void -enqueue_job(int pattern, const char* range) +enqueue_job(int pattern, const char* range_str) { job j; j.pattern = pattern; - - // Parse the range; it should have the form INT..INT or INT:INT - - char* end; - j.range_min = strtol(range, &end, 10); - if (end == range) - { - // No leading number. It's OK as long as the string is not - // empty. - if (!*end) - error(1, 0, "invalid empty range"); - j.range_min = 1; - } - if (!*end) - { - // Only one number. - j.range_max = j.range_min; - } - else - { - // Skip : or .. - if (end[0] == ':') - ++end; - else if (end[0] == '.' && end[1] == '.') - end += 2; - - // Parse the next integer. - char* end2; - j.range_max = strtol(end, &end2, 10); - if (end == end2) - error(1, 0, "invalid range '%s' (missing end?)", range); - if (*end2) - error(1, 0, "invalid range '%s' (trailing garbage?)", range); - } - - if (j.range_min < 0 || j.range_max < 0) - error(1, 0, "invalid range '%s': values must be positive", range); - + j.range = parse_range(range_str); jobs.push_back(j); } @@ -872,12 +832,12 @@ run_jobs() jobs_t::const_iterator i; for (i = jobs.begin(); i != jobs.end(); ++i) { - int inc = (i->range_max < i->range_min) ? -1 : 1; - int n = i->range_min; + int inc = (i->range.max < i->range.min) ? -1 : 1; + int n = i->range.min; for (;;) { output_pattern(i->pattern, n); - if (n == i->range_max) + if (n == i->range.max) break; n += inc; } diff --git a/src/bin/man/Makefile.am b/src/bin/man/Makefile.am index b8196ae0c..96bfa5fc5 100644 --- a/src/bin/man/Makefile.am +++ b/src/bin/man/Makefile.am @@ -24,9 +24,9 @@ x_to_1 = $(top_builddir)/tools/x-to-1 convman = ARGP_HELP_FMT=header-col=0 $(SHELL) "$(x_to_1)" \ "$(PERL)" "$(top_srcdir)/tools/help2man -N" -dist_man1_MANS = ltlfilt.1 genltl.1 +dist_man1_MANS = ltlfilt.1 genltl.1 randltl.1 MAINTAINERCLEANFILES = $(dist_man1_MANS) -man_aux = $(dist_man1_MANS:.1=.x) +EXTRA_DIST = $(dist_man1_MANS:.1=.x) ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc $(convman) ../ltlfilt$(EXEEXT) $(srcdir)/ltlfilt.x $@ @@ -34,4 +34,7 @@ ltlfilt.1: $(common_dep) $(srcdir)/ltlfilt.x $(srcdir)/../ltlfilt.cc genltl.1: $(common_dep) $(srcdir)/genltl.x $(srcdir)/../genltl.cc $(convman) ../genltl$(EXEEXT) $(srcdir)/genltl.x $@ +randltl.1: $(common_dep) $(srcdir)/randltl.x $(srcdir)/../randltl.cc + $(convman) ../randltl$(EXEEXT) $(srcdir)/randltl.x $@ + diff --git a/src/bin/man/genltl.x b/src/bin/man/genltl.x index ca1df1fe8..f55efcc94 100644 --- a/src/bin/man/genltl.x +++ b/src/bin/man/genltl.x @@ -20,3 +20,5 @@ Proceedings of CAV'01. LNCS 2102 rv K. Rozier and M. Vardi: LTL Satisfiability Checking. Proceedings of Spin'07. LNCS 4595. +[SEE ALSO] +randltl(1) diff --git a/src/bin/man/randltl.x b/src/bin/man/randltl.x new file mode 100644 index 000000000..1c6fb7281 --- /dev/null +++ b/src/bin/man/randltl.x @@ -0,0 +1,6 @@ +[NAME] +randltl \- generate random LTL/PSL formulas +[DESCRIPTION] +.\" Add any additional description here +[SEE ALSO] +genltl(1), ltlfilt(1) diff --git a/src/bin/randltl.cc b/src/bin/randltl.cc new file mode 100644 index 000000000..6395ff968 --- /dev/null +++ b/src/bin/randltl.cc @@ -0,0 +1,357 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2012 Laboratoire de Recherche et Développement de +// l'Epita (LRDE). +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 2 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with Spot; see the file COPYING. If not, write to the Free +// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA +// 02111-1307, USA. + +#ifdef HAVE_CONFIG_H +# include "config.h" +#endif + +#include +#include +#include +#include +#include "progname.h" +#include "error.h" + +#include "common_output.hh" +#include "common_range.hh" + +#include "misc/_config.h" +#include +#include "ltlast/atomic_prop.hh" +#include "ltlvisit/randomltl.hh" +#include "ltlvisit/tostring.hh" +#include "ltlvisit/length.hh" +#include "ltlvisit/simplify.hh" +#include "ltlenv/defaultenv.hh" +#include "misc/random.hh" +#include "misc/hash.hh" + +const char* argp_program_version = "\ +randltl (" SPOT_PACKAGE_STRING ")\n\ +\n\ +Copyright (C) 2012 Laboratoire de Recherche et Développement de l'Epita.\n\ +This is free software; see the source for copying conditions. There is NO\n\ +warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE,\n\ +to the extent permitted by law."; + +const char* argp_program_bug_address = "<" SPOT_PACKAGE_BUGREPORT ">"; + +const char argp_program_doc[] ="\ +Generate random temporal logic formulas.\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\ +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\ + % ./randltl --ltl-priorities='xor=0,implies=0,equiv=0,X=10' -n10 a b c\n\ +"; + +#define OPT_DUMP_PRIORITIES 1 +#define OPT_LTL_PRIORITIES 2 +#define OPT_SERE_PRIORITIES 3 +#define OPT_PSL_PRIORITIES 4 +#define OPT_BOOLEAN_PRIORITIES 5 +#define OPT_SEED 6 +#define OPT_TREE_SIZE 7 + +static const argp_option options[] = + { + // Keep this alphabetically sorted (expect for aliases). + /**************************************************/ + { 0, 0, 0, 0, "Type of formula to generate:", 1 }, + { "boolean", 'B', 0, 0, "generate Boolean formulas", 0 }, + { "ltl", 'L', 0, 0, "generate LTL formulas (default)", 0 }, + { "sere", 'S', 0, 0, "generate SERE", 0 }, + { "psl", 'P', 0, 0, "generate PSL formulas", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Generation:", 2 }, + { "formulas", 'n', "INT", 0, "number of formulas to output (1)\n"\ + "use a negative value for unbounded generation", 0 }, + { "seed", OPT_SEED, "INT", 0, + "seed for the random number generator (0)", 0 }, + { "tree-size", OPT_TREE_SIZE, "RANGE", 0, + "tree size of the formulas generated, before mandatory "\ + "trivial simplifications (15)", 0 }, + { "unique", 'u', 0, 0, "do not generate duplicate formulas", 0 }, + RANGE_DOC, + /**************************************************/ + { 0, 0, 0, 0, "Adjusting probabilities:", 3 }, + { "dump-priorities", OPT_DUMP_PRIORITIES, 0, 0, + "show current priorities, do not generate any formula", 0 }, + { "ltl-priorities", OPT_LTL_PRIORITIES, "STRING", 0, + "set priorities for LTL formulas", 0 }, + { "sere-priorities", OPT_SERE_PRIORITIES, "STRING", 0, + "set priorities for SERE formulas", 0 }, + { "boolean-priorities", OPT_BOOLEAN_PRIORITIES, "STRING", 0, + "set priorities for Boolean formulas", 0 }, + { 0, 0, 0, 0, "STRING should be a comma-separated list of " + "assignments, assigning integer priorities to the tokens " + "listed by --dump-priorities.", 0 }, + /**************************************************/ + { 0, 0, 0, 0, "Output options:", -20 }, + { 0, 0, 0, 0, "Miscellaneous options:", -1 }, + { 0, 0, 0, 0, 0, 0 } + }; + + +const struct argp_child children[] = + { + { &output_argp, 0, 0, -20 }, + { 0, 0, 0, 0 } + }; + +static enum { OutputBool, OutputLTL, OutputSERE, OutputPSL } + output = OutputLTL; +spot::ltl::atomic_prop_set aprops; +static char* opt_pL = 0; +static char* opt_pS = 0; +static char* opt_pB = 0; +static bool opt_dump_priorities = false; +static int opt_formulas = 1; +static int opt_seed = 0; +static range opt_tree_size = { 15, 15 }; +static bool opt_unique = false; + +static int +to_int(const char* s) +{ + char* endptr; + int res = strtol(s, &endptr, 10); + if (*endptr) + error(2, 0, "failed to parse '%s' as an integer.", s); + return res; +} + +static int +parse_opt(int key, char* arg, struct argp_state*) +{ + // This switch is alphabetically-ordered. + switch (key) + { + case 'B': + output = OutputBool; + break; + case 'L': + output = OutputLTL; + break; + case 'n': + opt_formulas = to_int(arg); + break; + case 'P': + output = OutputPSL; + break; + case 'S': + output = OutputSERE; + break; + case 'u': + opt_unique = true; + break; + case OPT_BOOLEAN_PRIORITIES: + opt_pB = arg; + break; + case OPT_LTL_PRIORITIES: + opt_pL = arg; + break; + case OPT_DUMP_PRIORITIES: + opt_dump_priorities = true; + break; + // case OPT_PSL_PRIORITIES: break; + case OPT_SERE_PRIORITIES: + opt_pS = arg; + break; + case OPT_SEED: + opt_seed = to_int(arg); + break; + case OPT_TREE_SIZE: + opt_tree_size = parse_range(arg); + if (opt_tree_size.min > opt_tree_size.max) + std::swap(opt_tree_size.min, opt_tree_size.max); + break; + case ARGP_KEY_ARG: + aprops.insert(static_cast + (spot::ltl::default_environment::instance().require(arg))); + break; + default: + return ARGP_ERR_UNKNOWN; + } + return 0; +} + +int +main(int argc, char** argv) +{ + set_program_name(argv[0]); + // Simplify the program name, because argp() uses it to report errors + // and display help text. + argv[0] = const_cast(program_name); + + const argp ap = { options, parse_opt, "PROP...", argp_program_doc, + children, 0, 0 }; + + if (int err = argp_parse(&ap, argc, argv, 0, 0, 0)) + exit(err); + + spot::ltl::random_formula* rf = 0; + spot::ltl::random_psl* rp = 0; + spot::ltl::random_sere* rs = 0; + const char* tok_pL = 0; + const char* tok_pS = 0; + const char* tok_pB = 0; + + switch (output) + { + case OutputLTL: + rf = new spot::ltl::random_ltl(&aprops); + tok_pL = rf->parse_options(opt_pL); + if (opt_pS) + error(2, 0, "option --sere-priorities unsupported for LTL output"); + if (opt_pB) + error(2, 0, "option --boolean-priorities unsupported for LTL output"); + break; + case OutputBool: + rf = new spot::ltl::random_boolean(&aprops); + tok_pB = rf->parse_options(opt_pB); + if (opt_pL) + error(2, 0, "option --ltl-priorities unsupported for Boolean output"); + if (opt_pS) + error(2, 0, "option --sere-priorities unsupported for Boolean output"); + break; + case OutputSERE: + rf = rs = new spot::ltl::random_sere(&aprops); + tok_pS = rf->parse_options(opt_pS); + if (opt_pL) + error(2, 0, "option --ltl-priorities unsupported for SERE output"); + break; + case OutputPSL: + rf = rp = new spot::ltl::random_psl(&aprops); + rs = &rp->rs; + tok_pL = rp->parse_options(opt_pL); + tok_pS = rs->parse_options(opt_pS); + tok_pB = rs->rb.parse_options(opt_pB); + break; + } + + if (tok_pL) + error(2, 0, "failed to parse LTL priorities near '%s'", tok_pL); + if (tok_pS) + error(2, 0, "failed to parse SERE priorities near '%s'", tok_pS); + if (tok_pB) + error(2, 0, "failed to parse Boolean priorities near '%s'", tok_pB); + + if (opt_dump_priorities) + { + switch (output) + { + case OutputLTL: + std::cout + << "Use --ltl-priorities to set the following LTL priorities:\n"; + rf->dump_priorities(std::cout); + break; + case OutputBool: + std::cout + << ("Use --boolean-priorities to set the following Boolean " + "formula priorities:\n"); + rf->dump_priorities(std::cout); + break; + case OutputPSL: + std::cout + << "Use --ltl-priorities to set the following LTL priorities:\n"; + rp->dump_priorities(std::cout); + // Fall through. + case OutputSERE: + std::cout + << "Use --sere-priorities to set the following SERE priorities:\n"; + rs->dump_priorities(std::cout); + std::cout + << ("Use --boolean-priorities to set the following Boolean " + "formula priorities:\n"); + rs->rb.dump_priorities(std::cout); + break; + default: + error(2, 0, "internal error: unknown type of output"); + } + exit(0); + } + + if (aprops.empty()) + error(2, 0, "No atomic proposition supplied? Run '%s --help' for usage.", + program_name); + + typedef Sgi::hash_set > fset_t; + + fset_t unique_set; + + while (opt_formulas < 0 || opt_formulas--) + { +#define MAX_TRIALS 100000 + unsigned trials = MAX_TRIALS; + bool ignore; + const spot::ltl::formula* f = 0; + spot::srand(opt_seed++); + do + { + ignore = false; + int size = opt_tree_size.min; + if (size != opt_tree_size.max) + size = spot::rrand(size, opt_tree_size.max); + f = rf->generate(size); + if (opt_unique) + { + if (unique_set.insert(f).second) + { + f->clone(); + } + else + { + ignore = true; + f->destroy(); + } + } + } + while (ignore && --trials); + if (trials == 0) + error(2, 0, "failed to generate a new unique formula after %d trials", + MAX_TRIALS); + output_formula(f); + f->destroy(); + }; + + + delete rf; + // Cleanup the unicity table. + { + fset_t::const_iterator i; + for (i = unique_set.begin(); i != unique_set.end(); ++i) + (*i)->destroy(); + } + // Cleanup the atomic_prop set. + { + spot::ltl::atomic_prop_set::const_iterator i = aprops.begin(); + while (i != aprops.end()) + (*(i++))->destroy(); + } + return 0; +}