ltl2tgba.cc 22.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
#include "tgbaalgos/nesteddfs.hh"
martinez's avatar
martinez committed
39
#include "tgbaalgos/nesteddfsgen.hh"
martinez's avatar
martinez committed
40
41
42
#include "tgbaalgos/colordfs.hh"
#include "tgbaalgos/tarjan_on_fly.hh"
//#include "tgbaalgos/minimalce.hh"
43
44
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
45
#include "tgbaparse/public.hh"
46
#include "tgbaalgos/dupexp.hh"
47
#include "tgbaalgos/neverclaim.hh"
48

49
50
#include "tgbaalgos/reductgba_sim.hh"

51
52
53
void
syntax(char* prog)
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
54
  std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl
55
            << "       "<< prog << " -F [OPTIONS...] file" << std::endl
56
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
57
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
58
	    << "Options:" << std::endl
martinez's avatar
martinez committed
59
	    << "  -a    display the acceptance_conditions BDD, not the "
60
	    << "reachability graph"
61
	    << std::endl
martinez's avatar
martinez committed
62
63
64
65
66
67
68
69
	    << "  -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 "
70
	    << "a counter-example" << std::endl
martinez's avatar
martinez committed
71
	    << "  -e2   emptiness-check (Couvreur variant), expect and compute "
72
	    << "a counter-example" << std::endl
martinez's avatar
martinez committed
73
	    << "  -E    emptiness-check (Couvreur), expect no counter-example "
74
	    << std::endl
martinez's avatar
martinez committed
75
	    << "  -E2   emptiness-check (Couvreur variant), expect no "
76
	    << "counter-example " << std::endl
martinez's avatar
martinez committed
77
78
79
80
81
82
83
84
            << "  -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
martinez's avatar
martinez committed
85
86
	    << "  -msit minmimal-search (implies -D), expect a counter-example"
	    << std::endl
martinez's avatar
martinez committed
87
88
89
90
91
	    << "  -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"
92
	    << std::endl
martinez's avatar
martinez committed
93
94
95
96
	    << "  -n    same as -m, but display more counter-examples"
	    << std::endl
	    << "  -N    display the never clain for Spin "
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
97
98
	    << "  -ndfs nesteddfs-search (implies -D), expect a "
	    << "counter-example"
99
	    << std::endl
martinez's avatar
martinez committed
100
101
	    << "  -Ndfs nesteddfs-search (implies -D), expect no "
	    << "counter-example"
102
	    << std::endl
martinez's avatar
martinez committed
103
104
	    << "  -ndfs2 modify-nesteddfs-search (implies -D), "
	    << "expect a counter-example"
105
	    << std::endl
martinez's avatar
martinez committed
106
107
108
	    << "  -Ndfs2 modify-nesteddfs-search (implies -D), "
	    << "expect no counter-example"
	    << std::endl
martinez's avatar
martinez committed
109
110
111
112
113
	    << "  -ng   nesteddfs-search generalized (implies -D), expect a "
	    << "counter-example"
	    << std::endl
	    << "  -NG   nesteddfs-search generalized (implies -D), expect no "
	    << "counter-example"
martinez's avatar
martinez committed
114
115
116
	    << std::endl
            << "  -p    branching postponement (implies -f)" << std::endl
	    << "  -r    display the relation BDD, not the reachability graph"
117
	    << std::endl
martinez's avatar
martinez committed
118
119
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
120
	    << "and universality" << std::endl
martinez's avatar
martinez committed
121
	    << "  -r3   reduce formula using implication between "
122
	    << "sub-formulae" << std::endl
martinez's avatar
martinez committed
123
124
125
	    << "  -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
martinez's avatar
martinez committed
126
	    << "  -R1q  use direct simulation to merge some state "
martinez's avatar
martinez committed
127
	    << "(use -L for more reduction)"
128
	    << std::endl
martinez's avatar
martinez committed
129
	    << "  -R1t  use direct simulation to remove some transition "
martinez's avatar
martinez committed
130
	    << "(use -L for more reduction)"
131
	    << std::endl
martinez's avatar
martinez committed
132
133
134
135
136
137
	    << "  -R2q  use delayed simulation to merge some state "
	    << "(the automaton must be degeneralised)"
	    << std::endl
	    << "  -R2t  use delayed simulation to remove some transition "
	    << "(the automaton must be degeneralised)"
	    << std::endl
