dve2check.cc 8.18 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
32
33
34
35
36
37
38
39
40
41
42
43
44
#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"
#include <cstring>

void
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
45
46
47
	    << "  -dDEAD use DEAD as property for marking DEAD states"
	    << std::endl
	    << "          (by default DEAD = true)" << std::endl
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
	    << "  -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
            << "  -T    time the different phases of the execution"
	    << std::endl;

  exit(1);
}
65
66
67
68

int
main(int argc, char **argv)
{
69
70
71
72
73
74
75
76
  spot::timer_map tm;

  bool use_timer = false;

  enum { DotFormula, DotModel, DotProduct, EmptinessCheck }
  output = EmptinessCheck;
  bool accepting_run = false;
  bool expect_counter_example = false;
77
  char *dead = 0;
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92

  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;
93
94
95
	    case 'd':
	      dead = opt + 1;
	      break;
96
97
98
99
100
101
102
103
104
105
106
107
108
109
	    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])
		{
110
111
112
113
114
115
116
117
118
		case 'm':
		  output = DotModel;
		  break;
		case 'p':
		  output = DotProduct;
		  break;
		case 'f':
		  output = DotFormula;
		  break;
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
		default:
		  goto error;
		}
	      break;
	    case 'T':
	      use_timer = true;
	      break;
	    default:
	    error:
	      std::cerr << "Unknown option `" << argv[i] << "'." << std::endl;
	      exit(1);
	    }
	  --argc;
	}
      else
	{
	  argv[dest++] = argv[i];
	}
    }

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

142
143
144
  spot::ltl::default_environment& env =
    spot::ltl::default_environment::instance();

145

146
  spot::ltl::atomic_prop_set ap;
147
148
149
150
151
152
153
  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;
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
  spot::ltl::formula* deadf = 0;

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

170
  if (output == EmptinessCheck)
171
    {
172
173
174
175
176
177
178
179
180
181
      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;
	}
182
183
    }

184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
  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)
199
    {
200
      tm.start("loading dve2");
201
      model = spot::load_dve2(argv[1], dict, &ap, deadf, true);
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
      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;
	}
217
218
    }

219

220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
  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);
241

242
  if (output == DotProduct)
243
    {
244
245
246
247
      tm.start("dotty output");
      spot::dotty_reachable(std::cout, product);
      tm.stop("dotty output");
      goto safe_exit;
248
249
250
    }


251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
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
  assert(echeck_inst);

  {
    spot::emptiness_check* ec = echeck_inst->instantiate(product);
    bool search_many = echeck_inst->options().get("repeated");
    assert(ec);
    do
      {
	tm.start("running emptiness check");
	spot::emptiness_check_result* res = ec->check();
	tm.stop("running emptiness check");

	ec->print_stats(std::cout);

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

	    tm.start("computing accepting run");
	    spot::tgba_run* run = res->accepting_run();
	    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;

330
331
  deadf->destroy();

332
333
  if (use_timer)
    tm.print(std::cout);
334
  tm.reset_all();		// This helps valgrind.
335
336
337
338
339
340
341
342
343
344
345
346

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

347
  exit(exit_code);
348
}