modelcheck.cc 18.7 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
57
58
59
const unsigned DOT_MODEL = 1;
const unsigned DOT_PRODUCT = 2;
const unsigned DOT_FORMULA = 4;
const unsigned CSV = 8;
60

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


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

156
157
158
159
160
161
162
163
164
165
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
166
    { "bloemen-ec", 'B', nullptr, 0,
167
168
      "run the emptiness-check of Bloemen et al.  (HVC'16). Return 1 "
      "if a counterexample is found.", 0},
169
    { "bloemen", 'b', nullptr, 0,
170
171
      "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
172
    { "cndfs", 'C', nullptr, 0,
173
174
      "run the emptiness check of Evangelista et al. (ATVA'12). Return 1 "
      "if a counterexample is found.", 0 },
175
176
    { "counterexample", 'c', nullptr, 0,
      "compute an accepting counterexample (if it exists)", 0 },
177
178
179
180
    { "has-deadlock", 'h', nullptr, 0,
      "check if the model has a deadlock. "
      "Return 1 if the model contains a deadlock."
      , 0 },
181
182
183
184
185
    { "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 },
186
    { "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 },
187
188
189
    { "selfloopize", 's', "STRING", 0,
      "use STRING as property for marking deadlock "
      "states (by default selfloopize is activated with STRING='true')", 0 },
190
191
192
193
    { "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 },
194
195
196
197
    { "timer", 't', nullptr, 0,
      "time the different phases of the execution", 0 },
    // ------------------------------------------------------------
    { nullptr, 0, nullptr, 0, "Output options:", 3 },
198
199
    { "csv", CSV, nullptr, 0,
      "output a CSV containing interesting values", 0 },
200
201
    { "dot", 'd', "[model|product|formula]", 0,
      "output the associated automaton in dot format", 0 },
202
203
204
205
206
207
208
209
210
211
212
    // ------------------------------------------------------------
    { 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,
213
214
                                  nullptr, nullptr, nullptr,
                                  nullptr, nullptr };
215
216
217
218
219
220
221

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

223
static std::string split_filename(const std::string& str) {
224
225
226
227
  unsigned found = str.find_last_of("/");
  return str.substr(found+1);
}

228
229
static int checked_main()
{
230
  spot::default_environment& env = spot::default_environment::instance();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
231
  spot::atomic_prop_set ap;
232
  auto dict = spot::make_bdd_dict();
233
  spot::const_kripke_ptr model = nullptr;
234
  spot::const_twa_graph_ptr prop = nullptr;
235
  spot::const_twa_ptr product = nullptr;
236
  spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
237
  int exit_code = 0;
238
  spot::postprocessor post;
239
  spot::formula deadf = spot::formula::tt();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240
  spot::formula f = nullptr;
241
  spot::timer_map tm;
242

243
  if (mc_options.selfloopize)
244
    {
245
      if (mc_options.dead_ap == nullptr ||
246
247
          !strcasecmp(mc_options.dead_ap, "true"))
        deadf = spot::formula::tt();
248
      else if (!strcasecmp(mc_options.dead_ap, "false"))
249
        deadf = spot::formula::ff();
250
      else
251
        deadf = env.require(mc_options.dead_ap);
252
    }
253

254
255
256
257
  if (mc_options.formula != nullptr)
    {
      tm.start("parsing formula");
      {
258
259
260
        auto pf = spot::parse_infix_psl(mc_options.formula, env, false);
        exit_code = pf.format_errors(std::cerr);
        f = pf.f;
261
262
      }
      tm.stop("parsing formula");
263

264
265
      tm.start("translating formula");
      {
266
267
268
269
        spot::translator trans(dict);
        // if (deterministic) FIXME
        //   trans.set_pref(spot::postprocessor::Deterministic);
        prop = trans.run(&f);
270
271
      }
      tm.stop("translating formula");
272

273
      atomic_prop_collect(f, &ap);
274

275
      if (mc_options.dot_output & DOT_FORMULA)
276
277
278
279
280
        {
          tm.start("dot output");
          spot::print_dot(std::cout, prop);
          tm.stop("dot output");
        }
281
    }
282

283
  if (mc_options.model != nullptr)
284
    {
285
      tm.start("loading ltsmin model");
286
      try
287
288
289
290
        {
          model = spot::ltsmin_model::load(mc_options.model)
            .kripke(&ap, dict, deadf, mc_options.compress);
        }
291
      catch (const std::runtime_error& e)
292
293
294
        {
          std::cerr << e.what() << '\n';
        }
295
      tm.stop("loading ltsmin model");
296
297

      if (!model)
298
299
300
301
        {
          exit_code = 2;
          goto safe_exit;
        }
302
303

      if (mc_options.dot_output & DOT_MODEL)
304
305
306
307
308
        {
          tm.start("dot output");
          spot::print_dot(std::cout, model);
          tm.stop("dot output");
        }
309
310
    }

311
  if (mc_options.force_parallel == false &&
312
      mc_options.formula != nullptr &&
313
      mc_options.model != nullptr)
314
    {
315
316
      std::cout << "Warning : using sequential algorithms (BDD-based)\n\n";

317
318
319
      product = spot::otf_product(model, prop);

      if (mc_options.is_empty)
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
        {
          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();
            }
340
          catch (const std::bad_alloc&)
341
          {
342
            std::cerr << "Out of memory during emptiness check.\n";
343
            if (!mc_options.compress)
344
              std::cerr << "Try option -z for state compression.\n";
345
346
347
348
349
350
351
352
353
354
355
356
            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)
          {
357
            std::cout << "no accepting run found" << std::endl;
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
          }
        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();
              }
374
            catch (const std::bad_alloc&)
375
              {
376
377
                std::cerr
                  << "Out of memory while looking for counterexample.\n";
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
                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");
              }
          }
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413

        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;
          }
414
        }
415
416

      if (mc_options.dot_output & DOT_PRODUCT)
417
418
419
420
421
        {
          tm.start("dot output");
          spot::print_dot(std::cout, product);
          tm.stop("dot output");
        }
422
    }
423
424
  // FIXME : handle here swarming
  else if (mc_options.force_parallel && mc_options.model != nullptr)
425
    {
426
      std::cout << "Warning : using parallel algorithms (CUBE-based)\n\n";
427

428
      if (mc_options.dot_output & DOT_PRODUCT)
429
        {
430
431
432
          std::cerr << "\nERROR: Parallel algorithm doesn't support DOT"
            " output  for the synchronous product.\n"
            "       Please consider removing '-p' option\n";
433
434
435
436
          exit_code = 2;
          goto safe_exit;
        }

437
438
439
440
      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))