martinez's avatar
martinez committed
138
	    << "  -R3   use SCC to reduce the automata"
139
	    << std::endl
martinez's avatar
martinez committed
140
	    << "  -Rd   display the simulation relation"
141
	    << std::endl
martinez's avatar
martinez committed
142
	    << "  -RD   display the parity game (dot format)"
143
	    << std::endl
martinez's avatar
martinez committed
144
	    << "  -s    convert to explicit automata, and number states "
145
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
146
	    << "  -S    convert to explicit automata, and number states "
147
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
148
149
150
151
152
153
	    << "  -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"
154
	    << std::endl
martinez's avatar
martinez committed
155
156
157
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
158
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
159
	    << "  -X    do not compute an automaton, read it from a file"
160
	    << std::endl
martinez's avatar
martinez committed
161
	    << "  -y    do not merge states with same symbolic representation "
162
	    << "(implies -f)" << std::endl;
163
164
165
166
167
168
169
170
  exit(2);
}

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

171
  bool debug_opt = false;
172
  bool degeneralize_opt = false;
173
  bool fm_opt = false;
174
  bool fm_exprop_opt = false;
175
  bool fm_symb_merge_opt = true;
176
  bool file_opt = false;
177
  int output = 0;
178
  int formula_index = 0;
martinez's avatar
martinez committed
179
180
  enum { None, Couvreur, Couvreur2, MagicSearch, MagicSearchOld,
	 NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch,
martinez's avatar
martinez committed
181
182
	 TarjanOnFly, MinimalSearch, MinimalSearchIterative,
	 NestedGeneSearch} echeck = None;
183
  spot::emptiness_search* es = 0;
martinez's avatar
martinez committed
184
  spot::search_opt opt_nested_search = spot::magic;
185
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
186
187
  bool magic_many = false;
  bool expect_counter_example = false;
188
  bool from_file = false;
189
  int reduc_aut = spot::Reduce_None;
190
  int redopt = spot::ltl::Reduce_None;
191
192
  bool display_reduce_form = false;
  bool display_rel_sim = false;
193
  bool display_parity_game = false;
194
  bool post_branching = false;
195
  bool fair_loop_approx = false;
196

197
  for (;;)
198
    {
199
      if (argc < formula_index + 2)
200
	syntax(argv[0]);
201
202
203

      ++formula_index;

204
205
206
207
208
209
210
211
      if (!strcmp(argv[formula_index], "-a"))
	{
	  output = 2;
	}
      else if (!strcmp(argv[formula_index], "-A"))
	{
	  output = 4;
	}
martinez's avatar
martinez committed
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  echeck = ColorDFSSearch;
	  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;
	}
227
      else if (!strcmp(argv[formula_index], "-d"))
228
229
230
	{
	  debug_opt = true;
	}
231
232
233
234
      else if (!strcmp(argv[formula_index], "-D"))
	{
	  degeneralize_opt = true;
	}
235
236
237
238
239
240
      else if (!strcmp(argv[formula_index], "-e"))
	{
	  echeck = Couvreur;
	  expect_counter_example = true;
	  output = -1;
	}
