modelcheck.cc 23.7 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2011-2019 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
27
#include <spot/ltsmin/spins_kripke.hh>
#include <spot/mc/mc.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>
34
#include <spot/twaalgos/are_isomorphic.hh>
35
36
37
#include <spot/twa/twaproduct.hh>
#include <spot/misc/timer.hh>
#include <spot/misc/memusage.hh>
38
#include <cstring>
39
40
#include <spot/kripke/kripkegraph.hh>
#include <spot/twaalgos/hoa.hh>
41

42
43
44
45
46
#include <thread>
#include <spot/twacube/twacube.hh>
#include <spot/twacube_algos/convert.hh>
#include <spot/mc/ec.hh>

47
48
49
50
51
52
53
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";
54

55
56
57
58
const unsigned DOT_MODEL = 1;
const unsigned DOT_PRODUCT = 2;
const unsigned DOT_FORMULA = 4;
const unsigned CSV = 8;
59

60
61
62
63
64
65
66
67
68
69
// 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;
70
  bool use_timer = false;
71
72
  unsigned compress = 0;
  bool kripke_output = false;
73
  unsigned nb_threads = 1;
74
  bool csv = false;
75
  bool has_deadlock = false;
76
  bool bloemen = 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;
89
90
91
    case 'b':
      mc_options.bloemen = true;
      break;
92
93
94
95
96
    case 'c':
      mc_options.compute_counterexample = true;
      break;
    case 'd':
      if (strcmp(arg, "model") == 0)
97
        mc_options.dot_output |= DOT_MODEL;
98
      else if (strcmp(arg, "product") == 0)
99
        mc_options.dot_output |= DOT_PRODUCT;
100
      else if (strcmp(arg, "formula") == 0)
101
        mc_options.dot_output |= DOT_FORMULA;
102
      else
103
104
105
106
107
        {
          std::cerr << "Unknown argument: '" << arg
                    << "' for option --dot\n";
          return ARGP_ERR_UNKNOWN;
        }
108
109
110
111
112
113
114
      break;
    case 'e':
      mc_options.is_empty = true;
      break;
    case 'f':
      mc_options.formula = arg;
      break;
115
116
117
118
    case 'h':
      mc_options.has_deadlock = true;
      mc_options.selfloopize = false;
      break;
119
120
121
122
123
124
    case 'k':
      mc_options.kripke_output = true;
      break;
    case 'm':
      mc_options.model = arg;
      break;
125
126
127
    case 'p':
      mc_options.nb_threads = to_unsigned(arg);
      break;
128
129
130
131
132
133
134
135
136
137
138
    case 's':
      mc_options.dead_ap = arg;
      break;
    case 't':
      mc_options.use_timer = true;
      break;
    case 'z':
      mc_options.compress = to_unsigned(arg);
      break;
    default:
      return ARGP_ERR_UNKNOWN;
139
    }
140
141
  return 0;
}
142

143
144
145
146
147
148
149
150
151
152
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 },
153
154
    { "bloemen", 'b', nullptr, 0,
      "run the SCC computation of Bloemen et al. (PPOPP'16)", 0 },
155
156
157
    { "counterexample", 'c', nullptr, 0,
      "compute an accepting counterexample (if it exists)", 0 },
    { "is-empty", 'e', nullptr, 0,
158
159
      "check if the model meets its specification. "
      "Return 1 if a counterexample is found."
160
      , 0 },
161
162
163
164
    { "has-deadlock", 'h', nullptr, 0,
      "check if the model has a deadlock. "
      "Return 1 if the model contains a deadlock."
      , 0 },
165
    { "parallel", 'p', "INT", 0, "use INT threads (when possible)", 0 },
166
167
168
169
170
171
172
173
174
175
176
    { "selfloopize", 's', "STRING", 0,
      "use STRING as property for marking deadlock "
      "states (by default selfloopize is activated with STRING='true')", 0 },
    { "timer", 't', nullptr, 0,
      "time the different phases of the execution", 0 },
    // ------------------------------------------------------------
    { nullptr, 0, nullptr, 0, "Output options:", 3 },
    { "dot", 'd', "[model|product|formula]", 0,
      "output the associated automaton in dot format", 0 },
    { "kripke", 'k', nullptr, 0,
      "output the associated automaton in (internal) kripke format", 0 },
177
178
    { "csv", CSV, nullptr, 0,
      "output a CSV containing interesting values", 0 },
179
180
181
182
183
184
185
186
187
188
189
    // ------------------------------------------------------------
    { 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,
190
191
                                  nullptr, nullptr, nullptr,
                                  nullptr, nullptr };
192
193
194
195
196
197
198

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

