modelcheck.cc 19.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011-2020 Laboratoire de Recherche et Developpement
3
// 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 "config.h"
21 22 23 24
#include "bin/common_conv.hh"
#include "bin/common_setup.hh"
#include "bin/common_output.hh"

25
#include <spot/ltsmin/ltsmin.hh>
26
#include <spot/ltsmin/spins_kripke.hh>
27
#include <spot/mc/mc_instanciator.hh>
28 29 30 31 32 33
#include <spot/twaalgos/dot.hh>
#include <spot/tl/defaultenv.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/emptiness.hh>
#include <spot/twaalgos/postproc.hh>
Antoine Martin's avatar
Antoine Martin committed
34
#include <spot/twaalgos/degen.hh>
35
#include <spot/twaalgos/are_isomorphic.hh>
36 37 38
#include <spot/twa/twaproduct.hh>
#include <spot/misc/timer.hh>
#include <spot/misc/memusage.hh>
39
#include <cstring>
40 41
#include <spot/kripke/kripkegraph.hh>
#include <spot/twaalgos/hoa.hh>
42

43
#include <algorithm>
44 45 46 47
#include <thread>
#include <spot/twacube/twacube.hh>
#include <spot/twacube_algos/convert.hh>

48 49 50 51 52 53 54
const char argp_program_doc[] =
"Process model and formula to check wether a "
"model meets a specification.\v\
Exit status:\n\
  0  No counterexample found\n\
  1  A counterexample has been found\n\
  2  Errors occurs during processing";
55

56
const unsigned DOT_MODEL = 1;
57 58 59 60
const unsigned HOA_MODEL = 2;
const unsigned DOT_PRODUCT = 4;
const unsigned DOT_FORMULA = 8;
const unsigned CSV = 16;
61

62 63 64 65
// Handle all options specified in the command line
struct mc_options_
{
  bool compute_counterexample = false;
66
  unsigned output = 0;
67 68 69 70 71
  bool is_empty = false;
  char* formula = nullptr;
  char* model = nullptr;
  bool selfloopize = true;
  char* dead_ap = nullptr;
72
  bool use_timer = false;
73
  unsigned compress = 0;
74
  unsigned nb_threads = 1;
75
  bool csv = false;
76 77
  spot::mc_algorithm algorithm = spot::mc_algorithm::BLOEMEN_EC;
  bool force_parallel = false;
78
} mc_options;
79 80


81 82 83 84 85
static int
parse_opt_finput(int key, char* arg, struct argp_state*)
{
  // This switch is alphabetically-ordered.
  switch (key)
86
    {
87 88 89
    case CSV:
      mc_options.csv = true;
      break;
Antoine Martin's avatar
Antoine Martin committed
90
    case 'B':
91 92
      mc_options.algorithm = spot::mc_algorithm::BLOEMEN_EC;
      mc_options.force_parallel = true;
Antoine Martin's avatar
Antoine Martin committed
93
      break;
94
    case 'b':
95 96 97
      // FIXME Differenciate  bloemen and bloemen_ec: -b/-B is not enough
      mc_options.algorithm = spot::mc_algorithm::BLOEMEN_SCC;
      mc_options.force_parallel = true;
98
      break;
99 100 101
    case 'c':
      mc_options.compute_counterexample = true;
      break;
Antoine Martin's avatar
Antoine Martin committed
102
    case 'C':
103 104
      mc_options.algorithm = spot::mc_algorithm::CNDFS;
      mc_options.force_parallel = true;
Antoine Martin's avatar
Antoine Martin committed
105
      break;
106 107
    case 'd':
      if (strcmp(arg, "model") == 0)
108
        mc_options.output |= DOT_MODEL;
109
      else if (strcmp(arg, "product") == 0)
110
        mc_options.output |= DOT_PRODUCT;
111
      else if (strcmp(arg, "formula") == 0)
112
        mc_options.output |= DOT_FORMULA;
113
      else
114 115 116 117 118
        {
          std::cerr << "Unknown argument: '" << arg
                    << "' for option --dot\n";
          return ARGP_ERR_UNKNOWN;
        }
119 120 121 122 123 124 125
      break;
    case 'e':
      mc_options.is_empty = true;
      break;
    case 'f':
      mc_options.formula = arg;
      break;
126
    case 'h':
127 128
      mc_options.algorithm = spot::mc_algorithm::DEADLOCK;
      mc_options.force_parallel = true;
129 130
      mc_options.selfloopize = false;
      break;
131 132 133
    case 'm':
      mc_options.model = arg;
      break;
134 135 136
    case 'k':
      mc_options.output |= HOA_MODEL;
      break;
137
    case 'p':
138
      mc_options.nb_threads = to_unsigned(arg, "-p/--parallel");
139
      mc_options.force_parallel = true;
140
      break;
141 142 143 144
    case 'r':
      mc_options.algorithm = spot::mc_algorithm::REACHABILITY;
      mc_options.force_parallel = true;
      break;
145 146 147 148 149 150
    case 's':
      mc_options.dead_ap = arg;
      break;
    case 't':
      mc_options.use_timer = true;
      break;
151 152 153 154
    case 'w':
      mc_options.algorithm = spot::mc_algorithm::SWARMING;
      mc_options.force_parallel = true;
      break;
155
    case 'z':
156
      mc_options.compress = to_unsigned(arg, "-z/--compress");
157 158 159
      break;
    default:
      return ARGP_ERR_UNKNOWN;
160
    }
161 162
  return 0;
}
163

