ltlgspn.cc 10.7 KB
Newer Older
1
2
3
4
5
6
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2011, 2012 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE)
// Copyright (C) 2003, 2004, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
//
// 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
25
#ifndef SSP
26
#include "gspn.hh"
27
28
#define MIN_ARG 3
#else
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
29
#include "ssp.hh"
30
31
32
33
#define MIN_ARG 4
#include "tgba/tgbaexplicit.hh"
#include "tgbaparse/public.hh"
#endif
34
35
36
#include "ltlparse/public.hh"
#include "tgba/tgbatba.hh"
#include "tgba/tgbaproduct.hh"
37
#include "tgbaalgos/ltl2tgba_lacim.hh"
38
#include "tgbaalgos/ltl2tgba_fm.hh"
39
#include "tgbaalgos/magic.hh"
40
41
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
42
#include "tgbaalgos/projrun.hh"
43

44

45
46
47
48
void
syntax(char* prog)
{
  std::cerr << "Usage: "<< prog
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
49
#ifndef SSP
50
	    << " [OPTIONS...] model formula props..."   << std::endl
51
52
53
#else
	    << " [OPTIONS...] model formula automata props..."   << std::endl
#endif
54
	    << std::endl
55
56
57
#ifdef SSP
	    << "  -1  do not use a double hash (for inclusion check)"
	    << std::endl
58
59
	    << "  -L  use LIFO ordering for inclusion check"
	    << std::endl
60
#endif
61
	    << "  -c  compute an example" << std::endl
62
63
	    << "      (instead of just checking for emptiness)" << std::endl
	    << std::endl
64
65
66
67
68
69
#ifndef SSP
            << "  -d DEAD" << std::endl
            << "      use DEAD as property for marking dead states"
	    << " (by default DEAD=true)" << std::endl
#endif

70
	    << "  -e  use Couvreur's emptiness-check (default)" << std::endl
71
	    << "  -e2 use Couvreur's emptiness-check's shy variant" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
72
#ifdef SSP
73
74
	    << "  -e3 use semi-d. incl. Couvreur's emptiness-check"
	    << std::endl
75
76
	    << "  -e4 use semi-d. incl. Couvreur's emptiness-check's "
	    << "shy variant"
77
	    << std::endl
78
79
80
	    << "  -e45 mix of -e4 and -e5 (semi.d. incl. before d.incl.)"
	    << std::endl
	    << "  -e54 mix of -e5 and -e4 (the other way around)" << std::endl
81
82
	    << "  -e5 use d. incl. Couvreur's emptiness-check's shy variant"
	    << std::endl
83
84
	    << "  -e6 like -e5, but without inclusion checks in the "
	    << "search stack" << std::endl
85
#endif
86
87
	    << "  -m  degeneralize and perform a magic-search" << std::endl
	    << std::endl
88
89
90
#ifdef SSP
            << "  -n  do not perform any decomposition" << std::endl
#endif
91
92
            << "  -l  use Couvreur's LaCIM algorithm for translation (default)"
	    << std::endl
93
94
            << "  -f  use Couvreur's FM algorithm for translation" << std::endl
	    << "  -P  do not project example on model" << std::endl;
95
96
97
  exit(2);
}

98
99
100
101
102
103
104
105
106
107

void
display_stats(const spot::unsigned_statistics* s)
{
  assert(s);
  spot::unsigned_statistics::stats_map::const_iterator i;
  for (i = s->stats.begin(); i != s->stats.end(); ++i)
    std::cout << i->first << " = " << (s->*i->second)() << std::endl;
}