200
201
202
203
204
205
static std::string  split_filename(const std::string& str) {
  unsigned found = str.find_last_of("/");
  return str.substr(found+1);
}


206
207
static int checked_main()
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
208
209
  spot::default_environment& env =
    spot::default_environment::instance();
210

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
211
  spot::atomic_prop_set ap;
212
  auto dict = spot::make_bdd_dict();
213
  spot::const_kripke_ptr model = nullptr;
214
  spot::const_twa_graph_ptr prop = nullptr;
215
  spot::const_twa_ptr product = nullptr;
216
  spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
217
  int exit_code = 0;
218
  spot::postprocessor post;
219
  spot::formula deadf = spot::formula::tt();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
220
  spot::formula f = nullptr;
221
  spot::timer_map tm;
222

223
  if (mc_options.selfloopize)
224
    {
225
      if (mc_options.dead_ap == nullptr ||
226
227
          !strcasecmp(mc_options.dead_ap, "true"))
        deadf = spot::formula::tt();
228
      else if (!strcasecmp(mc_options.dead_ap, "false"))
229
        deadf = spot::formula::ff();
230
      else
231
        deadf = env.require(mc_options.dead_ap);
232
    }
233
234


235
236
237
238
  if (mc_options.formula != nullptr)
    {
      tm.start("parsing formula");
      {
239
240
241
        auto pf = spot::parse_infix_psl(mc_options.formula, env, false);
        exit_code = pf.format_errors(std::cerr);
        f = pf.f;
242
243
      }
      tm.stop("parsing formula");
244

245
246
      tm.start("translating formula");
      {
247
248
249
250
        spot::translator trans(dict);
        // if (deterministic) FIXME
        //   trans.set_pref(spot::postprocessor::Deterministic);
        prop = trans.run(&f);
251
252
      }
      tm.stop("translating formula");
253

254
      atomic_prop_collect(f, &ap);
255

256
      if (mc_options.dot_output & DOT_FORMULA)
257
258
259
260
261
        {
          tm.start("dot output");
          spot::print_dot(std::cout, prop);
          tm.stop("dot output");
        }
262
    }
263

264
  if (mc_options.model != nullptr)
265
    {
266
      tm.start("loading ltsmin model");
267
      try
268
269
270
271
        {
          model = spot::ltsmin_model::load(mc_options.model)
            .kripke(&ap, dict, deadf, mc_options.compress);
        }
272
      catch (std::runtime_error& e)
273
274
275
        {
          std::cerr << e.what() << '\n';
        }
276
      tm.stop("loading ltsmin model");
277
278

      if (!model)
279
280
281
282
        {
          exit_code = 2;
          goto safe_exit;
        }
283
284

      if (mc_options.dot_output & DOT_MODEL)
285
286
287
288
289
        {
          tm.start("dot output");
          spot::print_dot(std::cout, model);
          tm.stop("dot output");
        }
290
      if (mc_options.kripke_output)
291
292
293
294
295
        {
          tm.start("kripke output");
          spot::print_hoa(std::cout, model);
          tm.stop("kripke output");
        }
296
297
    }

298
299
  if (mc_options.nb_threads == 1 &&
      mc_options.formula != nullptr &&
300
      mc_options.model != nullptr)
301
    {
302
303
304
      product = spot::otf_product(model, prop);

      if (mc_options.is_empty)
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
        {
          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();
            }
325
          catch (std::bad_alloc&)
326
327
328
329
330
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
357
358
359
          {
            std::cerr << "Out of memory during emptiness check."
                      << std::endl;
            if (!mc_options.compress)
              std::cerr << "Try option -z for state compression." << std::endl;
            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)
          {
            std::cout << "no accepting run found";
          }
        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();
              }
360
            catch (std::bad_alloc&)
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
              {
                std::cerr << "Out of memory while looking for counterexample."
                          << std::endl;
                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");
              }
          }
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399

        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;
          }
400
        }
401
402

      if (mc_options.dot_output & DOT_PRODUCT)
403
404
405
406
407
        {
          tm.start("dot output");
          spot::print_dot(std::cout, product);
          tm.stop("dot output");
        }
408
409
    }

