modelcheck.cc 10.1 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2011-2018 Laboratoire de Recherche et Developpement
// 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
#include <spot/ltsmin/ltsmin.hh>
22
23
24
25
26
27
28
29
30
#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>
#include <spot/twa/twaproduct.hh>
#include <spot/misc/timer.hh>
#include <spot/misc/memusage.hh>
31
#include <cstring>
32
33
#include <spot/kripke/kripkegraph.hh>
#include <spot/twaalgos/hoa.hh>
34

35
static void
36
37
38
39
40
41
42
syntax(char* prog)
{
  // Display the supplied name unless it appears to be a libtool wrapper.
  char* slash = strrchr(prog, '/');
  if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
    prog = slash + 4;

43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
  std::cerr << "usage: " << prog << " [options] model formula\n\
\n\
Options:\n\
  -dDEAD use DEAD as property for marking DEAD states\n\
          (by default DEAD = true)\n\
  -e[ALGO]  run emptiness check, expect an accepting run\n\
  -E[ALGO]  run emptiness check, expect no accepting run\n\
  -C     compute an accepting run (Counterexample) if it exists\n\
  -D     favor a deterministic translation over a small transition\n\
  -gf    output the automaton of the formula in dot format\n\
  -gm    output the model state-space in dot format\n\
  -gK    output the model state-space in Kripke format\n\
  -gp    output the product state-space in dot format\n\
  -T     time the different phases of the execution\n\
  -z     compress states to handle larger models\n\
  -Z     compress states (faster) assuming all values in [0 .. 2^28-1]\n\
";
60
61
  exit(1);
}
62

63
static int
64
checked_main(int argc, char **argv)
65
{
66
67
68
69
  spot::timer_map tm;

  bool use_timer = false;

70
  enum { DotFormula, DotModel, DotProduct, EmptinessCheck, Kripke }
71
72
73
  output = EmptinessCheck;
  bool accepting_run = false;
  bool expect_counter_example = false;
74
  bool deterministic = false;
75
  char *dead = nullptr;
76
  int compress_states = 0;
77
78
79
80
81
82
83
84
85

  const char* echeck_algo = "Cou99";

  int dest = 1;
  int n = argc;
  for (int i = 1; i < n; ++i)
    {
      char* opt = argv[i];
      if (*opt == '-')
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
        {
          switch (*++opt)
            {
            case 'C':
              accepting_run = true;
              break;
            case 'd':
              dead = opt + 1;
              break;
            case 'D':
              deterministic = true;
              break;
            case 'e':
            case 'E':
              {
                echeck_algo = opt + 1;
                if (!*echeck_algo)
                  echeck_algo = "Cou99";

                expect_counter_example = (*opt == 'e');
                output = EmptinessCheck;
                break;
              }
            case 'g':
              switch (opt[1])
                {
                case 'm':
                  output = DotModel;
                  break;
                case 'p':
                  output = DotProduct;
                  break;
                case 'f':
                  output = DotFormula;
                  break;
121
122
123
                case 'K':
                  output = Kripke;
                  break;
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
                default:
                  goto error;
                }
              break;
            case 'T':
              use_timer = true;
              break;
            case 'z':
              compress_states = 1;
              break;
            case 'Z':
              compress_states = 2;
              break;
            default:
            error:
              std::cerr << "Unknown option `" << argv[i] << "'." << std::endl;
              exit(1);
            }
          --argc;
        }
144
      else
145
146
147
        {
          argv[dest++] = argv[i];
        }
148
149
150
151
152
    }

  if (argc != 3)
    syntax(argv[0]);

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
153
154
  spot::default_environment& env =
    spot::default_environment::instance();
155

156

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
157
  spot::atomic_prop_set ap;
158
  auto dict = spot::make_bdd_dict();
159
  spot::const_kripke_ptr model = nullptr;
160
161
  spot::const_twa_ptr prop = nullptr;
  spot::const_twa_ptr product = nullptr;
162
  spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
163
  int exit_code = 0;
164
  spot::postprocessor post;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
165
166
  spot::formula deadf = nullptr;
  spot::formula f = nullptr;
167

168
  if (!dead || !strcasecmp(dead, "true"))
169
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
170
      deadf = spot::formula::tt();
171
172
173
    }
  else if (!strcasecmp(dead, "false"))
    {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
174
      deadf = spot::formula::ff();
175
176
177
178
179
    }
  else
    {
      deadf = env.require(dead);
    }
