dve2check.cc 9.28 KB
Newer Older
1
2
// Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE)
3
4
5
6
7
//
// 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
8
// the Free Software Foundation; either version 3 of the License, or
9
10
11
12
13
14
15
16
// (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
17
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
18
19
20

#include "dve2.hh"
#include "tgbaalgos/dotty.hh"
21
22
#include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh"
23
#include "ltlparse/public.hh"
24
#include "tgbaalgos/translate.hh"
25
26
#include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/reducerun.hh"
27
#include "tgbaalgos/postproc.hh"
28
29
#include "tgba/tgbaproduct.hh"
#include "misc/timer.hh"
30
#include "misc/memusage.hh"
31
#include <cstring>
32
33
#include "kripke/kripkeexplicit.hh"
#include "kripke/kripkeprint.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
64
65

int
main(int argc, char **argv)
{
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 = 0;
76
  int compress_states = 0;
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

  const char* echeck_algo = "Cou99";

  int dest = 1;
  int n = argc;
  for (int i = 1; i < n; ++i)
    {
      char* opt = argv[i];
      if (*opt == '-')
	{
	  switch (*++opt)
	    {
	    case 'C':
	      accepting_run = true;
	      break;
92
93
94
	    case 'd':
	      dead = opt + 1;
	      break;
95
96
97
	    case 'D':
	      deterministic = true;
	      break;
98
99
100
101
102
103
104
	    case 'e':
	    case 'E':
	      {
		echeck_algo = opt + 1;
		if (!*echeck_algo)
		  echeck_algo = "Cou99";

105
		expect_counter_example = (*opt == 'e');
106
107
108
109
110
111
		output = EmptinessCheck;
		break;
	      }
	    case 'g':
	      switch (opt[1])
		{
112
113
114
115
116
117
118
119
120
		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
		default:
		  goto error;
		}
	      break;
	    case 'T':
	      use_timer = true;
	      break;
131
	    case 'z':
132
133
134
135
	      compress_states = 1;
	      break;
	    case 'Z':
	      compress_states = 2;
136
	      break;
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
	    default:
	    error:
	      std::cerr << "Unknown option `" << argv[i] << "'." << std::endl;
	      exit(1);
	    }
	  --argc;
	}
      else
	{
	  argv[dest++] = argv[i];
	}
    }

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

153
154
155
  spot::ltl::default_environment& env =
    spot::ltl::default_environment::instance();

156

157
  spot::ltl::atomic_prop_set ap;
158
159
  spot::bdd_dict* dict = new spot::bdd_dict();
  spot::kripke* model = 0;
160
  const spot::tgba* prop = 0;
161
162
163
  spot::tgba* product = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
  int exit_code = 0;
164
165
  const spot::ltl::formula* f = 0;
  const spot::ltl::formula* deadf = 0;
166
  spot::postprocessor post;
167
168
169
170
171
172
173
174
175
176
177
178
179

  if (dead == 0 || !strcasecmp(dead, "true"))
    {
      deadf = spot::ltl::constant::true_instance();
    }
  else if (!strcasecmp(dead, "false"))
    {
      deadf = spot::ltl::constant::false_instance();
    }
  else
    {
      deadf = env.require(dead);
    }
180

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

195
196
197
198
199
200
201
202
203
204
205
  tm.start("parsing formula");
  {
    spot::ltl::parse_error_list pel;
    f = spot::ltl::parse(argv[2], pel, env, false);
    exit_code = spot::ltl::format_parse_errors(std::cerr, argv[2], pel);
  }
  tm.stop("parsing formula");

  if (exit_code)
    goto safe_exit;

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

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

216
217
218
  atomic_prop_collect(f, &ap);

  if (output != DotFormula)
219
    {
220
      tm.start("loading dve2");
221
      model = spot::load_dve2(argv[1], dict, &ap, deadf, compress_states, true);
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
      tm.stop("loading dve2");

      if (!model)
	{
	  exit_code = 1;
	  goto safe_exit;
	}

      if (output == DotModel)
	{
	  tm.start("dotty output");
	  spot::dotty_reachable(std::cout, model);
	  tm.stop("dotty output");
	  goto safe_exit;
	}
237
238
239
      if (output == Kripke)
      {
        tm.start("kripke output");
240
	spot::kripke_save_reachable_renumbered(std::cout, model);
241
242
243
        tm.stop("kripke output");
        goto safe_exit;
      }
244
245
    }

246
247
248
249
250
251
252
253
254
  if (output == DotFormula)
    {
      tm.start("dotty output");
      spot::dotty_reachable(std::cout, prop);
      tm.stop("dotty output");
      goto safe_exit;
    }

  product = new spot::tgba_product(model, prop);
255

256
  if (output == DotProduct)
257
    {
258
259
260
261
      tm.start("dotty output");
      spot::dotty_reachable(std::cout, product);
      tm.stop("dotty output");
      goto safe_exit;
262
263
    }

264
265
266
267
268
269
270
271
  assert(echeck_inst);

  {
    spot::emptiness_check* ec = echeck_inst->instantiate(product);
    bool search_many = echeck_inst->options().get("repeated");
    assert(ec);
    do
      {
272
	int memused = spot::memusage();
273
	tm.start("running emptiness check");
274
275
276
277
278
279
280
281
282
	spot::emptiness_check_result* res;
	try
	  {
	    res = ec->check();
	  }
	catch (std::bad_alloc)
	  {
	    std::cerr << "Out of memory during emptiness check."
		      << std::endl;
283
284
	    if (!compress_states)
	      std::cerr << "Try option -z for state compression." << std::endl;
285
286
287
	    exit_code = 2;
	    exit(exit_code);
	  }
288
	tm.stop("running emptiness check");
289
	memused = spot::memusage() - memused;
290
291

	ec->print_stats(std::cout);
292
293
	std::cout << memused << " pages allocated for emptiness check"
		  << std::endl;
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316

	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)
	  {

317
	    spot::tgba_run* run;
318
	    tm.start("computing accepting run");
319
320
321
322
323
324
325
326
327
328
329
	    try
	      {
		run = res->accepting_run();
	      }
	    catch (std::bad_alloc)
	      {
		std::cerr << "Out of memory while looking for counterexample."
			  << std::endl;
		exit_code = 2;
		exit(exit_code);
	      }
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
360
361
362
363
364
365
366
367
368
369
370
	    tm.stop("computing accepting run");

	    if (!run)
	      {
		std::cout << "an accepting run exists" << std::endl;
	      }
	    else
	      {
		tm.start("reducing accepting run");
		spot::tgba_run* redrun =
		  spot::reduce_run(res->automaton(), run);
		tm.stop("reducing accepting run");
		delete run;
		run = redrun;

		tm.start("printing accepting run");
		spot::print_tgba_run(std::cout, product, run);
		tm.stop("printing accepting run");
	      }
	    delete run;
	  }
	else
	  {
	    std::cout << "an accepting run exists "
		      << "(use -C to print it)" << std::endl;
	  }
	delete res;
      }
    while (search_many);
    delete ec;
  }

 safe_exit:
  delete echeck_inst;
  delete product;
  delete prop;
  delete model;
  if (f)
    f->destroy();
  delete dict;

371
372
  deadf->destroy();

373
374
  if (use_timer)
    tm.print(std::cout);
375
  tm.reset_all();		// This helps valgrind.
376
377
378
379
380
381
382
383
384
385
386
387

  spot::ltl::atomic_prop::dump_instances(std::cerr);
  spot::ltl::unop::dump_instances(std::cerr);
  spot::ltl::binop::dump_instances(std::cerr);
  spot::ltl::multop::dump_instances(std::cerr);
  spot::ltl::automatop::dump_instances(std::cerr);
  assert(spot::ltl::atomic_prop::instance_count() == 0);
  assert(spot::ltl::unop::instance_count() == 0);
  assert(spot::ltl::binop::instance_count() == 0);
  assert(spot::ltl::multop::instance_count() == 0);
  assert(spot::ltl::automatop::instance_count() == 0);

388
  exit(exit_code);
389
}