randltl.cc 11.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
// -*- 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 <iostream>
#include <fstream>
#include <argp.h>
#include <cstdlib>
30
#include <iterator>
31
32
33
34
35
#include "progname.h"
#include "error.h"

#include "common_output.hh"
#include "common_range.hh"
36
#include "common_r.hh"
37
38
39
40

#include "misc/_config.h"
#include <sstream>
#include "ltlast/atomic_prop.hh"
41
42
#include "ltlast/multop.hh"
#include "ltlast/unop.hh"
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
#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\
72
  % ./randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b c\n\
73
74
75
76
77
78
79
80
81
";

#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
82
#define OPT_WF 8
83
#define OPT_DUPS 9
84
85
86
87
88
89
90
91
92
93
94
95

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 },
96
97
    { "weak-fairness", OPT_WF, 0, 0,
      "append some weak-fairness conditions", 0 },
98
99
100
101
102
103
104
    { "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 },
105
106
    { "allow-dups", OPT_DUPS, 0, 0,
      "allow duplicate formulas to be output", 0 },
107
    DECLARE_OPT_R,
108
    RANGE_DOC,
109
    LEVEL_DOC(3),
110
    /**************************************************/
111
    { 0, 0, 0, 0, "Adjusting probabilities:", 4 },
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
    { "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 };
146
static bool opt_unique = true;
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
static bool opt_wf = false;

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;
  spot::ltl::atomic_prop_set::const_iterator i;
  for (i = ap.begin(); i != ap.end(); ++i)
    {
      const spot::ltl::formula* f =
	spot::ltl::unop::instance(spot::ltl::unop::F, (*i)->clone());
      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
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210

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;
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
245
246
247
248
249
250
251
252
253
254
255
256
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
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
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
    case ARGP_KEY_ARG:
      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)
{
  set_program_name(argv[0]);
  // Simplify the program name, because argp() uses it to report errors
  // and display help text.
  argv[0] = const_cast<char*>(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<const spot::ltl::formula*,
			const spot::ptr_hash<const spot::ltl::formula> > fset_t;

  fset_t unique_set;

359
360
  spot::ltl::ltl_simplifier simpl(simplifier_options());

361
362
363
364
365
366
367
368
369
370
371
372
373
374
  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);
375
376
377
378
379
380
381
382
383

	  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));
	    }

384
385
386
387
388
389
	  if (simplification_level)
	    {
	      const spot::ltl::formula* tmp = simpl.simplify(f);
	      f->destroy();
	      f = tmp;
	    }
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
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);
      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;
}