randomltl.cc 10 KB
Newer Older
1
2
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
3
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
4
5
// (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
24
25
26
//
// 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.

#include <cassert>
#include <algorithm>
#include "randomltl.hh"
27
#include "ltlast/allnodes.hh"
28
29
#include "misc/random.hh"
#include <iostream>
30
#include <cstring>
31
32
33
34
35
36
37

namespace spot
{
  namespace ltl
  {
    namespace
    {
38
      static formula*
39
      ap_builder(const random_formula* rl, int n)
40
41
42
43
44
      {
	assert(n == 1);
	(void) n;
	atomic_prop_set::const_iterator i = rl->ap()->begin();
	std::advance(i, mrand(rl->ap()->size()));
45
	return (*i)->clone();
46
47
      }

48
      static formula*
49
      true_builder(const random_formula*, int n)
50
51
52
53
54
55
      {
	assert(n == 1);
	(void) n;
	return constant::true_instance();
      }

56
57
58
59
60
61
62
63
64
      static formula*
      boolform_builder(const random_formula* rl, int n)
      {
	assert(n >= 1);
	const random_sere* rs = static_cast<const random_sere*>(rl);
	return rs->rb.generate(n);
      }

      static formula*
65
      false_builder(const random_formula*, int n)
66
67
68
69
70
71
      {
	assert(n == 1);
	(void) n;
	return constant::false_instance();
      }

72
73
74
75
76
77
78
79
      static formula*
      eword_builder(const random_formula*, int n)
      {
	assert(n == 1);
	(void) n;
	return constant::empty_word_instance();
      }

80
      template <unop::type Op>
81
      static formula*
82
      unop_builder(const random_formula* rl, int n)
83
84
85
86
87
      {
	assert(n >= 2);
	return unop::instance(Op, rl->generate(n - 1));
      }

88
89
90
91
92
93
94
95
      static formula*
      closure_builder(const random_formula* rl, int n)
      {
	assert(n >= 2);
	const random_psl* rp = static_cast<const random_psl*>(rl);
	return unop::instance(unop::Closure, rp->rs.generate(n - 1));
      }

96
      template <binop::type Op>
97
      static formula*
98
      binop_builder(const random_formula* rl, int n)
99
100
101
102
103
104
105
      {
	assert(n >= 3);
	--n;
	int l = rrand(1, n - 1);
	return binop::instance(Op, rl->generate(l), rl->generate(n - l));
      }

106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
      template <binop::type Op>
      static formula*
      binop_SERELTL_builder(const random_formula* rl, int n)
      {
	assert(n >= 3);
	--n;
	const random_psl* rp = static_cast<const random_psl*>(rl);
	int l = rrand(1, n - 1);
	return binop::instance(Op, rp->rs.generate(l), rl->generate(n - l));
      }

      template <bunop::type Op>
      static formula*
      bunop_unbounded_builder(const random_formula* rl, int n)
      {
	assert(n >= 2);
	return bunop::instance(Op, rl->generate(n - 1));
      }

      template <bunop::type Op>
      static formula*
      bunop_bounded_builder(const random_formula* rl, int n)
      {
	assert(n >= 2);
130
131
	int min = rrand(0, 2);
	int max = rrand(min, 3);
132
133
134
135
136
137
138
139
	return bunop::instance(Op, rl->generate(n - 1), min, max);
      }

      template <bunop::type Op>
      static formula*
      bunop_bool_bounded_builder(const random_formula* rl, int n)
      {
	assert(n >= 2);
140
141
	int min = rrand(0, 2);
	int max = rrand(min, 3);
142
143
144
145
146
	const random_sere* rp = static_cast<const random_sere*>(rl);
	return bunop::instance(Op, rp->rb.generate(n - 1), min, max);
      }


147
      template <multop::type Op>
148
      static formula*
149
      multop_builder(const random_formula* rl, int n)
150
151
152
153
154
155
156
157
158
159
      {
	assert(n >= 3);
	--n;
	int l = rrand(1, n - 1);
	return multop::instance(Op, rl->generate(l), rl->generate(n - l));
      }

    } // anonymous

