randomltl.cc 17.2 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
5
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
6
// Pierre et Marie Curie.
7 8 9 10 11
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13 14 15 16 17 18 19 20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22 23 24 25

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

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

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

58
      static const formula*
59 60 61 62 63 64 65
      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);
      }

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

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

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

90
      static const formula*
91 92 93 94 95 96 97
      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));
      }

98
      template <binop::type Op>
99
      static const formula*
100
      binop_builder(const random_formula* rl, int n)
101 102 103 104
      {
	assert(n >= 3);
	--n;
	int l = rrand(1, n - 1);
105 106 107 108 109 110 111 112
	// Force the order of generation of operands to be right, then
	// left.  This is historical, because gcc evaluates argument
	// from right to left and we used to make the two calls to
	// generate() inside of the call to instance() before
	// discovering that clang would perform the nested calls from
	// left to right.
	auto right = rl->generate(n - l);
	return binop::instance(Op, rl->generate(l), right);
113 114
      }

115
      template <binop::type Op>
116
      static const formula*
117 118 119 120 121 122
      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);
123 124 125
	// See comment in binop_builder.
	auto right = rl->generate(n - l);
	return binop::instance(Op, rp->rs.generate(l), right);
126 127 128
      }

      template <bunop::type Op>
129
      static const formula*
130 131 132 133 134 135 136
      bunop_unbounded_builder(const random_formula* rl, int n)
      {
	assert(n >= 2);
	return bunop::instance(Op, rl->generate(n - 1));
      }

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

      template <bunop::type Op>
147
      static const formula*
148 149 150
      bunop_bool_bounded_builder(const random_formula* rl, int n)
      {
	assert(n >= 2);
151 152
	int min = rrand(0, 2);
	int max = rrand(min, 3);
153 154 155 156 157
	const random_sere* rp = static_cast<const random_sere*>(rl);
	return bunop::instance(Op, rp->rb.generate(n - 1), min, max);
      }


158
      template <multop::type Op>
159
      static const formula*
160
      multop_builder(const random_formula* rl, int n)
161 162 163 164
      {
	assert(n >= 3);
	--n;
	int l = rrand(1, n - 1);
165 166 167
	// See comment in binop_builder.
	auto right = rl->generate(n - l);
	return multop::instance(Op, rl->generate(l), right);
168 169 170 171 172
      }

    } // anonymous

    void
173
    random_formula::op_proba::setup(const char* name, int min_n, builder build)
174 175 176 177 178 179 180 181
    {
      this->name = name;
      this->min_n = min_n;
      this->proba = 1.0;
      this->build = build;
    }

    void
182
    random_formula::update_sums()
183 184 185 186
    {
      total_1_ = 0.0;
      total_2_ = 0.0;
      total_2_and_more_ = 0.0;
187
      for (unsigned i = 0; i < proba_size_; ++i)
188 189
	{
	  if (proba_[i].min_n == 1)
190 191 192
	    {
	      total_1_ += proba_[i].proba;
	      if (proba_ + i >= proba_2_)
193
		total_2_ += proba_[i].proba;
194 195 196
	      if (proba_ + i >= proba_2_or_more_)
		total_2_and_more_ += proba_[i].proba;
	    }
197
	  else if (proba_[i].min_n == 2)
198 199 200 201 202
	    {
	      total_2_ += proba_[i].proba;
	      if (proba_ + i >= proba_2_or_more_)
		  total_2_and_more_ += proba_[i].proba;
	    }
203 204 205
	  else if (proba_[i].min_n > 2)
	    total_2_and_more_ += proba_[i].proba;
	  else
206
	    SPOT_UNREACHABLE(); // unexpected max_n
207
	}
208
      assert(total_2_and_more_ >= total_2_);
209 210
    }

211
    const formula*
212
    random_formula::generate(int n) const
