ltl2tgba.cc 19.6 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// Copyright (C) 2003, 2004  Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// 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.

22
23
#include <iostream>
#include <cassert>
24
25
#include <fstream>
#include <string>
26
#include "ltlvisit/destroy.hh"
27
#include "ltlvisit/reduce.hh"
28
#include "ltlvisit/tostring.hh"
29
30
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
31
#include "tgbaalgos/ltl2tgba_lacim.hh"
32
#include "tgbaalgos/ltl2tgba_fm.hh"
33
#include "tgba/bddprint.hh"
34
#include "tgbaalgos/dotty.hh"
35
#include "tgbaalgos/lbtt.hh"
36
#include "tgba/tgbatba.hh"
37
#include "tgbaalgos/magic.hh"
martinez's avatar
martinez committed
38
39
40
41
#include "tgbaalgos/nesteddfs.hh"
#include "tgbaalgos/colordfs.hh"
#include "tgbaalgos/tarjan_on_fly.hh"
//#include "tgbaalgos/minimalce.hh"
42
43
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
44
#include "tgbaparse/public.hh"
45
#include "tgbaalgos/dupexp.hh"
46
#include "tgbaalgos/neverclaim.hh"
47

48
49
#include "tgbaalgos/reductgba_sim.hh"

50
51
52
void
syntax(char* prog)
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
53
  std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl
54
            << "       "<< prog << " -F [OPTIONS...] file" << std::endl
55
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
56
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
57
	    << "Options:" << std::endl
martinez's avatar
martinez committed
58
	    << "  -a    display the acceptance_conditions BDD, not the "
59
	    << "reachability graph"
60
	    << std::endl
martinez's avatar
martinez committed
61
62
63
64
65
66
67
68
	    << "  -A    same as -a, but as a set" << std::endl
	    << "  -c    color-search (implies -D), expect a counter-example"
	    << std::endl
	    << "  -C    color-search (implies -D), expect no counter-example"
	    << std::endl
	    << "  -d    turn on traces during parsing" << std::endl
	    << "  -D    degeneralize the automaton" << std::endl
	    << "  -e    emptiness-check (Couvreur), expect and compute "
69
	    << "a counter-example" << std::endl
martinez's avatar
martinez committed
70
	    << "  -e2   emptiness-check (Couvreur variant), expect and compute "
71
	    << "a counter-example" << std::endl
martinez's avatar
martinez committed
72
	    << "  -E    emptiness-check (Couvreur), expect no counter-example "
73
	    << std::endl
martinez's avatar
martinez committed
74
	    << "  -E2   emptiness-check (Couvreur variant), expect no "
75
	    << "counter-example " << std::endl
martinez's avatar
martinez committed
76
77
78
79
80
81
82
83
84
85
86
87
88
            << "  -f    use Couvreur's FM algorithm for translation"
	    << std::endl
            << "  -F    read the formula from the file" << std::endl
            << "  -L    fair-loop approximation (implies -f)" << std::endl
	    << "  -m    magic-search (implies -D), expect a counter-example"
	    << std::endl
	    << "  -ms   minmimal-search (implies -D), expect a counter-example"
	    << std::endl
	    << "  -mold magic-search (implies -D), expect a counter-example"
	    << std::endl
	    << "  -M    magic-search (implies -D), expect no counter-example"
	    << std::endl
	    << "  -Mold magic-search (implies -D), expect no counter-example"
89
	    << std::endl
martinez's avatar
martinez committed
90
91
	    << "  -ndfs nesteddfs-search (implies -D), expect a "
	    << "counter-example"
92
	    << std::endl
martinez's avatar
martinez committed
93
94
	    << "  -Ndfs nesteddfs-search (implies -D), expect no "
	    << "counter-example"
95
	    << std::endl
martinez's avatar
martinez committed
96
97
	    << "  -ndfs2 modify-nesteddfs-search (implies -D), "
	    << "expect a counter-example"
98
	    << std::endl
martinez's avatar
martinez committed
99
100
101
102
103
104
	    << "  -Ndfs2 modify-nesteddfs-search (implies -D), "
	    << "expect no counter-example"
	    << std::endl
	    << "  -n    same as -m, but display more counter-examples"
	    << std::endl
	    << "  -N    display the never clain for Spin "
