randltl.cc 9.11 KB
Newer Older
1
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement
Guillaume Sadegh's avatar
Guillaume Sadegh committed
2
3
// de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de
4
5
// Paris 6 (LIP6), dpartement Systmes Rpartis Coopratifs (SRC),
// Universit Pierre et Marie Curie.
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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.

24
#include <cassert>
25
#include <iostream>
26
27
#include <set>
#include <string>
28
29
#include <cstdlib>
#include <cstring>
30
#include "ltlast/atomic_prop.hh"
31
32
33
#include "ltlvisit/randomltl.hh"
#include "ltlvisit/tostring.hh"
#include "ltlvisit/length.hh"
34
#include "ltlvisit/simplify.hh"
35
36
37
38
39
40
41
#include "ltlenv/defaultenv.hh"
#include "misc/random.hh"

void
syntax(char* prog)
{
  std::cerr << "Usage: "<< prog << " [OPTIONS...] PROPS..." << std::endl
42
43
44
45
46
47
	    << std::endl
	    << "Output selection:" << std::endl
	    << "  -B      generate Boolean formulae" << std::endl
	    << "  -L      generate LTL formulae [default]" << std::endl
	    << "  -S      generate SERE" << std::endl
	    << "  -P      generate PSL formulae" << std::endl
48
49
50
51
	    << std::endl
	    << "Options:" << std::endl
	    << "  -d      dump priorities, do not generate any formula"
	    << std::endl
52
53
54
55
56
57
	    << "  -f  N    the size of the formula [15]" << std::endl
	    << "  -F  N    number of formulae to generate [1]" << std::endl
	    << "  -pL S    priorities to use for LTL formula" << std::endl
	    << "  -pS S    priorities to use for SERE" << std::endl
	    << "  -pB S    priorities to use for Boolean formulae" << std::endl
	    << "  -r  N    simplify formulae using all available reductions"
58
59
60
61
	    << " and reject those" << std::endl
	    << "            strictly smaller than N" << std::endl
	    << "  -u      generate unique formulae"
	    << std::endl
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
	    << "  -s N    seed for the random number generator" << std::endl
	    << std::endl
	    << "Where:" << std::endl
	    << "  F      are floating values" << std::endl
	    << "  S      are `KEY=F, KEY=F, ...' strings" << std::endl
	    << "  N      are positive integers" << std::endl
	    << "  PROPS  are the atomic properties to use on transitions"
	    << std::endl
	    << "Use -d to see the list of KEYs." << std::endl;
  exit(2);
}

int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    {
      std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
      exit(1);
    }
  return res;
}