213 214
    {
      assert(n > 0);
215 216 217 218

      double r = drand();
      op_proba* p;

219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
      // Approximate impossible cases.
      if (n == 1 && total_1_ == 0.0)
	{
	  if (total_2_ != 0.0)
	    n = 2;
	  else
	    n = 3;
	}
      else if (n == 2 && total_2_ == 0.0)
	{
	  if (total_1_ != 0.0)
	    n = 1;
	  else
	    n = 3;
	}
      else if (n > 2 && total_2_and_more_ == 0.0)
	{
	  if (total_1_ != 0.0)
	    n = 1;
	  else
	    assert(total_2_ == 0.0);
	}


243 244
      if (n == 1)
	{
245 246
	  r *= total_1_;
	  p = proba_;
247 248 249
	}
      else if (n == 2)
	{
250 251
	  r *= total_2_;
	  p = proba_2_;
252 253 254
	}
      else
	{
255 256 257 258 259 260 261 262 263
	  r *= total_2_and_more_;
	  p = proba_2_or_more_;
	}

      double s = p->proba;
      while (s < r)
	{
	  ++p;
	  s += p->proba;
264
	}
265 266

      return p->build(this, n);
267 268 269
    }

    const char*
270
    random_formula::parse_options(char* options)
271
    {
272 273
      if (!options)
        return nullptr;
274 275 276 277 278 279 280 281 282 283 284 285
      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;

286 287
	  unsigned i;
	  for (i = 0; i < proba_size_; ++i)
288 289 290 291 292 293 294 295 296
	    {
	      if (('a' <= *proba_[i].name && *proba_[i].name <= 'z'
		   && !strcasecmp(proba_[i].name, key))
		  || !strcmp(proba_[i].name, key))
		{
		  proba_[i].proba = res;
		  break;
		}
	    }
297
	  if (i == proba_size_)
298 299 300 301 302 303 304 305 306
	    return key;

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

    std::ostream&
307
    random_formula::dump_priorities(std::ostream& os) const
308
    {
309
      for (unsigned i = 0; i < proba_size_; ++i)
310
	os << proba_[i].name << '\t' << proba_[i].proba << '\n';
311 312 313
      return os;
    }

314 315
    // SEREs
    random_sere::random_sere(const atomic_prop_set* ap)
316
      : random_formula(11, ap), rb(ap)
317 318 319 320 321 322 323
    {
      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>);
324 325 326 327 328 329 330
      proba_[4].setup("fstar",   2, bunop_unbounded_builder<bunop::FStar>);
      proba_[5].setup("fstar_b", 2, bunop_bounded_builder<bunop::FStar>);
      proba_[6].setup("and",     3, multop_builder<multop::AndRat>);
      proba_[7].setup("andNLM",  3, multop_builder<multop::AndNLM>);
      proba_[8].setup("or",      3, multop_builder<multop::OrRat>);
      proba_[9].setup("concat",  3, multop_builder<multop::Concat>);
      proba_[10].setup("fusion",  3, multop_builder<multop::Fusion>);
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
      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_()
357 358
    {
      proba_[0].setup("ap",      1, ap_builder);
359
      proba_[0].proba = ap_->size();
360 361
      proba_[1].setup("false",   1, false_builder);
      proba_[2].setup("true",    1, true_builder);
362
      proba_2_or_more_ = proba_2_ = proba_ + 3;
363 364 365 366 367 368 369 370 371 372 373 374 375
      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>);
376
    }
377

378 379 380 381 382 383 384 385 386 387 388 389 390 391
    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.
    }
392

393 394 395 396 397 398 399 400 401 402 403
    // 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>);
404 405
      update_sums();
    }
406