108
109
110
111
int
main(int argc, char **argv)
  try
    {
112
      int formula_index = 1;
113
114
      enum { Couvreur, Couvreur2, Couvreur3,
	     Couvreur4, Couvreur5, Magic } check = Couvreur;
115
116
      enum { Lacim, Fm } trans = Lacim;
      bool compute_counter_example = false;
117
      bool proj = true;
118
119
#ifdef SSP
      bool doublehash = true;
120
      bool stack_inclusion = true;
121
      bool pushfront = false;
122
      bool double_inclusion = false;
123
      bool reversed_double_inclusion = false;
124
      bool no_decomp = false;
125
#endif
126
      std::string dead = "true";
127

128
      spot::ltl::declarative_environment env;
129

130
      while (formula_index < argc && *argv[formula_index] == '-')
131
	{
132
133
134
135
136
#ifdef SSP
	  if (!strcmp(argv[formula_index], "-1"))
	    {
	      doublehash = false;
	    }
137
138
139
140
	  else if (!strcmp(argv[formula_index], "-L"))
	    {
	      pushfront = true;
	    }
141
142
	  else
#endif
143
144
145
146
	  if (!strcmp(argv[formula_index], "-c"))
	    {
	      compute_counter_example = true;
	    }
147
148
149
150
151
152
153
154
155
156
157
#ifndef SSP
	  else if (!strcmp(argv[formula_index], "-d"))
	    {
	      if (formula_index + 1 >= argc)
		syntax(argv[0]);
	      dead = argv[++formula_index];
	      if (strcasecmp(dead.c_str(), "true")
		  && strcasecmp(dead.c_str(), "false"))
		env.declare(dead);
	    }
#endif
158
159
160
161
	  else if (!strcmp(argv[formula_index], "-e"))
	    {
	      check = Couvreur;
	    }
162
163
164
165
	  else if (!strcmp(argv[formula_index], "-e2"))
	    {
	      check = Couvreur2;
	    }
166
#ifdef SSP
167
168
169
170
171
172
173
174
	  else if (!strcmp(argv[formula_index], "-e3"))
	    {
	      check = Couvreur3;
	    }
	  else if (!strcmp(argv[formula_index], "-e4"))
	    {
	      check = Couvreur4;
	    }
175
176
177
178
179
	  else if (!strcmp(argv[formula_index], "-e45"))
	    {
	      check = Couvreur5;
	      double_inclusion = true;
	    }
180
181
182
183
184
185
	  else if (!strcmp(argv[formula_index], "-e54"))
	    {
	      check = Couvreur5;
	      double_inclusion = true;
	      reversed_double_inclusion = true;
	    }
186
187
188
189
	  else if (!strcmp(argv[formula_index], "-e5"))
	    {
	      check = Couvreur5;
	    }
190
191
192
193
194
	  else if (!strcmp(argv[formula_index], "-e6"))
	    {
	      check = Couvreur5;
	      stack_inclusion = false;
	    }
195
#endif
196
197
198
199
	  else if (!strcmp(argv[formula_index], "-m"))
	    {
	      check = Magic;
	    }
200
201
202
203
204
205
#ifdef SSP
	  else if (!strcmp(argv[formula_index], "-n"))
	    {
	      no_decomp = true;
	    }
#endif
206
207
208
209
210
211
212
213
	  else if (!strcmp(argv[formula_index], "-l"))
	    {
	      trans = Lacim;
	    }
	  else if (!strcmp(argv[formula_index], "-f"))
	    {
	      trans = Fm;
	    }
214
215
216
217
	  else if (!strcmp(argv[formula_index], "-P"))
	    {
	      proj = 0;
	    }
218
219
220
221
222
	  else
	    {
	      syntax(argv[0]);
	    }
	  ++formula_index;
223
	}
224
      if (argc < formula_index + MIN_ARG)
225
226
	syntax(argv[0]);

227

228
      while (argc >= formula_index + MIN_ARG)
229
230
231
232
233
234
	{
	  env.declare(argv[argc - 1]);
	  --argc;
	}

      spot::ltl::parse_error_list pel;
235
236
      const spot::ltl::formula* f =
	spot::ltl::parse(argv[formula_index + 1], pel, env);
237

238
239
240
      if (spot::ltl::format_parse_errors(std::cerr,
					 argv[formula_index + 1], pel))
	exit(2);
241

242
      argv[1] = argv[formula_index];
243
244
      spot::bdd_dict* dict = new spot::bdd_dict();

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
245
#if SSP
246
      bool inclusion = (check != Couvreur && check != Couvreur2);
247
248
      spot::gspn_ssp_interface gspn(2, argv, dict, env, inclusion,
				    doublehash, pushfront);
249
250
251
252

      spot::tgba_parse_error_list pel1;
      spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2],
						      pel1, dict, env);
253
254
      if (spot::format_tgba_parse_errors(std::cerr, argv[formula_index + 2],
					 pel1))
255
256
	return 2;
#else
257
      spot::gspn_interface gspn(2, argv, dict, env, dead);
258
259
#endif

260
261
262
263
264
265
266
267
268
269
      spot::tgba* a_f = 0;
      switch (trans)
	{
	case Fm:
	  a_f = spot::ltl_to_tgba_fm(f, dict);
	  break;
	case Lacim:
	  a_f = spot::ltl_to_tgba_lacim(f, dict);
	  break;
	}
270
      f->destroy();
271

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
272
#ifndef SSP
273
      spot::tgba* model        = gspn.automaton();
274
      spot::tgba_product* prod = new spot::tgba_product(model, a_f);
275
276
#else
      spot::tgba_product* ca = new spot::tgba_product(control, a_f);