int
main(int argc, char** argv)
{
90
  enum { OutputBool, OutputLTL, OutputSERE, OutputPSL } output = OutputLTL;
91
92
93
94
  bool opt_d = false;
  int opt_s = 0;
  int opt_f = 15;
  int opt_F = 1;
95
96
97
  char* opt_pL = 0;
  char* opt_pS = 0;
  char* opt_pB = 0;
98
99
  int opt_r = 0;
  bool opt_u = false;
100
101
  spot::ltl::ltl_simplifier_options simpopt(true, true, true, true, true);
  spot::ltl::ltl_simplifier simp(simpopt);
102
103
104
105
106
107
108
109
110
111
112

  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* ap = new spot::ltl::atomic_prop_set;

  int argn = 0;

  if (argc <= 1)
    syntax(argv[0]);

  while (++argn < argc)
    {
113
114
115
116
117
      if (!strcmp(argv[argn], "-B"))
	{
	  output = OutputBool;
	}
      else if (!strcmp(argv[argn], "-d"))
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
	{
	  opt_d = true;
	}
      else if (!strcmp(argv[argn], "-f"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_f = to_int(argv[++argn]);
	}
      else if (!strcmp(argv[argn], "-F"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_F = to_int(argv[++argn]);
	}
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
      else if (!strcmp(argv[argn], "-L"))
	{
	  output = OutputLTL;
	}
      else if ((!strcmp(argv[argn], "-p")) || (!strcmp(argv[argn], "-pL")))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_pL = argv[++argn];
	}
      else if (!strcmp(argv[argn], "-pS"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_pS = argv[++argn];
	}
      else if (!strcmp(argv[argn], "-pB"))
150
151
152
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
153
154
155
156
157
	  opt_pB = argv[++argn];
	}
      else if (!strcmp(argv[argn], "-P"))
	{
	  output = OutputPSL;
158
	}
159
160
161
162
163
164
      else if (!strcmp(argv[argn], "-r"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_r = to_int(argv[++argn]);
	}
165
166
167
168
169
170
      else if (!strcmp(argv[argn], "-s"))
	{
	  if (argc < argn + 2)
	    syntax(argv[0]);
	  opt_s = to_int(argv[++argn]);
	}
171
172
173
174
      else if (!strcmp(argv[argn], "-S"))
	{
	  output = OutputSERE;
	}
175
176
177
178
      else if (!strcmp(argv[argn], "-u"))
	{
	  opt_u = true;
	}
179
180
181
182
183
184
185
      else
	{
	  ap->insert(static_cast<spot::ltl::atomic_prop*>
		     (env.require(argv[argn])));
	}
    }

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
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
  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(ap);
      tok_pL = rf->parse_options(opt_pL);
      if (opt_pS)
	{
	  std::cerr << "option -pS unsupported for LTL output" << std::endl;
	  exit(2);
	}
      if (opt_pB)
	{
	  std::cerr << "option -pB unsupported for LTL output" << std::endl;
	  exit(2);
	}
      break;
    case OutputBool:
      rf = new spot::ltl::random_boolean(ap);
      tok_pB = rf->parse_options(opt_pB);
      if (opt_pL)
	{
	  std::cerr << "option -pL unsupported for Boolean output" << std::endl;
	  exit(2);
	}
      if (opt_pS)
	{
	  std::cerr << "option -pS unsupported for Boolean output" << std::endl;
	  exit(2);
	}
      break;
    case OutputSERE:
      rf = rs = new spot::ltl::random_sere(ap);
      tok_pS = rf->parse_options(opt_pS);
      if (opt_pL)
	{
	  std::cerr << "option -pL unsupported for SERE output" << std::endl;
	  exit(2);
	}
      break;
    case OutputPSL:
      rf = rp = new spot::ltl::random_psl(ap);
      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)
241
    {
242
243
      std::cerr << "failed to parse priorities (option -pL) near `"
		<< tok_pL << "'" << std::endl;
244
245
      exit(2);
    }
246
247
248
249
250
251
252
253
254
255
256
257
258
  if (tok_pS)
    {
      std::cerr << "failed to parse priorities (option -pS) near `"
		<< tok_pS << "'" << std::endl;
      exit(2);
    }
  if (tok_pB)
    {
      std::cerr << "failed to parse priorities (option -pB) near `"
		<< tok_pB << "'" << std::endl;
      exit(2);
    }

259

260
  if (opt_r > opt_f)
261
262
    {
      std::cerr << "-r's argument (" << opt_r << ") should not be larger than "
263
		<< "-f's (" << opt_f << ")" << std::endl;
264
265
266
      exit(2);
    }

267
268
  if (opt_d)
    {
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
      switch (output)
	{
	case OutputLTL:
	  std::cout << "Use option -pL to set the following LTL priorities:"
		    << std::endl;
	  rf->dump_priorities(std::cout);
	  break;
	case OutputBool:
	  std::cout << "Use option -pB to set the following Boolean "
		    << "formula priorities:" << std::endl;
	  rf->dump_priorities(std::cout);
	  break;
	case OutputPSL:
	  std::cout << "Use option -pL to set the following LTL priorities:"
		    << std::endl;
	  rp->dump_priorities(std::cout);
	  // Fall through.
	case OutputSERE:
	  std::cout << "Use option -pS to set the following SERE priorities:"
		    << std::endl;
	  rs->dump_priorities(std::cout);
	  std::cout << "Use option -pB to set the following Boolean "
		    << "formula priorities:" << std::endl;
	  rs->rb.dump_priorities(std::cout);
	  break;
	}
295
296
297
    }
  else
    {
298
299
      std::set<std::string> unique;

300
301
      while (opt_F--)
	{
302
303
304
305
	  int max_tries_u = 1000;
	  while (max_tries_u--)
	    {
	      spot::srand(opt_s++);
306
	      spot::ltl::formula* f = 0;
307
308
309
	      int max_tries_r = 1000;
	      while (max_tries_r--)
		{
310
		  f = rf->generate(opt_f);
311
312
		  if (opt_r)
		    {
313
		      spot::ltl::formula* g = simp.simplify(f);
314
		      f->destroy();
315
316
		      if (spot::ltl::length(g) < opt_r)
			{
317
			  g->destroy();
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
			  continue;
			}
		      f = g;
		    }
		  else
		    {
		      assert(spot::ltl::length(f) <= opt_f);
		    }
		  break;
		}
	      if (max_tries_r < 0)
		{
		  assert(opt_r);
		  std::cerr << "Failed to generate non-reducible formula "
			    << "of size " << opt_r << " or more." << std::endl;
		  exit(2);
		}
335
336
	      std::string txt = spot::ltl::to_string(f, false,
						     output == OutputSERE);
337
	      f->destroy();
338
339
340
341
342
343
344
345
346
347
348
349
350
	      if (!opt_u || unique.insert(txt).second)
		{
		  std::cout << txt << std::endl;
		  break;
		}
	    }
	  if (max_tries_u < 0)
	    {
	      assert(opt_u);
	      std::cerr << "Failed to generate another unique formula."
			<< std::endl;
	      exit(2);
	    }
351
352
	}
    }
353

354
355
  delete rf;

356
357
358
359
360
  spot::ltl::atomic_prop_set::const_iterator i = ap->begin();
  while (i != ap->end())
    {
      spot::ltl::atomic_prop_set::const_iterator j = i;
      ++i;
361
      (*j)->destroy();
362
    }
363
364
  delete ap;
}