105
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
106
107
            << "  -p    branching postponement (implies -f)" << std::endl
	    << "  -r    display the relation BDD, not the reachability graph"
108
	    << std::endl
martinez's avatar
martinez committed
109
110
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
111
	    << "and universality" << std::endl
martinez's avatar
martinez committed
112
	    << "  -r3   reduce formula using implication between "
113
	    << "sub-formulae" << std::endl
martinez's avatar
martinez committed
114
115
116
117
	    << "  -r4   reduce formula using all rules" << std::endl
	    << "  -rd   display the reduce formula" << std::endl
	    << "  -R    same as -r, but as a set" << std::endl
	    << "  -R1   use direct simulation to reduce the automata "
martinez's avatar
martinez committed
118
	    << "(use -L for more reduction)"
119
	    << std::endl
martinez's avatar
martinez committed
120
	    << "  -R2   use delayed simulation to reduce the automata "
martinez's avatar
martinez committed
121
	    << "(use -L for more reduction)"
122
	    << std::endl
martinez's avatar
martinez committed
123
	    << "  -R3   use SCC to reduce the automata"
124
	    << std::endl
martinez's avatar
martinez committed
125
	    << "  -Rd   display the simulation relation"
126
	    << std::endl
martinez's avatar
martinez committed
127
	    << "  -RD   display the parity game (dot format)"
128
	    << std::endl
martinez's avatar
martinez committed
129
	    << "  -s    convert to explicit automata, and number states "
130
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
131
	    << "  -S    convert to explicit automata, and number states "
132
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
133
134
135
136
137
138
	    << "  -t    display reachable states in LBTT's format" << std::endl
	    << "  -T    display reachable states in LBTT's format w/o "
	    << "acceptance conditions" << std::endl
	    << "  -tj   tarjan-on-fly (implies -D), expect a counter-example"
	    << std::endl
	    << "  -TJ   tarjan-on-fly (implies -D), expect no counter-example"
139
	    << std::endl
martinez's avatar
martinez committed
140
141
142
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
143
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
144
	    << "  -X    do not compute an automaton, read it from a file"
145
	    << std::endl
martinez's avatar
martinez committed
146
	    << "  -y    do not merge states with same symbolic representation "
147
	    << "(implies -f)" << std::endl;
148
149
150
151
152
153
154
155
  exit(2);
}

