randltl.cc 9.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
3
// Développement de l'Epita (LRDE).
4 5 6 7 8
//
// 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
9
// the Free Software Foundation; either version 3 of the License, or
10 11 12 13 14 15 16 17
// (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
18
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
19

20
#include "common_sys.hh"
21 22 23 24 25

#include <iostream>
#include <fstream>
#include <argp.h>
#include <cstdlib>
26
#include <iterator>
27 28
#include "error.h"

29
#include "common_setup.hh"
30 31
#include "common_output.hh"
#include "common_range.hh"
32
#include "common_r.hh"
33
#include "common_conv.hh"
34 35

#include <sstream>
36 37
#include "ltlast/multop.hh"
#include "ltlast/unop.hh"
38 39 40 41 42 43 44
#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"
45
#include "misc/optionmap.hh"
46 47

const char argp_program_doc[] ="\
48 49 50
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\
51 52 53 54 55 56
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\
57 58
If you do not mind about the name of the atomic propositions, just give\n\
a number instead:\n\
59
  % randltl -n10 3\n\
60
\n\
61 62 63
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\
64
  % randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b c\n\
65 66
";

67 68 69 70 71 72 73 74 75 76 77
enum {
  OPT_BOOLEAN_PRIORITIES = 1,
  OPT_DUMP_PRIORITIES,
  OPT_DUPS,
  OPT_LTL_PRIORITIES,
  OPT_PSL_PRIORITIES,
  OPT_SEED,
  OPT_SERE_PRIORITIES,
  OPT_TREE_SIZE,
  OPT_WF,
};
78 79 80 81 82 83 84 85 86 87 88 89

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 },
90 91
    { "weak-fairness", OPT_WF, 0, 0,
      "append some weak-fairness conditions", 0 },
92 93 94 95 96 97 98
    { "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 },
99 100
    { "allow-dups", OPT_DUPS, 0, 0,
      "allow duplicate formulas to be output", 0 },
101
    DECLARE_OPT_R,
102
    RANGE_DOC,
103
    LEVEL_DOC(3),
104
    /**************************************************/
105
    { 0, 0, 0, 0, "Adjusting probabilities:", 4 },
106 107 108 109 110 111 112 113 114 115 116 117 118
    { "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 },
119 120 121 122 123 124 125 126
    { 0, 0, 0, 0, "The FORMAT string passed to --format may use "\
      "the following interpreted sequences:", -19 },
    { "%f", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the formula (in the selected syntax)", 0 },
    { "%L", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "the (serial) number of the formula", 0 },
    { "%%", 0, 0, OPTION_DOC | OPTION_NO_USAGE,
      "a single %", 0 },
127 128 129 130 131 132 133 134
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { 0, 0, 0, 0, 0, 0 }
  };


const struct argp_child children[] =
  {
    { &output_argp, 0, 0, -20 },
135
    { &misc_argp, 0, 0, -1 },
136 137 138 139
    { 0, 0, 0, 0 }
  };

spot::ltl::atomic_prop_set aprops;
140
static int output = OUTPUTLTL;
141 142 143 144 145 146 147
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 };
148
static bool opt_unique = true;
149
static bool opt_wf = false;
150
static bool ap_count_given = false;
151

152
static int
153
parse_opt(int key, char* arg, struct argp_state* as)
154 155 156 157 158
{
  // This switch is alphabetically-ordered.
  switch (key)
    {
    case 'B':
159
      output = OUTPUTBOOL;
160 161
      break;
    case 'L':
162
      output = OUTPUTLTL;
163 164 165 166 167
      break;
    case 'n':
      opt_formulas = to_int(arg);
      break;
    case 'P':
168
      output = OUTPUTPSL;
169
      break;
170 171 172
    case OPT_R:
      parse_r(arg);
      break;
173
    case 'S':
174
      output = OUTPUTSERE;
175 176 177 178
      break;
    case OPT_BOOLEAN_PRIORITIES:
      opt_pB = arg;
      break;
179 180 181
    case OPT_DUPS:
      opt_unique = false;
      break;
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199
    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;
200 201 202
    case OPT_WF:
      opt_wf = true;
      break;
203
    case ARGP_KEY_ARG:
204 205 206 207 208 209 210 211 212 213 214 215 216 217
      // 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;
218
	      aprops = spot::ltl::create_atomic_prop_set(res);
219 220 221
	      break;
	    }
	}
222
      aprops.insert(spot::ltl::default_environment::instance().require(arg));
223 224 225 226 227 228 229 230 231 232
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

int
main(int argc, char** argv)
{
233
  setup(argv);
234

235
  const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
236 237
		    children, 0, 0 };

238
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
239 240
    exit(err);

241 242 243
  // 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)
244 245 246
    error(2, 0, "No atomic proposition supplied?   Run '%s --help' for usage.",
	  program_name);

247 248
  spot::srand(opt_seed);

249 250 251 252 253 254 255 256
  spot::option_map opts;
  opts.set("output", output);
  opts.set("tree_size_min", opt_tree_size.min);
  opts.set("tree_size_max", opt_tree_size.max);
  opts.set("opt_wf", opt_wf);
  opts.set("opt_seed", opt_seed);
  opts.set("simplification_level", simplification_level);
  spot::ltl::randltlgenerator rg(aprops, opts, opt_pL, opt_pS, opt_pB);
257

258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293
  if (opt_dump_priorities)
    {
      switch (output)
        {
        case OUTPUTLTL:
          std::cout
          << "Use --ltl-priorities to set the following LTL priorities:\n";
          rg.dump_ltl_priorities(std::cout);
          break;
        case OUTPUTBOOL:
          std::cout
          << ("Use --boolean-priorities to set the following Boolean "
              "formula priorities:\n");
          rg.dump_bool_priorities(std::cout);
          break;
        case OUTPUTPSL:
          std::cout
          << "Use --ltl-priorities to set the following LTL priorities:\n";
          rg.dump_psl_priorities(std::cout);
          // Fall through.
        case OUTPUTSERE:
          std::cout
          << "Use --sere-priorities to set the following SERE priorities:\n";
          rg.dump_sere_priorities(std::cout);
          std::cout
          << ("Use --boolean-priorities to set the following Boolean "
              "formula priorities:\n");
          rg.dump_sere_bool_priorities(std::cout);
          break;
        default:
          error(2, 0, "internal error: unknown type of output");
        }
      opts.~option_map();
      destroy_atomic_prop_set(aprops);
      exit(0);
    }
294

295 296
  while (opt_formulas < 0 || opt_formulas--)
    {
297
      static int count = 0;
298 299 300 301 302 303 304 305 306 307 308 309 310
      spot::ltl::randltlgenerator rg2(aprops, opts);
      const spot::ltl::formula* f = rg.next();
      if (!f)
        {
          opts.~option_map();
          error(2, 0, "failed to generate a new unique formula after %d "\
                "trials", MAX_TRIALS);
        }
      else
        {
          output_formula_checked(f, 0, ++count);
          f->destroy();
        }
311 312 313
    };


314
  destroy_atomic_prop_set(aprops);
315 316
  return 0;
}