dve2check.cc 9.15 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE)
//
// 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
// the Free Software Foundation; either version 2 of the License, or
// (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
// along with Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

#include "dve2.hh"
#include "tgbaalgos/dotty.hh"
23
24
#include "ltlenv/defaultenv.hh"
#include "ltlast/allnodes.hh"
25
26
27
28
29
30
31
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/emptiness.hh"
#include "tgbaalgos/reducerun.hh"
#include "tgba/tgbaproduct.hh"
#include "misc/timer.hh"
32
#include "misc/memusage.hh"
33
34
#include <cstring>

35
static void
36
37
38
39
40
41
42
43
44
45
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;

  std::cerr << "usage: " << prog << " [options] model formula" << std::endl
	    << std::endl
	    << "Options:" << std::endl
46
47
48
	    << "  -dDEAD use DEAD as property for marking DEAD states"
	    << std::endl
	    << "          (by default DEAD = true)" << std::endl
49
50
51
52
53
54
55
56
57
58
59
60
	    << "  -e[ALGO]  run emptiness check, expect an accepting run"
	    << std::endl
	    << "  -E[ALGO]  run emptiness check, expect no accepting run"
	    << std::endl
	    << "  -C     compute an accepting run (Counterexample) if it exists"
	    << std::endl
	    << "  -gf    output the automaton of the formula in dot format"
	    << std::endl
	    << "  -gm    output the model state-space in dot format"
	    << std::endl
	    << "  -gp    output the product state-space in dot format"
	    << std::endl
61
62
63
            << "  -T     time the different phases of the execution"
	    << std::endl
            << "  -z     compress states to handle larger models"
64
65
66
	    << std::endl
            << "  -Z     compress states (faster) "
	    << "assuming all values in [0 .. 2^28-1]"
67
68
69
70
	    << std::endl;

  exit(1);
}
71
72
73
74

int
main(int argc, char **argv)
{
75
76
77
78
79
80
81
82
  spot::timer_map tm;

  bool use_timer = false;

  enum { DotFormula, DotModel, DotProduct, EmptinessCheck }
  output = EmptinessCheck;
  bool accepting_run = false;
  bool expect_counter_example = false;
83
  char *dead = 0;
84
  int compress_states = 0;
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

  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;
100
101
102
	    case 'd':
	      dead = opt + 1;
	      break;
103
104
105
106
107
108
109
110
111
112
113
114
115
116
	    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])
		{
117
118
119
120
121
122
123
124
125
		case 'm':
		  output = DotModel;
		  break;
		case 'p':
		  output = DotProduct;
		  break;
		case 'f':
		  output = DotFormula;
		  break;
126
127
128
129
130
131
132
		default:
		  goto error;
		}
	      break;
	    case 'T':
	      use_timer = true;
	      break;
133
	    case 'z':
134
135
136
137
	      compress_states = 1;
	      break;
	    case 'Z':
	      compress_states = 2;
138
	      break;
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
	    default:
	    error:
	      std::cerr << "Unknown option `" << argv[i] << "'." << std::endl;
	      exit(1);
	    }
	  --argc;
	}
      else
	{
	  argv[dest++] = argv[i];
	}
    }

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

155
156
157
  spot::ltl::default_environment& env =
    spot::ltl::default_environment::instance();

158

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

  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);
    }
181

182
  if (output == EmptinessCheck)
183
    {
184
185
186
187
188
189
190
191
192
193
      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;
	}
194
195
    }

196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
  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;

  atomic_prop_collect(f, &ap);


  if (output != DotFormula)
211
    {
212
      tm.start("loading dve2");
213
      model = spot::load_dve2(argv[1], dict, &ap, deadf, compress_states, true);
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
      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;
	}
229
230
    }

231

232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
  tm.start("translating formula");
  prop = spot::ltl_to_tgba_fm(f, dict);
  tm.stop("translating formula");

  tm.start("reducing A_f w/ SCC");
  {
    spot::tgba* aut_scc = spot::scc_filter(prop, true);
    delete prop;
    prop = aut_scc;
  }
  tm.stop("reducing A_f w/ SCC");

  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);
253

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


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

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

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

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

316
	    spot::tgba_run* run;
317
	    tm.start("computing accepting run");
318
319
320
321
322
323
324
325
326
327
328
	    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);
	      }
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
360
361
362
363
364
365
366
367
368
369
	    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;

370
371
  deadf->destroy();

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

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

387
  exit(exit_code);
388
}