410
411
412
413
414
415
416
417
418
419
420
    if (mc_options.nb_threads != 1 &&
        mc_options.formula != nullptr &&
        mc_options.model != nullptr)
    {
      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";

      tm.start("twa to twacube");
Etienne Renault's avatar
Etienne Renault committed
421
      auto propcube = spot::twa_to_twacube(prop);
422
423
424
      tm.stop("twa to twacube");

      tm.start("load kripkecube");
Etienne Renault's avatar
Etienne Renault committed
425
      spot::ltsmin_kripkecube_ptr modelcube = nullptr;
426
427
      try
        {
428
           modelcube = spot::ltsmin_model::load(mc_options.model)
429
430
             .kripkecube(propcube->get_ap(), deadf, mc_options.compress,
                         mc_options.nb_threads);
431
432
433
434
435
436
437
438
439
        }
      catch (std::runtime_error& e)
        {
          std::cerr << e.what() << '\n';
        }
      tm.stop("load kripkecube");

      int memused = spot::memusage();
      tm.start("emptiness check");
440
441
442
443
444
      auto res = spot::modelcheck<spot::ltsmin_kripkecube_ptr,
                                  spot::cspins_state,
                                  spot::cspins_iterator,
                                  spot::cspins_state_hash,
                                  spot::cspins_state_equal>
445
446
447
448
449
450
451
452
453
454
455
        (modelcube, propcube, mc_options.compute_counterexample);
      tm.stop("emptiness check");
      memused = spot::memusage() - memused;

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

      // Display statistics
456
457
      unsigned smallest = 0;
      for (unsigned i = 0; i < std::get<2>(res).size(); ++i)
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
          if (std::get<2>(res)[i].states < std::get<2>(res)[smallest].states)
            smallest = i;

          std::cout << "\n---- Thread number : " << i << '\n';
          std::cout << std::get<2>(res)[i].states << " unique states visited\n";
          std::cout << std::get<2>(res)[i].instack_sccs
                    << " strongly connected components in search stack\n";
          std::cout << std::get<2>(res)[i].transitions
                    << " transitions explored\n";
          std::cout << std::get<2>(res)[i].instack_item
                    << " items max in DFS search stack\n";

          // FIXME: produce walltime for each threads.
          if (mc_options.csv)
            {
              std::cout << "Find following the csv: "
                        << "thread_id,walltimems,type,"
                        << "states,transitions\n";
              std::cout << "@th_" << i << ','
                        << tm.timer("emptiness check").walltime() << ','
                        << (!std::get<2>(res)[i].is_empty ?
                            "EMPTY," : "NONEMPTY,")
                        << std::get<2>(res)[i].states << ','
                        << std::get<2>(res)[i].transitions
                        << std::endl;
            }
485
        }
486