    void
160
    random_formula::op_proba::setup(const char* name, int min_n, builder build)
161
162
163
164
165
166
167
168
    {
      this->name = name;
      this->min_n = min_n;
      this->proba = 1.0;
      this->build = build;
    }

    void
169
    random_formula::update_sums()
170
171
172
173
    {
      total_1_ = 0.0;
      total_2_ = 0.0;
      total_2_and_more_ = 0.0;
174
      for (unsigned i = 0; i < proba_size_; ++i)
175
176
	{
	  if (proba_[i].min_n == 1)
177
178
179
	    {
	      total_1_ += proba_[i].proba;
	      if (proba_ + i >= proba_2_)
180
		total_2_ += proba_[i].proba;
181
182
183
	      if (proba_ + i >= proba_2_or_more_)
		total_2_and_more_ += proba_[i].proba;
	    }
184
	  else if (proba_[i].min_n == 2)
185
186
187
188
189
	    {
	      total_2_ += proba_[i].proba;
	      if (proba_ + i >= proba_2_or_more_)
		  total_2_and_more_ += proba_[i].proba;
	    }
190
191
192
	  else if (proba_[i].min_n > 2)
	    total_2_and_more_ += proba_[i].proba;
	  else
193
	    assert(!"unexpected max_n");
194
195
196
197
198
199
200
	}
      assert(total_1_ != 0.0);
      assert(total_2_ != 0.0);
      assert(total_2_and_more_ != 0.0);
    }

    formula*
201
    random_formula::generate(int n) const
202
203
    {
      assert(n > 0);
204
205
206
207

      double r = drand();
      op_proba* p;

208
209
      if (n == 1)
	{
210
211
	  r *= total_1_;
	  p = proba_;
212
213
214
	}
      else if (n == 2)
	{
215
216
	  r *= total_2_;
	  p = proba_2_;
217
218
219
	}
      else
	{
220
221
222
223
224
225
226
227
228
	  r *= total_2_and_more_;
	  p = proba_2_or_more_;
	}

      double s = p->proba;
      while (s < r)
	{
	  ++p;
	  s += p->proba;
229
	}
230
231

      return p->build(this, n);
232
233
234
    }

    const char*
235
    random_formula::parse_options(char* options)
236
237
238
239
240
241
242
243
244
245
246
247
248
    {
      char* key = strtok(options, "=\t, :;");
      while (key)
	{
	  char* value = strtok(0, "=\t, :;");
	  if (value == 0)
	    return key;

	  char* endptr;
	  double res = strtod(value, &endptr);
	  if (*endptr)
	    return value;

249
250
	  unsigned i;
	  for (i = 0; i < proba_size_; ++i)
251
252
253
254
255
256
257
258
259
	    {
	      if (('a' <= *proba_[i].name && *proba_[i].name <= 'z'
		   && !strcasecmp(proba_[i].name, key))
		  || !strcmp(proba_[i].name, key))
		{
		  proba_[i].proba = res;
		  break;
		}
	    }
260
	  if (i == proba_size_)
261
262
263
264
265
266
267
268
269
	    return key;

	  key = strtok(0, "=\t, :;");
	}
      update_sums();
      return 0;
    }

    std::ostream&
270
    random_formula::dump_priorities(std::ostream& os) const
271
    {
272
      for (unsigned i = 0; i < proba_size_; ++i)
273
274
275
276
	os << proba_[i].name << "\t" << proba_[i].proba << std::endl;
      return os;
    }

277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
    // SEREs
    random_sere::random_sere(const atomic_prop_set* ap)
      : random_formula(11, ap), rb(ap)
    {
      proba_[0].setup("eword",   1, eword_builder);
      proba_2_ = proba_ + 1;
      proba_2_or_more_ = proba_ + 1;
      proba_[1].setup("boolform", 1, boolform_builder);
      proba_[2].setup("star",    2, bunop_unbounded_builder<bunop::Star>);
      proba_[3].setup("star_b",  2, bunop_bounded_builder<bunop::Star>);
      proba_[4].setup("equal_b", 2, bunop_bool_bounded_builder<bunop::Equal>);
      proba_[5].setup("goto_b",  2, bunop_bool_bounded_builder<bunop::Goto>);
      proba_[6].setup("and",     3, multop_builder<multop::And>);
      proba_[7].setup("andNLM",  3, multop_builder<multop::AndNLM>);
      proba_[8].setup("or",      3, multop_builder<multop::Or>);
      proba_[9].setup("concat",  3, multop_builder<multop::Concat>);
      proba_[10].setup("fusion",  3, multop_builder<multop::Fusion>);
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
      update_sums();
    }