int
main(int argc, char** argv)
{
  int exit_code = 0;

156
  bool debug_opt = false;
157
  bool degeneralize_opt = false;
158
  bool fm_opt = false;
159
  bool fm_exprop_opt = false;
160
  bool fm_symb_merge_opt = true;
161
  bool file_opt = false;
162
  int output = 0;
163
  int formula_index = 0;
martinez's avatar
martinez committed
164
165
166
167
168
169
  enum { None, Couvreur, Couvreur2, MagicSearch, MagicSearchOld,
	 NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch,
	 TarjanOnFly, MinimalSearch} echeck = None;
  spot::emptyness_search* es = 0;
  //int opt_search = 0; //FIXME
  spot::search_opt opt_nested_search = spot::magic;
170
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
171
172
  bool magic_many = false;
  bool expect_counter_example = false;
173
  bool from_file = false;
174
  int reduc_aut = spot::Reduce_None;
175
  int redopt = spot::ltl::Reduce_None;
176
177
  bool display_reduce_form = false;
  bool display_rel_sim = false;
178
  bool display_parity_game = false;
179
  bool post_branching = false;
180
  bool fair_loop_approx = false;
181

182
  for (;;)
183
    {
184
      if (argc < formula_index + 2)
185
	syntax(argv[0]);
186
187
188

      ++formula_index;

189
190
191
192
193
194
195
196
      if (!strcmp(argv[formula_index], "-a"))
	{
	  output = 2;
	}
      else if (!strcmp(argv[formula_index], "-A"))
	{
	  output = 4;
	}
martinez's avatar
martinez committed
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  echeck = ColorDFSSearch;
	  //opt_search = 0;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	  magic_many = false;
	}
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  echeck = ColorDFSSearch;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
213
      else if (!strcmp(argv[formula_index], "-d"))
214
215
216
	{
	  debug_opt = true;
	}
217
218
219
220
      else if (!strcmp(argv[formula_index], "-D"))
	{
	  degeneralize_opt = true;
	}
221
222
223
224
225
226
      else if (!strcmp(argv[formula_index], "-e"))
	{
	  echeck = Couvreur;
	  expect_counter_example = true;
	  output = -1;
	}
227
228
229
230
231
232
      else if (!strcmp(argv[formula_index], "-e2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = true;
	  output = -1;
	}
233
234
235
236
237
238
      else if (!strcmp(argv[formula_index], "-E"))
	{
	  echeck = Couvreur;
	  expect_counter_example = false;
	  output = -1;
	}
239
240
241
242
243
244
      else if (!strcmp(argv[formula_index], "-E2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = false;
	  output = -1;
	}
245
246
247
248
249
250
251
252
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
253
254
255
256
257
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
martinez's avatar
martinez committed
258
259
260
261
262
263
264
265
      else if (!strcmp(argv[formula_index], "-mold"))
	{
	  echeck = MagicSearchOld;
	  //opt_search = 0;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
266
267
      else if (!strcmp(argv[formula_index], "-m"))
	{
martinez's avatar
martinez committed
268
	  opt_nested_search = spot::magic;
269
	  echeck = MagicSearch;
martinez's avatar
martinez committed
270
	  //opt_search = 0;
271
272
273
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
martinez's avatar
martinez committed
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
	  //magic_many = true;
	}
      else if (!strcmp(argv[formula_index], "-ms"))
	{
	  echeck = MinimalSearch;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-Mold"))
	{
	  echeck = MagicSearchOld; // FIXME
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
289
290
291
	}
      else if (!strcmp(argv[formula_index], "-M"))
	{
martinez's avatar
martinez committed
292
	  opt_nested_search = spot::magic;
293
294
295
296
297
	  echeck = MagicSearch;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
martinez's avatar
martinez committed
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
330
331
332
333
334
335
336
337
338
339
340
      else if (!strcmp(argv[formula_index], "-Ms"))
	{
	  echeck = MinimalSearch;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-ndfs"))
	{
	  opt_nested_search = spot::nested;
	  echeck = NestedDFSSearch;
	  //opt_search = 1;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-Ndfs"))
	{
	  opt_nested_search = spot::nested;
	  echeck = NestedDFSSearch;
	  //opt_search = 1;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-ndfs2"))
	{
	  opt_nested_search = spot::my_nested;
	  echeck = NestedDFSSearchModify;
	  //opt_search = 2;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-Ndfs2"))
	{
	  opt_nested_search = spot::my_nested;
	  echeck = NestedDFSSearchModify;
	  //opt_search = 2;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
341
342
      else if (!strcmp(argv[formula_index], "-n"))
	{
martinez's avatar
martinez committed
343
	  echeck = MagicSearchOld;
344
345
346
347
348
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	  magic_many = true;
	}
349
350
351
352
353
      else if (!strcmp(argv[formula_index], "-N"))
	{
	  degeneralize_opt = true;
	  output = 8;
	}
354
355
356
357
358
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
359
360
      else if (!strcmp(argv[formula_index], "-r"))
	{
361
362
	  output = 1;
	}
363
364
365
366
367
368
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
369
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
370
371
372
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
373
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
374
375
376
377
378
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
379
380
381
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
382
	}
383
384
      else if (!strcmp(argv[formula_index], "-R1"))
	{
martinez's avatar
martinez committed
385
	  //degeneralize_opt = true; // FIXME
386
387
388
389
	  reduc_aut |= spot::Reduce_Dir_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R2"))
	{
martinez's avatar
martinez committed
390
	  //degeneralize_opt = true; // FIXME
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
	  reduc_aut |= spot::Reduce_Del_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	}
      else if (!strcmp(argv[formula_index], "-rd"))
	{
	  display_reduce_form = true;
	}
      else if (!strcmp(argv[formula_index], "-Rd"))
	{
	  display_rel_sim = true;
	}
      else if (!strcmp(argv[formula_index], "-RD"))
	{
	  display_parity_game = true;
	}
409
410
411
412
413
414
415
416
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
417
418
419
420
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
martinez's avatar
martinez committed
421
422
423
424
425
426
427
428
429
430
431
432
433
434
      else if (!strcmp(argv[formula_index], "-tj"))
	{
	  echeck = TarjanOnFly;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-TJ"))
	{
	  echeck = TarjanOnFly;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
435
436
437
438
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
439
440
441
442
443
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
444
445
446
447
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
448
449
450
451
452
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
453
454
455
456
      else
	{
	  break;
	}
457
458
    }

459
460
461
462
  std::string input;

  if (file_opt)
    {
463
      if (strcmp(argv[formula_index], "-"))
464
	{
465
	  std::ifstream fin(argv[formula_index]);
466
	  if (!fin)
467
468
469
470
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
471

472
	  if (!std::getline(fin, input, '\0'))
473
474
475
476
477
478
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
479
	{
480
	  std::getline(std::cin, input, '\0');
481
482
483
484
485
486
487
	}
    }
  else
    {
      input = argv[formula_index];
    }

488
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
489
  spot::bdd_dict* dict = new spot::bdd_dict();
490
491
492
493
494
495
496
497
498

  spot::ltl::formula* f = 0;
  if (!from_file)
    {
      spot::ltl::parse_error_list pel;
      f = spot::ltl::parse(input, pel, env, debug_opt);
      exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
    }
  if (f || from_file)
499
    {
500
501
502
503
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

504
505
506
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
507
508
	  spot::tgba_explicit* e;
	  to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
509
510
	  if (spot::format_tgba_parse_errors(std::cerr, pel))
	    return 2;
511
	  e->merge_transitions();
512
	}
513
      else
514
	{
515
	  if (redopt != spot::ltl::Reduce_None)
516
	    {
517
518
519
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
520
521
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
522
	    }
523

524
	  if (fm_opt)
525
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
526
					       fm_symb_merge_opt,
527
528
					       post_branching,
					       fair_loop_approx);
529
530
531
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
532

533
534
535
536
      spot::tgba_tba_proxy* degeneralized = 0;
      if (degeneralize_opt)
	a = degeneralized = new spot::tgba_tba_proxy(a);

537
538
539
540
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
541
542
543
544

	  if (reduc_aut & spot::Reduce_Scc)
	    aut_red->prune_scc();

545
546
547
548
549
	  if ((reduc_aut & spot::Reduce_Dir_Sim) ||
	      (reduc_aut & spot::Reduce_Del_Sim))
	    {
	      spot::simulation_relation* rel;
	      if (reduc_aut & spot::Reduce_Dir_Sim)
550
551
552
		rel = spot::get_direct_relation_simulation(a,
							   std::cout,
							   display_parity_game);
553
	      else if (reduc_aut & spot::Reduce_Del_Sim)
554
555
556
		rel = spot::get_delayed_relation_simulation(a,
							    std::cout,
							    display_parity_game);
557
	      else
558
559
560
561
562
		{
		  assert(0);
		  // Please GCC so it does not think REL is unused.
		  rel = 0;
		}
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577

	      if (display_rel_sim)
		aut_red->display_rel_sim(rel, std::cout);

	      if (reduc_aut & spot::Reduce_Dir_Sim)
		aut_red->prune_automata(rel);
	      else if (reduc_aut & spot::Reduce_Del_Sim)
		aut_red->quotient_state(rel);
	      else
		assert(0);

	      spot::free_relation_simulation(rel);
	    }
	}

578
579
580
581
582
583
584
585
586
587
588
589
590
      spot::tgba_explicit* expl = 0;
      switch (dupexp)
	{
	case NoneDup:
	  break;
	case BFS:
	  a = expl = tgba_dupexp_bfs(a);
	  break;
	case DFS:
	  a = expl = tgba_dupexp_dfs(a);
	  break;
	}

591
592
      switch (output)
	{
593
594
595
	case -1:
	  /* No output.  */
	  break;
596
597
598
599
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
600
601
602
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
603
604
	  break;
	case 2:
605
606
607
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
608
				get_core_data().acceptance_conditions);
609
610
	  break;
	case 3:
611
612
613
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
614
615
	  break;
	case 4:
616
617
618
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
619
				get_core_data().acceptance_conditions);
620
	  break;
621
	case 5:
622
	  a->get_dict()->dump(std::cout);
623
	  break;
624
625
626
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
627
628
629
	case 8:
	  spot::never_claim_reachable(std::cout, degeneralized, f);
	  break;
630
631
632
	default:
	  assert(!"unknown output option");
	}
633

634
635
636
637
      switch (echeck)
	{
	case None:
	  break;
martinez's avatar
martinez committed
638

639
	case Couvreur:
640
	case Couvreur2:
641
	  {
642
	    spot::emptiness_check* ec;
643
	    if (echeck == Couvreur)
644
	      ec = new spot::emptiness_check(a);
645
	    else
646
647
	      ec = new spot::emptiness_check_shy(a);
	    bool res = ec->check();
648
649
650
651
652
	    if (expect_counter_example)
	      {
		if (res)
		  {
		    exit_code = 1;
653
		    delete ec;
654
655
		    break;
		  }
656
		spot::counter_example ce(ec->result());
martinez's avatar
martinez committed
657
658
659
660
661
662
		//ce.print_result(std::cout);
		spot::ce::counter_example* res2 = ce.get_counter_example();
		spot::tgba* aut = res2->ce2tgba();
		spot::dotty_reachable(std::cout, aut);
		delete res2;
		delete aut;
663
664
665
666
667
	      }
	    else
	      {
		exit_code = !res;
	      }
668
	    delete ec;
669
670
	  }
	  break;
martinez's avatar
martinez committed
671
672

	case MagicSearchOld:
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
	  {
	    spot::magic_search ms(degeneralized);
	    bool res = ms.check();
	    if (expect_counter_example)
	      {
		if (!res)
		  {
		    exit_code = 1;
		    break;
		  }
		do
		  ms.print_result(std::cout);
		while (magic_many && ms.check());
	      }
	    else
	      {
		exit_code = res;
	      }
	  }
	  break;
martinez's avatar
martinez committed
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750

	case ColorDFSSearch:
	  es = new spot::colordfs_search(degeneralized);
	  break;

	case TarjanOnFly:
	  es = new spot::tarjan_on_fly(degeneralized);
	  break;

	case MinimalSearch:
	  es = new spot::minimalce_search(degeneralized);
	  break;

	case MagicSearch:
	case NestedDFSSearch:
	case NestedDFSSearchModify:
	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
	  break;

	}

      if (es)
	{
	  spot::ce::counter_example* res = es->check();
	  if (expect_counter_example)
	    {
	      do
		{
		  if (!res)
		    {
		      exit_code = 1;
		      break;
		    }
		  std::cout << "CE : " << std::endl
			    << "     size : " << res->size()
			    << std::endl;
		  spot::tgba* aut = res->ce2tgba();
		  //spot::dotty_reachable(std::cout, aut);
		  res->print(std::cout);
		  es->print_stat(std::cout);
		  delete aut;
		  delete res;
		  res = 0;
		}
	      while (magic_many && (res = es->check()));
	    }
	  else if (res)
	    {
	      exit_code = res->size();
	      std::cout << "res->size ?? : " << exit_code << std::endl;
	    }
	  else
	    {
	      exit_code = (res != 0);
	      std::cout << "res != 0 ?? : " << exit_code << std::endl;
	    }
	  if (res)
	    delete res;
751
752
	}

martinez's avatar
martinez committed
753
754
      if (es)
	delete es;
755
756
      if (f)
        spot::ltl::destroy(f);
757
758
      if (expl)
	delete expl;
759
760
      if (degeneralize_opt)
	delete degeneralized;
761
762
      if (aut_red)
	delete aut_red;
763

764
      delete to_free;
765
766
767
768
769
770
771
772
773
774
    }
  else
    {
      exit_code = 1;
    }

  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);
775
  delete dict;
776
777
  return exit_code;
}