407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624
    void
    randltlgenerator::construct(atomic_prop_set aprops, option_map& opts,
                                       char* opt_pL,
                                       char* opt_pS,
                                       char* opt_pB)

    {
      aprops_ = aprops;
      output_ = opts.get("output", OUTPUTLTL);
      opt_seed_ = opts.get("seed", 0);
      opt_tree_size_min_ = opts.get("tree_size_min", 15);
      opt_tree_size_max_ = opts.get("tree_size_max", 15);
      opt_unique_ = opts.get("unique", true);
      opt_wf_ = opts.get("wf", false);
      opt_simpl_level_ = opts.get("simplification_level", 3);

      const char* tok_pL = 0;
      const char* tok_pS = 0;
      const char* tok_pB = 0;

      switch (output_)
        {
        case OUTPUTLTL:
          rf_ = new random_ltl(&aprops_);
          if (opt_pS)
            throw std::invalid_argument("Cannot set sere priorities with "\
                                        "LTL output");
          if (opt_pB)
            throw std::invalid_argument("Cannot set boolean priorities with "\
                                        "LTL output");
          tok_pL = rf_->parse_options(opt_pL);
          break;
        case OUTPUTBOOL:
          rf_ = new random_boolean(&aprops_);
          tok_pB = rf_->parse_options(opt_pB);
          if (opt_pL)
            throw std::invalid_argument("Cannot set ltl priorities with "\
                                        "Boolean output");
          if (opt_pS)
            throw std::invalid_argument("Cannot set sere priorities "\
                                        "with Boolean output");
          break;
        case OUTPUTSERE:
          rf_ = rs_ = new random_sere(&aprops_);
          tok_pS = rs_->parse_options(opt_pS);
          tok_pB = rs_->rb.parse_options(opt_pB);
          if (opt_pL)
            throw std::invalid_argument("Cannot set ltl priorities "\
                                        "with SERE output");
          break;
        case OUTPUTPSL:
          rf_ = rp_ = new 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)
        throw("failed to parse LTL priorities near '" + std::string(tok_pL));
      if (tok_pS)
        throw("failed to parse SERE priorities near " + std::string(tok_pS));
      if (tok_pB)
        throw("failed to parse Boolean priorities near "
              + std::string(tok_pB));

      spot::srand(opt_seed_);
      ltl_simplifier_options simpl_opts(opt_simpl_level_);
      ltl_simplifier simpl_(simpl_opts);
    }

    randltlgenerator::randltlgenerator(int aprops_n, option_map& opts,
                                       char* opt_pL,
                                       char* opt_pS,
                                       char* opt_pB)
      {
        atomic_prop_set aprops_;
        default_environment& e =
        default_environment::instance();
        for (int i = 0; i < aprops_n; ++i)
          {
            std::ostringstream p;
            p << 'p' << i;
            aprops_.insert(static_cast<const atomic_prop*>
                           (e.require(p.str())));
          }
        construct(aprops_, opts, opt_pL, opt_pS, opt_pB);
      }

    randltlgenerator::randltlgenerator(atomic_prop_set aprops,
                                       option_map& opts,
                                       char* opt_pL,
                                       char* opt_pS,
                                       char* opt_pB)

    {
      construct(aprops, opts, opt_pL, opt_pS, opt_pB);
    }


    randltlgenerator::~randltlgenerator()
    {
      delete rf_;
      // Cleanup the unicity table.
      for (auto i: unique_set_)
        i->destroy();
    }
    const formula* randltlgenerator::next()
    {
      unsigned trials = MAX_TRIALS;
      bool ignore;
      const formula* f = nullptr;
      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);

          if (opt_wf_)
            {
              atomic_prop_set s = aprops_;
              remove_some_props(s);
              f = multop::instance(multop::And,
                                              f, GF_n());
            }

	  if (opt_simpl_level_)
	    {
	      const spot::ltl::formula* tmp = simpl_.simplify(f);
	      f->destroy();
	      f = tmp;
	    }

          if (opt_unique_)
            {
              if (unique_set_.insert(f).second)
                {
                  f->clone();
                }
              else
                {
		  ignore = true;
                  f->destroy();
                }
            }
        } while (ignore && --trials);
      if (trials <= 0)
        return nullptr;
      return f;
    }

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

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

    // GF(p_1) & GF(p_2) & ... & GF(p_n)
    const formula*
    randltlgenerator::GF_n()
    {
      const formula* res = 0;
      for (auto v: aprops_)
        {
          const formula* f =
          unop::instance(unop::F, v->clone());
          f = unop::instance(unop::G, f);
          if (res)
            res = multop::instance(multop::And, f, res);
          else
            res = f;
        }
      return res;
    }

    void
    randltlgenerator::dump_ltl_priorities(std::ostream& os)
      {
        rf_->dump_priorities(os);
      }

    void
    randltlgenerator::dump_bool_priorities(std::ostream& os)
      {
        rf_->dump_priorities(os);
      }

    void
    randltlgenerator::dump_psl_priorities(std::ostream& os)
      {
        rp_->dump_priorities(os);
      }

    void
    randltlgenerator::dump_sere_priorities(std::ostream& os)
      {
        rs_->dump_priorities(os);
      }

    void
    randltlgenerator::dump_sere_bool_priorities(std::ostream& os)
      {
        rs_->rb.dump_priorities(os);
      }
  }
}