randltl.cc 12.5 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
// 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
34
35

#include <sstream>
#include "ltlast/atomic_prop.hh"
36
37
#include "ltlast/multop.hh"
#include "ltlast/unop.hh"
38
39
40
41
42
43
44
45
46
#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_doc[] ="\
47
48
49
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\
50
51
52
53
54
55
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\
56
57
58
59
If you do not mind about the name of the atomic propositions, just give\n\
a number instead:\n\
  % ./randltl -n10 3\n\
\n\
60
61
62
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\
63
  % ./randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b c\n\
64
65
66
67
68
69
70
71
72
";

#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
73
#define OPT_WF 8
74
#define OPT_DUPS 9
75
76
77
78
79
80
81
82
83
84
85
86

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 },
87
88
    { "weak-fairness", OPT_WF, 0, 0,
      "append some weak-fairness conditions", 0 },
89
90
91
92
93
94
95
    { "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 },
96
97
    { "allow-dups", OPT_DUPS, 0, 0,
      "allow duplicate formulas to be output", 0 },
98
    DECLARE_OPT_R,
99
    RANGE_DOC,
100
    LEVEL_DOC(3),
101
    /**************************************************/
102
    { 0, 0, 0, 0, "Adjusting probabilities:", 4 },
103
104
105
106
107
108
109
110
111
112
113
114
115
    { "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 },
116
117
118
119
120
121
122
123
    { 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 },
124
125
126
127
128
129
130
131
    { 0, 0, 0, 0, "Miscellaneous options:", -1 },
    { 0, 0, 0, 0, 0, 0 }
  };


const struct argp_child children[] =
  {
    { &output_argp, 0, 0, -20 },
132
    { &misc_argp, 0, 0, -1 },
133
134
135
136
137
138
139
140
141
142
143
144
145
    { 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 };
146
static bool opt_unique = true;
147
static bool opt_wf = false;
148
static bool ap_count_given = false;
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169

void
remove_some_props(spot::ltl::atomic_prop_set& s)
{
  // How many propositions to remove from s?
  // (We keep at least one.)
  size_t n = spot::mrand(s.size());

  while (n--)
    {
      spot::ltl::atomic_prop_set::iterator i = s.begin();
      std::advance(i, spot::mrand(s.size()));
      s.erase(i);
    }
}

// GF(p_1) & GF(p_2) & ... & GF(p_n)
const spot::ltl::formula*
GF_n(spot::ltl::atomic_prop_set& ap)
{
  const spot::ltl::formula* res = 0;
170
  for (auto v: ap)
171
172
    {
      const spot::ltl::formula* f =
173
	spot::ltl::unop::instance(spot::ltl::unop::F, v->clone());
174
175
176
177
178
179
180
181
      f = spot::ltl::unop::instance(spot::ltl::unop::G, f);
      if (res)
        res = spot::ltl::multop::instance(spot::ltl::multop::And, f, res);
      else
        res = f;
    }
  return res;
}
182
183
184
185
186
187
188
189
190
191
192
193

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
194
parse_opt(int key, char* arg, struct argp_state* as)
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
{
  // 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;
211
212
213
    case OPT_R:
      parse_r(arg);
      break;
214
215
216
217
218
219
    case 'S':
      output = OutputSERE;
      break;
    case OPT_BOOLEAN_PRIORITIES:
      opt_pB = arg;
      break;
220
221
222
    case OPT_DUPS:
      opt_unique = false;
      break;
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
    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;
241
242
243
    case OPT_WF:
      opt_wf = true;
      break;
244
    case ARGP_KEY_ARG:
245
246
247
248
249
250
251
252
253
254
255
256
257
258
      // 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;
259
	      aprops = spot::ltl::create_atomic_prop_set(res);
260
261
262
	      break;
	    }
	}
263
264
265
266
267
268
269
270
271
272
273
274
      aprops.insert(static_cast<const spot::ltl::atomic_prop*>
		    (spot::ltl::default_environment::instance().require(arg)));
      break;
    default:
      return ARGP_ERR_UNKNOWN;
    }
  return 0;
}

int
main(int argc, char** argv)
{
275
  setup(argv);
276

277
  const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
278
279
		    children, 0, 0 };

280
  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, 0, 0))
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
    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);
310
311
      tok_pS = rs->parse_options(opt_pS);
      tok_pB = rs->rb.parse_options(opt_pB);
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
      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");
	}
363
      destroy_atomic_prop_set(aprops);
364
365
366
      exit(0);
    }

367
368
369
  // 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)
370
371
372
    error(2, 0, "No atomic proposition supplied?   Run '%s --help' for usage.",
	  program_name);

373
374
  spot::srand(opt_seed);

375
376
377
  typedef
    std::unordered_set<const spot::ltl::formula*,
		       const spot::ptr_hash<const spot::ltl::formula>> fset_t;
378
379
  fset_t unique_set;

380
381
  spot::ltl::ltl_simplifier simpl(simplifier_options());

382
383
384
385
386
387
388
389
390
391
392
393
394
  while (opt_formulas < 0 || opt_formulas--)
    {
#define MAX_TRIALS 100000
      unsigned trials = MAX_TRIALS;
      bool ignore;
      const spot::ltl::formula* f = 0;
      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);
395
396
397
398
399
400
401
402
403

	  if (opt_wf)
	    {
	      spot::ltl::atomic_prop_set s = aprops;
	      remove_some_props(s);
	      f = spot::ltl::multop::instance(spot::ltl::multop::And,
					      f, GF_n(s));
	    }

404
405
406
407
408
409
	  if (simplification_level)
	    {
	      const spot::ltl::formula* tmp = simpl.simplify(f);
	      f->destroy();
	      f = tmp;
	    }
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
	  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);
427
      static int count = 0;
428
      output_formula_checked(f, 0, ++count);
429
430
431
432
433
434
      f->destroy();
    };


  delete rf;
  // Cleanup the unicity table.
435
436
  for (auto i: unique_set)
    i->destroy();
437
  // Cleanup the atomic_prop set.
438
  destroy_atomic_prop_set(aprops);
439
440
  return 0;
}