    // Boolean formulae
    random_boolean::random_boolean(const atomic_prop_set* ap)
      : random_formula(9, ap)
    {
      proba_[0].setup("ap",      1, ap_builder);
      proba_[0].proba = ap_->size();
      proba_[1].setup("false",   1, false_builder);
      proba_[2].setup("true",    1, true_builder);
      proba_2_or_more_ = proba_2_ = proba_ + 3;
      proba_[3].setup("not",     2, unop_builder<unop::Not>);
      proba_[4].setup("equiv",   3, binop_builder<binop::Equiv>);
      proba_[5].setup("implies", 3, binop_builder<binop::Implies>);
      proba_[6].setup("xor",     3, binop_builder<binop::Xor>);
      proba_[7].setup("and",     3, multop_builder<multop::And>);
      proba_[8].setup("or",      3, multop_builder<multop::Or>);

      update_sums();
    }

    // LTL formulae
    void
    random_ltl::setup_proba_()
320
321
    {
      proba_[0].setup("ap",      1, ap_builder);
322
      proba_[0].proba = ap_->size();
323
324
      proba_[1].setup("false",   1, false_builder);
      proba_[2].setup("true",    1, true_builder);
325
      proba_2_or_more_ = proba_2_ = proba_ + 3;
326
327
328
329
330
331
332
333
334
335
336
337
338
      proba_[3].setup("not",     2, unop_builder<unop::Not>);
      proba_[4].setup("F",       2, unop_builder<unop::F>);
      proba_[5].setup("G",       2, unop_builder<unop::G>);
      proba_[6].setup("X",       2, unop_builder<unop::X>);
      proba_[7].setup("equiv",   3, binop_builder<binop::Equiv>);
      proba_[8].setup("implies", 3, binop_builder<binop::Implies>);
      proba_[9].setup("xor",     3, binop_builder<binop::Xor>);
      proba_[10].setup("R",      3, binop_builder<binop::R>);
      proba_[11].setup("U",      3, binop_builder<binop::U>);
      proba_[12].setup("W",      3, binop_builder<binop::W>);
      proba_[13].setup("M",      3, binop_builder<binop::M>);
      proba_[14].setup("and",    3, multop_builder<multop::And>);
      proba_[15].setup("or",     3, multop_builder<multop::Or>);
339
    }
340

341
342
343
344
345
346
347
348
349
350
351
352
353
354
    random_ltl::random_ltl(const atomic_prop_set* ap)
      : random_formula(16, ap)
    {
      setup_proba_();
      update_sums();
    }

    random_ltl::random_ltl(int size, const atomic_prop_set* ap)
      : random_formula(size, ap)
    {
      setup_proba_();
      // No call to update_sums(), this functions is always
      // called by the random_psl constructor.
    }
355

356
357
358
359
360
361
362
363
364
365
366
    // PSL
    random_psl::random_psl(const atomic_prop_set* ap)
      : random_ltl(19, ap), rs(ap)
    {
      // FIXME: This looks very fragile.
      memmove(proba_ + 8, proba_ + 7,
	      ((proba_ + 16) - (proba_ + 7)) * sizeof(*proba_));

      proba_[7].setup("Closure", 2, closure_builder);
      proba_[17].setup("EConcat", 3, binop_SERELTL_builder<binop::EConcat>);
      proba_[18].setup("UConcat", 3, binop_SERELTL_builder<binop::UConcat>);
367
368
      update_sums();
    }
369

370
371
  } // ltl
} // spot