ltl2tgba.cc 23.2 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
#include "ltlvisit/apcollect.hh"
30
31
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
32
#include "tgbaalgos/ltl2tgba_lacim.hh"
33
#include "tgbaalgos/ltl2tgba_fm.hh"
34
#include "tgba/bddprint.hh"
35
#include "tgbaalgos/dotty.hh"
36
#include "tgbaalgos/lbtt.hh"
37
#include "tgba/tgbatba.hh"
38
#include "tgbaalgos/magic.hh"
martinez's avatar
martinez committed
39
#include "tgbaalgos/nesteddfs.hh"
martinez's avatar
martinez committed
40
#include "tgbaalgos/nesteddfsgen.hh"
martinez's avatar
martinez committed
41
42
43
#include "tgbaalgos/colordfs.hh"
#include "tgbaalgos/tarjan_on_fly.hh"
//#include "tgbaalgos/minimalce.hh"
44
45
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
46
#include "tgbaparse/public.hh"
47
#include "tgbaalgos/dupexp.hh"
48
#include "tgbaalgos/neverclaim.hh"
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
155
156
            << "  -U[PROPS]  consider atomic properties PROPS as exclusive "
	    << "events (implies -f)" << std::endl
martinez's avatar
martinez committed
157
158
159
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
160
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
161
	    << "  -X    do not compute an automaton, read it from a file"
162
	    << std::endl
martinez's avatar
martinez committed
163
	    << "  -y    do not merge states with same symbolic representation "
164
	    << "(implies -f)" << std::endl;
165
166
167
168
169
170
171
172
  exit(2);
}

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

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

201
  for (;;)
202
    {
203
      if (argc < formula_index + 2)
204
	syntax(argv[0]);
205
206
207

      ++formula_index;

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

514
515
516
517
  std::string input;

  if (file_opt)
    {
518
      if (strcmp(argv[formula_index], "-"))
519
	{
520
	  std::ifstream fin(argv[formula_index]);
521
	  if (!fin)
522
523
524
525
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
526

527
	  if (!std::getline(fin, input, '\0'))
528
529
530
531
532
533
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
534
	{
535
	  std::getline(std::cin, input, '\0');
536
537
538
539
540
541
542
	}
    }
  else
    {
      input = argv[formula_index];
    }

543
  spot::bdd_dict* dict = new spot::bdd_dict();
544
545
546
547
548
549
550
551
552

  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)
553
    {
554
555
556
557
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

558
559
560
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
561
562
	  spot::tgba_explicit* e;
	  to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
563
564
	  if (spot::format_tgba_parse_errors(std::cerr, pel))
	    return 2;
565
	  e->merge_transitions();
566
	}
567
      else
568
	{
569
	  if (redopt != spot::ltl::Reduce_None)
570
	    {
571
572
573
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
574
575
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
576
	    }
577

578
	  if (fm_opt)
579
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
580
					       fm_symb_merge_opt,
581
					       post_branching,
582
					       fair_loop_approx, unobservables);
583
584
585
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
586

587
588
589
590
      spot::tgba_tba_proxy* degeneralized = 0;
      if (degeneralize_opt)
	a = degeneralized = new spot::tgba_tba_proxy(a);

591
592
593
594
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
595
596
597
598

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

martinez's avatar
martinez committed
599
600
601
602
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
603
	    {
martinez's avatar
martinez committed
604
605
606
607
608
609
610
611
612
613
614
615
616
	      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);
617
618

	      if (display_rel_sim)
martinez's avatar
martinez committed
619
620
621
622
623
624
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
625

martinez's avatar
martinez committed
626
627
628
629
630
631
632
633
634
635
636
637
638
	      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);
639
640
641
	    }
	}

642
643
644
645
646
647
648
649
650
651
652
653
654
      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;
	}

655
656
      switch (output)
	{
657
658
659
	case -1:
	  /* No output.  */
	  break;
660
661
662
663
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
664
665
666
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
667
668
	  break;
	case 2:
669
670
671
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
672
				get_core_data().acceptance_conditions);
673
674
	  break;
	case 3:
675
676
677
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
678
679
	  break;
	case 4:
680
681
682
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
683
				get_core_data().acceptance_conditions);
684
	  break;
685
	case 5:
686
	  a->get_dict()->dump(std::cout);
687
	  break;
688
689
690
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
691
692
693
	case 8:
	  spot::never_claim_reachable(std::cout, degeneralized, f);
	  break;
694
695
696
	default:
	  assert(!"unknown output option");
	}
697

698
699
700
701
      switch (echeck)
	{
	case None:
	  break;
martinez's avatar
martinez committed
702

703
	case Couvreur:
704
	case Couvreur2:
705
	  {
martinez's avatar
martinez committed
706
	    std::cout << "Tarjan Couvreur" << std::endl;
707
	    spot::emptiness_check* ec;
708
	    if (echeck == Couvreur)
709
	      ec = new spot::emptiness_check(a);
710
	    else
711
712
	      ec = new spot::emptiness_check_shy(a);
	    bool res = ec->check();
713
714
715
716
717
	    if (expect_counter_example)
	      {
		if (res)
		  {
		    exit_code = 1;
718
		    delete ec;
719
720
		    break;
		  }
721
		spot::counter_example ce(ec->result());
martinez's avatar
martinez committed
722
723
724
725
726
727
728
729
730
731
		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;

732
733
734
735
736
	      }
	    else
	      {
		exit_code = !res;
	      }
737
	    delete ec;
738
739
	  }
	  break;
martinez's avatar
martinez committed
740

martinez's avatar
martinez committed
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
	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
760
	case MagicSearchOld:
761
	  {
martinez's avatar
martinez committed
762
	    std::cout << "Magic Search" << std::endl;
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
	    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
782
783

	case ColorDFSSearch:
martinez's avatar
martinez committed
784
	  std::cout << "Colored Search" << std::endl;
martinez's avatar
martinez committed
785
786
787
788
	  es = new spot::colordfs_search(degeneralized);
	  break;

	case TarjanOnFly:
martinez's avatar
martinez committed
789
	  std::cout << "Tarjan On Fly" << std::endl;
martinez's avatar
martinez committed
790
791
792
793
	  es = new spot::tarjan_on_fly(degeneralized);
	  break;

	case MinimalSearch:
martinez's avatar
martinez committed
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
	  {
	    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
809
810
811
	  break;

	case MagicSearch:
martinez's avatar
martinez committed
812
813
814
815
	  std::cout << "Magic Search" << std::endl;
	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
	  break;

martinez's avatar
martinez committed
816
817
	case NestedDFSSearch:
	case NestedDFSSearchModify:
martinez's avatar
martinez committed
818
	  std::cout << "Nested DFS" << std::endl;
martinez's avatar
martinez committed
819
820
821
	  es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
	  break;

martinez's avatar
martinez committed
822
823
	default:
	  assert(0);
martinez's avatar
martinez committed
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
	}

      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;
863
864
	}

martinez's avatar
martinez committed
865

martinez's avatar
martinez committed
866
867
      if (es)
	delete es;
868
869
      if (f)
        spot::ltl::destroy(f);
870
871
      if (expl)
	delete expl;
872
873
      if (degeneralize_opt)
	delete degeneralized;
874
875
      if (aut_red)
	delete aut_red;
876

877
      delete to_free;
878
879
880
881
882
883
884
885
886
887
    }
  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);
888
  delete dict;
889
890
  return exit_code;
}