180

181
  if (output == EmptinessCheck)
182
    {
183
      const char* err;
184
      echeck_inst = spot::make_emptiness_check_instantiator(echeck_algo, &err);
185
      if (!echeck_inst)
186
187
188
189
190
191
        {
          std::cerr << "Failed to parse argument of -e/-E near `"
                    << err <<  "'\n";
          exit_code = 1;
          goto safe_exit;
        }
192
193
    }

194
195
  tm.start("parsing formula");
  {
196
197
198
    auto pf = spot::parse_infix_psl(argv[2], env, false);
    exit_code = pf.format_errors(std::cerr);
    f = pf.f;
199
200
201
202
203
204
  }
  tm.stop("parsing formula");

  if (exit_code)
    goto safe_exit;

205
  tm.start("translating formula");
206
  {
207
208
209
210
211
    spot::translator trans(dict);
    if (deterministic)
      trans.set_pref(spot::postprocessor::Deterministic);

    prop = trans.run(&f);
212
  }
213
  tm.stop("translating formula");
214

215
216
217
  atomic_prop_collect(f, &ap);

  if (output != DotFormula)
218
    {
219
      tm.start("loading ltsmin model");
220
      try
221
222
223
224
        {
          model = spot::ltsmin_model::load(argv[1]).kripke(&ap, dict, deadf,
                                                           compress_states);
        }
225
      catch (std::runtime_error& e)
226
227
228
        {
          std::cerr << e.what() << '\n';
        }
229
      tm.stop("loading ltsmin model");
230
231

      if (!model)
232
233
234
235
        {
          exit_code = 1;
          goto safe_exit;
        }
236
237

      if (output == DotModel)
238
239
240
241
242
243
        {
          tm.start("dot output");
          spot::print_dot(std::cout, model);
          tm.stop("dot output");
          goto safe_exit;
        }
244
245
246
      if (output == Kripke)
      {
        tm.start("kripke output");
247
        spot::print_hoa(std::cout, model);
248
249
250
        tm.stop("kripke output");
        goto safe_exit;
      }
251
252
    }

253
254
  if (output == DotFormula)
    {
255
256
257
      tm.start("dot output");
      spot::print_dot(std::cout, prop);
      tm.stop("dot output");
258
259
260
      goto safe_exit;
    }

261
  product = spot::otf_product(model, prop);
262

263
  if (output == DotProduct)
264
    {
265
266
267
      tm.start("dot output");
      spot::print_dot(std::cout, product);
      tm.stop("dot output");
268
      goto safe_exit;
269
270
    }

271
272
273
  assert(echeck_inst);

  {
274
    auto ec = echeck_inst->instantiate(product);
275
276
277
278
    bool search_many = echeck_inst->options().get("repeated");
    assert(ec);
    do
      {
279
280
281
282
283
284
285
        int memused = spot::memusage();
        tm.start("running emptiness check");
        spot::emptiness_check_result_ptr res;
        try
          {
            res = ec->check();
          }
286
        catch (const std::bad_alloc&)
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
          {
            std::cerr << "Out of memory during emptiness check."
                      << std::endl;
            if (!compress_states)
              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 (expect_counter_example == !res &&
            (!expect_counter_example || ec->safe()))
          exit_code = 1;

        if (!res)
          {
            std::cout << "no accepting run found";
            if (!ec->safe() && expect_counter_example)
              {
                std::cout << " even if expected" << std::endl;
                std::cout << "this may be due to the use of the bit"
                          << " state hashing technique" << std::endl;
                std::cout << "you can try to increase the heap size "
                          << "or use an explicit storage"
                          << std::endl;
              }
            std::cout << std::endl;
            break;
          }
        else if (accepting_run)
          {

            spot::twa_run_ptr run;
            tm.start("computing accepting run");
            try
              {
                run = res->accepting_run();
              }
330
            catch (const std::bad_alloc&)
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
              {
                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");
              }
          }
        else
          {
            std::cout << "an accepting run exists "
                      << "(use -C to print it)" << std::endl;
          }
358
359
360
361
362
363
364
      }
    while (search_many);
  }

 safe_exit:
  if (use_timer)
    tm.print(std::cout);
365
  tm.reset_all();                // This helps valgrind.
366
367
  return exit_code;
}
368

369
370
371
372
373
374
int
main(int argc, char **argv)
{
  auto exit_code = checked_main(argc, argv);

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