164 165 166 167 168 169 170 171 172 173
static const argp_option options[] =
  {
    // Keep each section sorted
    // ------------------------------------------------------------
    { nullptr, 0, nullptr, 0, "Input options:", 1 },
    { "formula", 'f', "STRING", 0, "use the formula STRING", 0 },
    // FIXME do we want support for reading more than one formula?
    { "model", 'm', "STRING", 0, "use  the model stored in file STRING", 0 },
    // ------------------------------------------------------------
    { nullptr, 0, nullptr, 0, "Process options:", 2 },
Antoine Martin's avatar
Antoine Martin committed
174
    { "bloemen-ec", 'B', nullptr, 0,
175 176
      "run the emptiness-check of Bloemen et al.  (HVC'16). Return 1 "
      "if a counterexample is found.", 0},
177
    { "bloemen", 'b', nullptr, 0,
178 179
      "run the SCC computation of Bloemen et al. (PPOPP'16). Return 1 "
      "if a counterexample is found.", 0 },
Antoine Martin's avatar
Antoine Martin committed
180
    { "cndfs", 'C', nullptr, 0,
181 182
      "run the emptiness check of Evangelista et al. (ATVA'12). Return 1 "
      "if a counterexample is found.", 0 },
183 184
    { "counterexample", 'c', nullptr, 0,
      "compute an accepting counterexample (if it exists)", 0 },
185 186 187 188
    { "has-deadlock", 'h', nullptr, 0,
      "check if the model has a deadlock. "
      "Return 1 if the model contains a deadlock."
      , 0 },
189 190 191 192 193
    { "is-empty", 'e', nullptr, 0,
      "check if the model meets its specification. Uses Cou99 in sequential "
      "and bloemen-ec in pallel (option -p). Return 1 if a counterexample "
      "is found."
      , 0 },
194
    { "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 },
195 196
    { "reachability", 'r', nullptr, 0, "performs a traversal of the model "
      , 0 },
197 198 199
    { "selfloopize", 's', "STRING", 0,
      "use STRING as property for marking deadlock "
      "states (by default selfloopize is activated with STRING='true')", 0 },
200 201 202 203
    { "swarming", 'w', nullptr, 0,
      "run the technique of of Holzmann et al. (IEEE'11) with the emptiness-"
      "check of Renault et al. (LPAR'13). Returns 1 if a counterexample "
      "is found.", 0 },
204 205 206 207
    { "timer", 't', nullptr, 0,
      "time the different phases of the execution", 0 },
    // ------------------------------------------------------------
    { nullptr, 0, nullptr, 0, "Output options:", 3 },
208 209
    { "csv", CSV, nullptr, 0,
      "output a CSV containing interesting values", 0 },
210 211
    { "dot", 'd', "[model|product|formula]", 0,
      "output the associated automaton in dot format", 0 },
212 213
    { "kripke", 'k', nullptr, 0,
      "output the model state-space in Kripke format", 0 },
214 215 216 217 218 219 220 221 222 223 224
    // ------------------------------------------------------------
    { nullptr, 0, nullptr, 0, "Optimization options:", 4 },
    { "compress", 'z', "INT", 0, "specify the level of compression\n"
      "1 : handle large models\n"
      "2 : (faster) assume all values in [0 .. 2^28-1]", 0 },
    // ------------------------------------------------------------
    { nullptr, 0, nullptr, 0, "General options:", 5 },
    { nullptr, 0, nullptr, 0, nullptr, 0 }
  };

const struct argp finput_argp = { options, parse_opt_finput,
225 226
                                  nullptr, nullptr, nullptr,
                                  nullptr, nullptr };
227 228 229 230 231 232 233

const struct argp_child children[] =
  {
    { &finput_argp, 0, nullptr, 1 },
    { &misc_argp, 0, nullptr, -1 },
    { nullptr, 0, nullptr, 0 }
  };
234

235
static std::string split_filename(const std::string& str) {
236 237 238 239
  unsigned found = str.find_last_of("/");
  return str.substr(found+1);
}

240 241
static int checked_main()
{
242
  spot::default_environment& env = spot::default_environment::instance();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
243
  spot::atomic_prop_set ap;
244
  auto dict = spot::make_bdd_dict();
245
  spot::const_kripke_ptr model = nullptr;
246
  spot::const_twa_graph_ptr prop = nullptr;
247
  spot::const_twa_ptr product = nullptr;
248
  spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
249
  int exit_code = 0;
250
  spot::postprocessor post;
251
  spot::formula deadf = spot::formula::tt();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
252
  spot::formula f = nullptr;
253
  spot::timer_map tm;
254

255
  if (mc_options.selfloopize)
256
    {
257
      if (mc_options.dead_ap == nullptr ||
258 259
          !strcasecmp(mc_options.dead_ap, "true"))
        deadf = spot::formula::tt();
260
      else if (!strcasecmp(mc_options.dead_ap, "false"))
261
        deadf = spot::formula::ff();
262
      else
263
        deadf = env.require(mc_options.dead_ap);
264
    }
265

266 267 268 269
  if (mc_options.formula != nullptr)
    {
      tm.start("parsing formula");
      {
270 271 272
        auto pf = spot::parse_infix_psl(mc_options.formula, env, false);
        exit_code = pf.format_errors(std::cerr);
        f = pf.f;
273 274
      }
      tm.stop("parsing formula");
275

276 277
      tm.start("translating formula");
      {
278 279 280 281
        spot::translator trans(dict);
        // if (deterministic) FIXME
        //   trans.set_pref(spot::postprocessor::Deterministic);
        prop = trans.run(&f);
282 283
      }
      tm.stop("translating formula");
284

285
      atomic_prop_collect(f, &ap);
286

287
      if (mc_options.output & DOT_FORMULA)
288 289 290 291 292
        {
          tm.start("dot output");
          spot::print_dot(std::cout, prop);
          tm.stop("dot output");
        }
293
    }
294

295
  if (mc_options.model != nullptr)
296
    {
297
      tm.start("loading ltsmin model");
298
      try
299 300 301 302
        {
          model = spot::ltsmin_model::load(mc_options.model)
            .kripke(&ap, dict, deadf, mc_options.compress);
        }
303
      catch (const std::runtime_error& e)
304 305 306
        {
          std::cerr << e.what() << '\n';
        }
307
      tm.stop("loading ltsmin model");
308 309

      if (!model)
310 311 312 313
        {
          exit_code = 2;
          goto safe_exit;
        }
314

315
      if (mc_options.output & DOT_MODEL)
316 317 318 319 320
        {
          tm.start("dot output");
          spot::print_dot(std::cout, model);
          tm.stop("dot output");
        }
321 322 323 324 325 326 327 328

      if (mc_options.output & HOA_MODEL)
        {
          tm.start("kripke output");
          spot::print_hoa(std::cout, model);
          tm.stop("kripke output");
          goto safe_exit;
        }
329 330
    }

331
  if (mc_options.force_parallel == false &&
332
      mc_options.formula != nullptr &&
333
      mc_options.model != nullptr)
334
    {
335 336
      std::cout << "Warning : using sequential algorithms (BDD-based)\n\n";

337 338 339
      product = spot::otf_product(model, prop);

      if (mc_options.is_empty)
340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359
        {
          const char* err;
          echeck_inst = spot::make_emptiness_check_instantiator("Cou99", &err);
          if (!echeck_inst)
            {
              std::cerr << "Unknown emptiness check algorihm `"
                        << err <<  "'\n";
              exit_code = 1;
              goto safe_exit;
            }

          auto ec = echeck_inst->instantiate(product);
          assert(ec);
          int memused = spot::memusage();
          tm.start("running emptiness check");
          spot::emptiness_check_result_ptr res;
          try
            {
              res = ec->check();
            }
360
          catch (const std::bad_alloc&)
361
          {
362
            std::cerr << "Out of memory during emptiness check.\n";
363
            if (!mc_options.compress)
364
              std::cerr << "Try option -z for state compression.\n";
365 366 367 368 369 370 371 372 373 374 375 376
            exit_code = 2;
            exit(exit_code);
          }
        tm.stop("running emptiness check");
        memused = spot::memusage() - memused;

        ec->print_stats(std::cout);
        std::cout << memused << " pages allocated for emptiness check"
                  << std::endl;

        if (!res)
          {
377
            std::cout << "no accepting run found" << std::endl;
378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393
          }
        else if (!mc_options.compute_counterexample)
          {
            std::cout << "an accepting run exists "
                      << "(use -c to print it)" << std::endl;
            exit_code = 1;
          }
        else
          {
            exit_code = 1;
            spot::twa_run_ptr run;
            tm.start("computing accepting run");
            try
              {
                run = res->accepting_run();
              }
394
            catch (const std::bad_alloc&)
395
              {
396 397
                std::cerr
                  << "Out of memory while looking for counterexample.\n";
398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416
                exit_code = 2;
                exit(exit_code);
              }
            tm.stop("computing accepting run");

            if (!run)
              {
                std::cout << "an accepting run exists" << std::endl;
              }
            else
              {
                tm.start("reducing accepting run");
                run = run->reduce();
                tm.stop("reducing accepting run");
                tm.start("printing accepting run");
                std::cout << *run;
                tm.stop("printing accepting run");
              }
          }
417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433

        if (mc_options.csv)
          {
            std::cout << "\nFind following the csv: "
                      << "model,formula,walltimems,memused,type,"
                      << "states,transitions\n";
            std::cout << '#'
                      << split_filename(mc_options.model)
                      << ','
                      << mc_options.formula << ','
                      << tm.timer("running emptiness check").walltime() << ','
                      << memused << ','
                      << (!res ? "EMPTY," : "NONEMPTY,")
                      << ec->statistics()->get("states") << ','
                      << ec->statistics()->get("transitions")
                      << std::endl;
          }
434
        }
435

436
      if (mc_options.output & DOT_PRODUCT)
437 438 439 440 441
        {
          tm.start("dot output");
          spot::print_dot(std::cout, product);
          tm.stop("dot output");
        }
442
    }
443
  else if (mc_options.force_parallel && mc_options.model != nullptr)
444
    {
445
      std::cout << "Warning : using parallel algorithms (CUBE-based)\n\n";
446

447
      if (mc_options.output & DOT_PRODUCT)
448
        {
449 450 451
          std::cerr << "\nERROR: Parallel algorithm doesn't support DOT"
            " output  for the synchronous product.\n"
            "       Please consider removing '-p' option\n";
452 453 454 455 456 457 458 459 460
          exit_code = 2;
          goto safe_exit;
        }

      if (mc_options.output & HOA_MODEL)
        {
          std::cerr << "\nERROR: Parallel algorithm doesn't support HOA"
            " output  for the synchronous product.\n"
            "       Please consider removing '-p' option\n";
461 462 463 464
          exit_code = 2;
          goto safe_exit;
        }

465 466 467 468
      if (prop == nullptr &&
          (mc_options.algorithm == spot::mc_algorithm::CNDFS ||
           mc_options.algorithm == spot::mc_algorithm::BLOEMEN_EC ||
           mc_options.algorithm == spot::mc_algorithm::SWARMING))
469
        {
470 471
          std::cerr << "\nERROR: Algorithm " << mc_options.algorithm
                    << " requires to provide a formula (--formula)\n";
472 473 474 475
          exit_code = 2;
          goto safe_exit;
        }

Antoine Martin's avatar
Antoine Martin committed
476 477 478 479 480 481
      unsigned int hc = std::thread::hardware_concurrency();
      if (mc_options.nb_threads > hc)
        std::cerr << "Warning: you require " << mc_options.nb_threads
                  << " threads, but your computer only support " << hc
                  << ". This could slow down parallel algorithms.\n";

482 483 484 485 486 487 488 489
      auto prop_degen = prop;
      if (mc_options.algorithm == spot::mc_algorithm::CNDFS)
        {
          // Only support Single Acceptance Conditions
          tm.start("degeneralize");
          prop_degen = spot::degeneralize_tba(prop);
          tm.stop("degeneralize");
        }
Antoine Martin's avatar
Antoine Martin committed
490 491 492 493 494 495 496 497 498

      tm.start("twa to twacube");
      auto propcube = spot::twa_to_twacube(prop_degen);
      tm.stop("twa to twacube");

      tm.start("load kripkecube");
      spot::ltsmin_kripkecube_ptr modelcube = nullptr;
      try
        {
499 500
          std::vector<std::string> aps = {};
          if (propcube != nullptr)
Etienne Renault's avatar
Etienne Renault committed
501
            aps = propcube->ap();
502

Antoine Martin's avatar
Antoine Martin committed
503
          modelcube = spot::ltsmin_model::load(mc_options.model)
504
            .kripkecube(aps, deadf, mc_options.compress, mc_options.nb_threads);
Antoine Martin's avatar
Antoine Martin committed
505 506 507 508 509 510 511 512
        }
      catch (const std::runtime_error& e)
        {
          std::cerr << e.what() << '\n';
        }
      tm.stop("load kripkecube");

      int memused = spot::memusage();
513 514 515 516 517 518 519 520 521 522
      tm.start("exploration");

      auto result =
        spot::ec_instanciator<spot::ltsmin_kripkecube_ptr, spot::cspins_state,
                              spot::cspins_iterator, spot::cspins_state_hash,
                              spot::cspins_state_equal>
        (mc_options.algorithm, modelcube, propcube,
         mc_options.compute_counterexample);

      tm.stop("exploration");
Antoine Martin's avatar
Antoine Martin committed
523 524 525 526 527 528 529 530 531
      memused = spot::memusage() - memused;

      if (!modelcube)
        {
          exit_code = 2;
          goto safe_exit;
        }

      // Display statistics
532 533 534 535
      std::cout << result << '\n';
      std::cout << memused << " pages allocated for "
                << mc_options.algorithm << '\n';

Antoine Martin's avatar
Antoine Martin committed
536 537 538 539

      if (mc_options.csv)
        {
          std::cout << "\nSummary :\n";
540 541 542 543 544 545 546 547
          auto rval = result.value[0];
          std::for_each(result.value.rbegin(), result.value.rend(),
                        [&](spot::mc_rvalue n) { rval = rval | n; });

          if (rval == spot::mc_rvalue::NO_DEADLOCK ||
              rval == spot::mc_rvalue::EMPTY ||
              rval == spot::mc_rvalue::SUCCESS)
            std::cout << "no accepting run / counterexample found\n";
Antoine Martin's avatar
Antoine Martin committed
548 549 550 551 552 553 554
          else if (!mc_options.compute_counterexample)
            {
              std::cout << "an accepting run exists "
                        << "(use -c to print it)" << std::endl;
              exit_code = 1;
            }
          else
555
            std::cout << "an accepting run exists\n" <<  result.trace << '\n';
Antoine Martin's avatar
Antoine Martin committed
556

557

558
          // Grab The informations to display into the CSV
559 560 561 562 563 564 565 566 567 568 569 570
          unsigned c_states = 0;
          unsigned c_trans = 0;
          int c_sccs = 0; // not unsigned since it can be negative
          unsigned walltime = 0;
          for (unsigned i = 0; i < result.finisher.size(); ++i)
            {
              if (result.finisher[i])
                walltime = result.walltime[i];
              c_states += result.states[i];
              c_trans += result.transitions[i];
              c_sccs += result.sccs[i];
            }
571 572

          std::cout << "Find following the csv: "
573
                    << "model,formula,walltimems,memused,type,"
574
                    << "cumul_states,cumul_transitions,cumul_sccs\n";
575
          std::cout << '#'
576 577 578 579 580
                    << split_filename(mc_options.model) << ',';

          if (mc_options.formula != nullptr)
            std::cout << mc_options.formula;

581 582 583
          std::cout << ',' << walltime << ',' << memused << ','
                    << rval << ',' << c_states << ',' << c_trans << ','
                    << (c_sccs < 0 ? -1 : c_sccs) << '\n';
584
        }
585
    }
Antoine Martin's avatar
Antoine Martin committed
586

587
 safe_exit:
588
  if (mc_options.use_timer)
589
    tm.print(std::cout);
590
  tm.reset_all();                // This helps valgrind.
591 592
  return exit_code;
}
593

594
int
595
main(int argc, char** argv)
596
{
597 598
  setup(argv);
  const argp ap = { nullptr, nullptr, nullptr,
599
                    argp_program_doc, children, nullptr, nullptr };
600 601 602 603 604

  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
    exit(err);

  auto exit_code = checked_main();
605 606

  // Additional checks to debug reference counts in formulas.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
607
  assert(spot::fnode::instances_check());
608
  exit(exit_code);
609
}