277
      spot::tgba* model      = gspn.automaton(ca);
278
279
      spot::tgba* prod = model;
#endif
280

281
282
283
      switch (check)
	{
	case Couvreur:
284
	case Couvreur2:
285
286
287
	case Couvreur3:
	case Couvreur4:
	case Couvreur5:
288
	  {
289
	    spot::couvreur99_check* ec;
290

291
292
293
	    switch (check)
	      {
	      case Couvreur:
294
		ec = new spot::couvreur99_check(prod);
295
296
		break;
	      case Couvreur2:
297
		ec = new spot::couvreur99_check_shy(prod);
298
		break;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
299
#ifdef SSP
300
	      case Couvreur3:
301
		ec = spot::couvreur99_check_ssp_semi(prod);
302
303
		break;
	      case Couvreur4:
304
		ec = spot::couvreur99_check_ssp_shy_semi(prod);
305
306
		break;
	      case Couvreur5:
307
308
		ec = spot::couvreur99_check_ssp_shy(prod, stack_inclusion,
						    double_inclusion,
309
						    reversed_double_inclusion,
310
						    no_decomp);
311
		break;
312
#endif
313
314
	      default:
		assert(0);
315
316
317
		// Assign something so that GCC does not complains
		// EC might be used uninitialized if assert is disabled.
		ec = 0;
318
	      }
319

320
321
322
	    spot::emptiness_check_result* res = ec->check();
	    const spot::couvreur99_check_status* ecs = ec->result();
	    if (res)
323
324
325
	      {
		if (compute_counter_example)
		  {
326
		    spot::couvreur99_check_result* ce;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
327
#ifndef SSP
328
		    ce = new spot::couvreur99_check_result(ecs);
329
#else
330
331
332
333
		    switch (check)
		      {
		      case Couvreur:
		      case Couvreur2:
334
		      case Couvreur5:
335
			ce = new spot::couvreur99_check_result(ecs);
336
337
			break;
		      default:
338
339
340
341
342
			// ce = spot::counter_example_ssp(ecs);
			std::cerr
			  << "counter_example_ssp() is no longer supported"
			  << std::endl;
			exit(1);
343
		      }
344
#endif
345
		    spot::tgba_run* run = ce->accepting_run();
346
347
348
349
350
351
352
353
354
355
		    if (proj)
		      {
			spot::tgba_run* p = project_tgba_run(prod, model, run);
			spot::print_tgba_run(std::cout, model, p);
			delete p;
		      }
		    else
		      {
			spot::print_tgba_run(std::cout, prod, run);
		      }
356
		    ce->print_stats(std::cout);
357
		    display_stats(ec);
358
		    delete run;
359
		    delete ce;
360
361
362
363
		  }
		else
		  {
		    std::cout << "non empty" << std::endl;
364
		    ecs->print_stats(std::cout);
365
		    display_stats(ec);
366
		  }
367
		delete res;
368
369
370
371
	      }
	    else
	      {
		std::cout << "empty" << std::endl;
372
		ecs->print_stats(std::cout);
373
		display_stats(ec);
374
	      }
375
	    std::cout << std::endl;
376
	    delete ec;
377
	    if (res)
378
	      exit(1);
379
	  }
380
381
	  break;
	case Magic:
382
	  {
383
	    spot::tgba_tba_proxy* d  = new spot::tgba_tba_proxy(prod);
384
	    spot::emptiness_check* ec = spot::explicit_magic_search(d);
385

386
	    spot::emptiness_check_result* res = ec->check();
387
	    if (res)
388
389
	      {
		if (compute_counter_example)
390
391
		  {
		    spot::tgba_run* run = res->accepting_run();
392
393
394
395
396
397
398
399
400
401
		    if (proj)
		      {
			spot::tgba_run* p = project_tgba_run(prod, model, run);
			spot::print_tgba_run(std::cout, model, p);
			delete p;
		      }
		    else
		      {
			spot::print_tgba_run(std::cout, prod, run);
		      }
402
403
		    delete run;
		  }
404
405
		else
		  std::cout << "non-empty" << std::endl;
406
		delete res;
407
408
409
410
411
412
		exit(1);
	      }
	    else
	      {
		std::cout << "empty" << std::endl;
	      }
413
	    delete ec;
414
	    delete d;
415
	  }
416
	}
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
417
#ifndef SSP
418
419
      delete prod;
      delete model;
420
421
422
#else
      delete model;
      delete control;
423
      delete ca;
424
#endif
425
426
427
      delete a_f;
      delete dict;
    }
428
  catch (spot::gspn_exception e)
429
430
431
432
    {
      std::cerr << e << std::endl;
      throw;
    }