241
242
243
244
245
246
      else if (!strcmp(argv[formula_index], "-e2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = true;
	  output = -1;
	}
247
248
249
250
251
252
      else if (!strcmp(argv[formula_index], "-E"))
	{
	  echeck = Couvreur;
	  expect_counter_example = false;
	  output = -1;
	}
253
254
255
256
257
258
      else if (!strcmp(argv[formula_index], "-E2"))
	{
	  echeck = Couvreur2;
	  expect_counter_example = false;
	  output = -1;
	}
259
260
261
262
263
264
265
266
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
267
268
269
270
271
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
martinez's avatar
martinez committed
272
      else if (!strcmp(argv[formula_index], "-m"))
martinez's avatar
martinez committed
273
	{
martinez's avatar
martinez committed
274
275
	  opt_nested_search = spot::magic;
	  echeck = MagicSearch;
martinez's avatar
martinez committed
276
277
278
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
martinez's avatar
martinez committed
279
	  magic_many = true;
martinez's avatar
martinez committed
280
	}
martinez's avatar
martinez committed
281
      else if (!strcmp(argv[formula_index], "-M"))
282
	{
martinez's avatar
martinez committed
283
	  opt_nested_search = spot::magic;
284
285
	  echeck = MagicSearch;
	  degeneralize_opt = true;
martinez's avatar
martinez committed
286
	  expect_counter_example = false;
287
	  output = -1;
martinez's avatar
martinez committed
288
	}
martinez's avatar
martinez committed
289
      else if (!strcmp(argv[formula_index], "-mold"))
martinez's avatar
martinez committed
290
	{
martinez's avatar
martinez committed
291
	  echeck = MagicSearchOld;
martinez's avatar
martinez committed
292
293
294
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
martinez's avatar
martinez committed
295
	  magic_many = true;
martinez's avatar
martinez committed
296
297
298
	}
      else if (!strcmp(argv[formula_index], "-Mold"))
	{
martinez's avatar
martinez committed
299
	  echeck = MagicSearchOld;
martinez's avatar
martinez committed
300
301
302
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
303
	}
martinez's avatar
martinez committed
304
      else if (!strcmp(argv[formula_index], "-ms"))
305
	{
martinez's avatar
martinez committed
306
	  echeck = MinimalSearch;
307
	  degeneralize_opt = true;
martinez's avatar
martinez committed
308
	  expect_counter_example = true;
309
310
	  output = -1;
	}
martinez's avatar
martinez committed
311
312
313
314
315
316
317
      else if (!strcmp(argv[formula_index], "-Ms"))
	{
	  echeck = MinimalSearch;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
martinez's avatar
martinez committed
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
      else if (!strcmp(argv[formula_index], "-msit"))
	{
	  echeck = MinimalSearchIterative;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  magic_many = true;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-n"))
	{
	  echeck = MagicSearchOld;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	  magic_many = true;
	}
      else if (!strcmp(argv[formula_index], "-N"))
	{
	  degeneralize_opt = true;
	  output = 8;
	}
martinez's avatar
martinez committed
339
340
341
342
343
344
345
      else if (!strcmp(argv[formula_index], "-ndfs"))
	{
	  opt_nested_search = spot::nested;
	  echeck = NestedDFSSearch;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
martinez's avatar
martinez committed
346
	  magic_many = true;
martinez's avatar
martinez committed
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
	}
      else if (!strcmp(argv[formula_index], "-Ndfs"))
	{
	  opt_nested_search = spot::nested;
	  echeck = NestedDFSSearch;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-ndfs2"))
	{
	  opt_nested_search = spot::my_nested;
	  echeck = NestedDFSSearchModify;
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
      else if (!strcmp(argv[formula_index], "-Ndfs2"))
	{
	  opt_nested_search = spot::my_nested;
	  echeck = NestedDFSSearchModify;
	  degeneralize_opt = true;
	  expect_counter_example = false;
	  output = -1;
	}
martinez's avatar
martinez committed
372
      else if (!strcmp(argv[formula_index], "-ng"))
373
	{
martinez's avatar
martinez committed
374
	  echeck = NestedGeneSearch;
375
376
377
378
	  degeneralize_opt = true;
	  expect_counter_example = true;
	  output = -1;
	}
martinez's avatar
martinez committed
379
      else if (!strcmp(argv[formula_index], "-NG"))
380
	{
martinez's avatar
martinez committed
381
	  echeck = NestedGeneSearch;
382
	  degeneralize_opt = true;
martinez's avatar
martinez committed
383
384
	  expect_counter_example = false;
	  output = -1;
385
	}
386
387
388
389
390
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
391
392
      else if (!strcmp(argv[formula_index], "-r"))
	{
393
394
	  output = 1;
	}
395
396
397
398
399
400
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
401
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
402
403
404
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
405
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
406
407
408
409
410
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
411
412
413
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
414
	}
martinez's avatar
martinez committed
415
416
417
418
419
420
421
422
423
      else if (!strcmp(argv[formula_index], "-R1q"))
	{
	  reduc_aut |= spot::Reduce_quotient_Dir_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R1t"))
	{
	  reduc_aut |= spot::Reduce_transition_Dir_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R2q"))
424
	{
martinez's avatar
martinez committed
425
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
426
	}
martinez's avatar
martinez committed
427
      else if (!strcmp(argv[formula_index], "-R2t"))
428
	{
martinez's avatar
martinez committed
429
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
	}
      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;
	}
447
448
449
450
451
452
453
454
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
455
456
457
458
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
martinez's avatar
martinez committed
459
460
461
462
463
464
465
466
467
468
469
470
471
472
      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;
	}
473
474
475
476
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
477
478
479
480
481
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
482
483
484
485
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
486
487
488
489
490
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
491
492
493
494
      else
	{
	  break;
	}
495
496
    }

497
498
499
500
  std::string input;

  if (file_opt)
    {
501
      if (strcmp(argv[formula_index], "-"))
502
	{
503
	  std::ifstream fin(argv[formula_index]);
504
	  if (!fin)
505
506
507
508
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
509

510
	  if (!std::getline(fin, input, '\0'))
511
512
513
514
515
516
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
517
	{
518
	  std::getline(std::cin, input, '\0');
519
520
521
522
523
524
525
	}
    }
  else
    {
      input = argv[formula_index];
    }

526
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
527
  spot::bdd_dict* dict = new spot::bdd_dict();
528
529
530
531
532
533
534
535
536

  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)
537
    {
538
539
540
541
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

542
543
544
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
545
546
	  spot::tgba_explicit* e;
	  to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
547
548
	  if (spot::format_tgba_parse_errors(std::cerr, pel))
	    return 2;
549
	  e->merge_transitions();
550
	}
551
      else
552
	{
553
	  if (redopt != spot::ltl::Reduce_None)
554
	    {
555
556
557
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
558
559
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
560
	    }
561

562
	  if (fm_opt)
563
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
564
					       fm_symb_merge_opt,
565
566
					       post_branching,
					       fair_loop_approx);
567
568
569
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
570

571
572
573
574
      spot::tgba_tba_proxy* degeneralized = 0;
      if (degeneralize_opt)
	a = degeneralized = new spot::tgba_tba_proxy(a);

575
576
577
578
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
579
580
581
582

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

martinez's avatar
martinez committed
583
584
585
586
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
587
	    {
martinez's avatar
martinez committed
588
589
590
591
592
593
594
595
596
597
598
599
600
	      spot::direct_simulation_relation* rel_dir = 0;
	      spot::delayed_simulation_relation* rel_del = 0;

	      if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			       spot::Reduce_transition_Dir_Sim))
		rel_dir = spot::get_direct_relation_simulation(a,
							       std::cout,
							       display_parity_game);
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
		rel_del = spot::get_delayed_relation_simulation(a,
								std::cout,
								display_parity_game);
601
602

	      if (display_rel_sim)
martinez's avatar
martinez committed
603
604
605
606
607
608
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
609

martinez's avatar
martinez committed
610
611
612
613
614
615
616
617
618
619
620
621
622
	      if (reduc_aut & spot::Reduce_quotient_Dir_Sim)
		aut_red->quotient_state(rel_dir);
	      if (reduc_aut & spot::Reduce_transition_Dir_Sim)
		aut_red->delete_transitions(rel_dir);
	      if (reduc_aut & spot::Reduce_quotient_Del_Sim)
		aut_red->quotient_state(rel_del);
	      if (reduc_aut & spot::Reduce_transition_Del_Sim)
		aut_red->delete_transitions(rel_del);

	      if (rel_dir)
		spot::free_relation_simulation(rel_dir);
	      if (rel_del)
		spot::free_relation_simulation(rel_del);
623
624
625
	    }
	}