441
        {
442
443
          std::cerr << "\nERROR: Algorithm " << mc_options.algorithm
                    << " requires to provide a formula (--formula)\n";
444
445
446
447
          exit_code = 2;
          goto safe_exit;
        }

Antoine Martin's avatar
Antoine Martin committed
448
449
450
451
452
453
      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";

454
455
456
457
458
459
460
461
      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
462
463
464
465
466
467
468
469
470

      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
        {
471
472
          std::vector<std::string> aps = {};
          if (propcube != nullptr)
Etienne Renault's avatar
Etienne Renault committed
473
            aps = propcube->ap();
474

Antoine Martin's avatar
Antoine Martin committed
475
          modelcube = spot::ltsmin_model::load(mc_options.model)
476
            .kripkecube(aps, deadf, mc_options.compress, mc_options.nb_threads);
Antoine Martin's avatar
Antoine Martin committed
477
478
479
480
481
482
483
484
        }
      catch (const std::runtime_error& e)
        {
          std::cerr << e.what() << '\n';
        }
      tm.stop("load kripkecube");

      int memused = spot::memusage();
485
486
487
488
489
490
491
492
493
494
      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
495
496
497
498
499
500
501
502
503
      memused = spot::memusage() - memused;

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

      // Display statistics
504
505
506
507
      std::cout << result << '\n';
      std::cout << memused << " pages allocated for "
                << mc_options.algorithm << '\n';

Antoine Martin's avatar
Antoine Martin committed
508
509
510
511

      if (mc_options.csv)
        {
          std::cout << "\nSummary :\n";
512
513
514
515
516
517
518
519
          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
520
521
522
523
524
525
526
          else if (!mc_options.compute_counterexample)
            {
              std::cout << "an accepting run exists "
                        << "(use -c to print it)" << std::endl;
              exit_code = 1;
            }
          else
527
            std::cout << "an accepting run exists\n" <<  result.trace << '\n';
Antoine Martin's avatar
Antoine Martin committed
528

529

530
531
532
533
534
535
536
537
538
539
540
          // Grab The informations to display into the CSV
          // FIXME: The CSV can be inconsistent since it may return
          // time of one thread and SCC of another.
          auto walltime = std::min_element(result.walltime.rbegin(),
                                           result.walltime.rend());
          auto states = std::min_element(result.states.rbegin(),
                                         result.states.rend());
          auto trans = std::min_element(result.transitions.rbegin(),
                                        result.transitions.rend());
          auto sccs = std::max_element(result.sccs.rbegin(),
                                       result.sccs.rend());
541
542

          std::cout << "Find following the csv: "
543
544
                    << "model,formula,walltimems,memused,type,"
                    << "states,transitions,sccs\n";
545
          std::cout << '#'
546
547
548
549
550
551
                    << split_filename(mc_options.model) << ',';

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

          std::cout << ',' << *walltime << ',' << memused << ','
552
553
                    << rval << ',' << *states << ',' << *trans << ','
                    << *sccs << '\n';
554
        }
555
    }
Antoine Martin's avatar
Antoine Martin committed
556

557
 safe_exit:
558
  if (mc_options.use_timer)
559
    tm.print(std::cout);
560
  tm.reset_all();                // This helps valgrind.
561
562
  return exit_code;
}
563

564
int
565
main(int argc, char** argv)
566
{
567
568
  setup(argv);
  const argp ap = { nullptr, nullptr, nullptr,
569
                    argp_program_doc, children, nullptr, nullptr };
570
571
572
573
574

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

  auto exit_code = checked_main();
575
576

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