487
488
489

      if (mc_options.csv)
        {
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
          std::cout << "\nSummary :\n";
          if (!std::get<0>(res))
            std::cout << "no accepting run found\n";
          else if (!mc_options.compute_counterexample)
            {
              std::cout << "an accepting run exists "
                        << "(use -c to print it)" << std::endl;
              exit_code = 1;
            }
          else
            std::cout << "an accepting run exists!\n" << std::get<1>(res)
                      << '\n';

          std::cout << "Find following the csv: "
                    << "model,formula,walltimems,memused,type"
505
                    << "states,transitions\n";
506

507
508
509
510
511
512
513
          std::cout << '#'
                    << split_filename(mc_options.model)
                    << ','
                    << mc_options.formula << ','
                    << tm.timer("emptiness check").walltime() << ','
                    << memused << ','
                    << (!std::get<0>(res) ? "EMPTY," : "NONEMPTY,")
514
515
516
                    << std::get<2>(res)[smallest].states << ','
                    << std::get<2>(res)[smallest].transitions
                    << '\n';
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

    if (mc_options.has_deadlock &&  mc_options.model != nullptr)
    {
      assert(!mc_options.selfloopize);
      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";

      tm.start("load kripkecube");
      spot::ltsmin_kripkecube_ptr modelcube = nullptr;
      try
        {
           modelcube = spot::ltsmin_model::load(mc_options.model)
             .kripkecube({}, deadf, mc_options.compress,
                         mc_options.nb_threads);
        }
      catch (std::runtime_error& e)
        {
          std::cerr << e.what() << '\n';
        }
      tm.stop("load kripkecube");

      int memused = spot::memusage();
      tm.start("deadlock check");
      auto res = spot::has_deadlock<spot::ltsmin_kripkecube_ptr,
                                    spot::cspins_state,
                                    spot::cspins_iterator,
                                    spot::cspins_state_hash,
                                    spot::cspins_state_equal>(modelcube);
      tm.stop("deadlock check");
      memused = spot::memusage() - memused;

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

      // Display statistics
      unsigned smallest = 0;
      for (unsigned i = 0; i < std::get<1>(res).size(); ++i)
        {
          if (std::get<1>(res)[i].states < std::get<1>(res)[smallest].states)
            smallest = i;

          std::cout << "\n---- Thread number : " << i << '\n';
          std::cout << std::get<1>(res)[i].states << " unique states visited\n";
          std::cout << std::get<1>(res)[i].transitions
                    << " transitions explored\n";
          std::cout << std::get<1>(res)[i].instack_dfs
                    << " items max in DFS search stack\n";
          std::cout << std::get<1>(res)[i].walltime
                    << " milliseconds\n";

          if (mc_options.csv)
            {
              std::cout << "Find following the csv: "
                        << "thread_id,walltimems,type,"
                        << "states,transitions\n";
              std::cout << "@th_" << i << ','
                        << std::get<1>(res)[i].walltime << ','
                        << (std::get<1>(res)[i].has_deadlock ?
                            "DEADLOCK," : "NO-DEADLOCK,")
                        << std::get<1>(res)[i].states << ','
                        << std::get<1>(res)[i].transitions
                        << std::endl;
            }
        }

      if (mc_options.csv)
        {
          std::cout << "\nSummary :\n";
          if (!std::get<0>(res))
            std::cout << "No no deadlock found!\n";
          else
            {
              std::cout << "A deadlock exists!\n";
              exit_code = 1;
            }

          std::cout << "Find following the csv: "
                    << "model,walltimems,memused,type,"
                    << "states,transitions\n";

          std::cout << '#'
                    << split_filename(mc_options.model)
                    << ','
                    << tm.timer("deadlock check").walltime() << ','
                    << memused << ','
                    << (std::get<0>(res) ? "DEADLOCK," : "NO-DEADLOCK,")
                    << std::get<1>(res)[smallest].states << ','
                    << std::get<1>(res)[smallest].transitions
                    << '\n';
        }
    }

618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
    if (mc_options.bloemen &&  mc_options.model != nullptr)
      {
        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";

        tm.start("load kripkecube");
        spot::ltsmin_kripkecube_ptr modelcube = nullptr;
        try
          {
            modelcube = spot::ltsmin_model::load(mc_options.model)
              .kripkecube({}, deadf, mc_options.compress,
                          mc_options.nb_threads);
          }
        catch (std::runtime_error& e)
          {
            std::cerr << e.what() << '\n';
          }
        tm.stop("load kripkecube");

        int memused = spot::memusage();
        tm.start("bloemen");
        auto res = spot::bloemen<spot::ltsmin_kripkecube_ptr,
                                 spot::cspins_state,
                                 spot::cspins_iterator,
                                 spot::cspins_state_hash,
                                 spot::cspins_state_equal>(modelcube);
        tm.stop("bloemen");
        memused = spot::memusage() - memused;

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

        // Display statistics
657
658
659
        unsigned sccs = 0;
        unsigned st = 0;
        unsigned tr = 0;
660
661
662
663
664
665
666
667
668
669
        for (unsigned i = 0; i < res.first.size(); ++i)
          {
            std::cout << "\n---- Thread number : " << i << '\n';
            std::cout << res.first[i].states << " unique states visited\n";
            std::cout << res.first[i].transitions
                      << " transitions explored\n";
            std::cout << res.first[i].sccs << " sccs found\n";
            std::cout << res.first[i].walltime
                      << " milliseconds\n";

670
671
672
673
            sccs += res.first[i].sccs;
            st += res.first[i].states;
            tr += res.first[i].transitions;

674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
            if (mc_options.csv)
              {
                std::cout << "Find following the csv: "
                          << "thread_id,walltimems,"
                          << "states,transitions,sccs\n";
                std::cout << "@th_" << i << ','
                          << res.first[i].walltime << ','
                          << res.first[i].states << ','
                          << res.first[i].transitions << ','
                          << res.first[i].sccs
                          << std::endl;
              }
          }

      if (mc_options.csv)
        {
          std::cout << "\nSummary :\n";
          std::cout << "Find following the csv: "
692
693
694
                    << "model,walltimems,memused,"
                    << "cumulated_states,cumulated_transitions,"
                    << "cumulated_sccs\n";
695
696
697
698
699
700

          std::cout << '#'
                    << split_filename(mc_options.model)
                    << ','
                    << tm.timer("bloemen").walltime() << ','
                    << memused << ','
701
702
703
                    << st << ','
                    << tr << ','
                    << sccs
704
705
706
707
                    << '\n';
        }
      }

708
 safe_exit:
709
  if (mc_options.use_timer)
710
    tm.print(std::cout);
711
  tm.reset_all();                // This helps valgrind.
712
713
  return exit_code;
}
714

715

716
int
717
main(int argc, char** argv)
718
{
719
720
  setup(argv);
  const argp ap = { nullptr, nullptr, nullptr,
721
                    argp_program_doc, children, nullptr, nullptr };
722
723
724
725
726

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

  auto exit_code = checked_main();
727
728

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