626
627
628
629
630
631
632
633
634
635
636
637
638
      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;
	}

639
640
      switch (output)
	{
641
642
643
	case -1:
	  /* No output.  */
	  break;
644
645
646
647
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
648
649
650
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
651
652
	  break;
	case 2:
653
654
655
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
656
				get_core_data().acceptance_conditions);
657
658
	  break;
	case 3:
659
660
661
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
662
663
	  break;
	case 4:
664
665
666
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
667
				get_core_data().acceptance_conditions);
668
	  break;
669
	case 5:
670
	  a->get_dict()->dump(std::cout);
671
	  break;
672
673
674
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
675
676
677
	case 8:
	  spot::never_claim_reachable(std::cout, degeneralized, f);
	  break;
678
679
680
	default:
	  assert(!"unknown output option");
	}
681

682
683
684
685
      switch (echeck)
	{
	case None:
	  break;
martinez's avatar
martinez committed
686

687
	case Couvreur:
688
	case Couvreur2:
689
	  {
martinez's avatar
martinez committed
690
	    std::cout << "Tarjan Couvreur" << std::endl;
691
	    spot::emptiness_check* ec;
692
	    if (echeck == Couvreur)
693
	      ec = new spot::emptiness_check(a);
694
	    else
695
696
	      ec = new spot::emptiness_check_shy(a);
	    bool res = ec->check();
697
698
699
700
701
	    if (expect_counter_example)
	      {
		if (res)
		  {
		    exit_code = 1;
702
		    delete ec;
703
704
		    break;
		  }
705
		spot::counter_example ce(ec->result());
martinez's avatar
martinez committed
706
707
708
709
710
711
712
713
714
715
		ce.print_result(std::cout);
		ce.print_stats(std::cout);

		//spot::ce::counter_example* res2 = ce.get_counter_example();
		//spot::tgba* aut = res2->ce2tgba();
		//spot::dotty_reachable(std::cout, aut);
		//res2->print(std::cout);
		//delete res2;
		//delete aut;

716
717
718
719
720
	      }
	    else
	      {
		exit_code = !res;
	      }
721
	    delete ec;
722
723
	  }
	  break;
martinez's avatar
martinez committed
724

martinez's avatar
martinez committed
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
	case NestedGeneSearch:
	  {
	    std::cout << "Nested DFS generalized" << std::endl;
	    spot::nesteddfsgen_search* ec = new spot::nesteddfsgen_search(a);
	    bool res = ec->check();
	    ec->print_stats(std::cout);
	    if (expect_counter_example)
	      {
		if (!res)
		  exit_code = 1;
	      }
	    else
	      {
		exit_code = res;
	      }
	    delete ec;
	  }
	  break;

martinez's avatar
martinez committed
744
	case MagicSearchOld:
745
	  {
martinez's avatar
martinez committed
746
	    std::cout << "Magic Search" << std::endl;
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
	    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
766
767

	case ColorDFSSearch:
martinez's avatar
martinez committed
768
	  std::cout << "Colored Search" << std::endl;
martinez's avatar
martinez committed
769
770
771
772
	  es = new spot::colordfs_search(degeneralized);
	  break;

	case TarjanOnFly:
martinez's avatar
martinez committed
773
	  std::cout << "Tarjan On Fly" << std::endl;
martinez's avatar
martinez committed
774
775
776
777
	  es = new spot::tarjan_on_fly(degeneralized);
	  break;

	case MinimalSearch:
martinez's avatar
martinez committed
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
	  {
	    std::cout << "Recursive Minimal Search" << std::endl;
	    es = new spot::colordfs_search(degeneralized);
	    spot::ce::counter_example* res = es->check();
	    res->print(std::cout);
	    std::cout << "Minimisation:" << std::endl;
	    es = new spot::minimalce_search(degeneralized, false);
	    res = es->check();
	    res->print(std::cout);
	  }
	  break;

	case MinimalSearchIterative:
	    std::cout << "Iterative Minimal Search" << std::endl;
	  es = new spot::minimalce_search(degeneralized, true);
martinez's avatar
martinez committed
793
794
795
	  break;

	case MagicSearch:
martinez's avatar
martinez committed
796
797
798
799
	  std::cout << "Magic Search" << std::endl;
	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
	  break;

martinez's avatar
martinez committed
800
801
	case NestedDFSSearch:
	case NestedDFSSearchModify:
martinez's avatar
martinez committed
802
	  std::cout << "Nested DFS" << std::endl;
martinez's avatar
martinez committed
803
804
805
	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
	  break;

martinez's avatar
martinez committed
806
807
	default:
	  assert(0);
martinez's avatar
martinez committed
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
	}

      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;
847
848
	}

martinez's avatar
martinez committed
849

martinez's avatar
martinez committed
850
851
      if (es)
	delete es;
852
853
      if (f)
        spot::ltl::destroy(f);
854
855
      if (expl)
	delete expl;
856
857
      if (degeneralize_opt)
	delete degeneralized;
858
859
      if (aut_red)
	delete aut_red;
860

861
      delete to_free;
862
863
864
865
866
867
868
869
870
871
    }
  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);
872
  delete dict;
873
874
  return exit_code;
}