ltl2tgba.cc 26.6 KB
Newer Older
1
// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// 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
#include <iostream>
23
#include <iomanip>
24
#include <cassert>
25
26
#include <fstream>
#include <string>
27
#include "ltlvisit/destroy.hh"
28
#include "ltlvisit/reduce.hh"
29
#include "ltlvisit/tostring.hh"
30
#include "ltlvisit/apcollect.hh"
31
32
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
33
#include "tgbaalgos/ltl2tgba_lacim.hh"
34
#include "tgbaalgos/ltl2tgba_fm.hh"
35
#include "tgba/bddprint.hh"
36
#include "tgbaalgos/save.hh"
37
#include "tgbaalgos/dotty.hh"
38
#include "tgbaalgos/lbtt.hh"
39
#include "tgba/tgbatba.hh"
40
#include "tgba/tgbaproduct.hh"
41
#include "tgbaalgos/gv04.hh"
42
#include "tgbaalgos/magic.hh"
43
#include "tgbaalgos/reducerun.hh"
44
45
#include "tgbaalgos/se05.hh"
#include "tgbaalgos/tau03.hh"
46
#include "tgbaalgos/tau03opt.hh"
47
48
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
49
#include "tgbaparse/public.hh"
50
#include "tgbaalgos/dupexp.hh"
51
#include "tgbaalgos/neverclaim.hh"
52
#include "tgbaalgos/reductgba_sim.hh"
53
#include "tgbaalgos/replayrun.hh"
54
#include "tgbaalgos/rundotdec.hh"
55

56
57
58
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/emptiness_stats.hh"

59
60
61
void
syntax(char* prog)
{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
62
  std::cerr << "Usage: "<< prog << " [OPTIONS...] formula" << std::endl
63
            << "       "<< prog << " -F [OPTIONS...] file" << std::endl
64
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
65
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
66
	    << "Options:" << std::endl
67
68
	    << "  -0    produce minimal output dedicated to the paper"
	    << std::endl
martinez's avatar
martinez committed
69
	    << "  -a    display the acceptance_conditions BDD, not the "
70
	    << "reachability graph"
71
	    << std::endl
martinez's avatar
martinez committed
72
	    << "  -A    same as -a, but as a set" << std::endl
73
74
	    << "  -b    display the automaton in the format of spot"
            << std::endl
martinez's avatar
martinez committed
75
	    << "  -d    turn on traces during parsing" << std::endl
76
77
	    << "  -D    degeneralize the automaton as a TBA" << std::endl
	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
78
79
80
	    << "  -e[ALGO]  emptiness-check, expect and compute an "
	    << "accepting run" << std::endl
	    << "  -E[ALGO]  emptiness-check, expect no accepting run"
81
	    << std::endl
martinez's avatar
martinez committed
82
83
84
            << "  -f    use Couvreur's FM algorithm for translation"
	    << std::endl
            << "  -F    read the formula from the file" << std::endl
85
	    << "  -g    graph the accepting run on the automaton (requires -e)"
86
	    << std::endl
87
88
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
martinez's avatar
martinez committed
89
            << "  -L    fair-loop approximation (implies -f)" << std::endl
90
	    << "  -m    try to reduce accepting runs, in a second pass"
91
	    << std::endl
martinez's avatar
martinez committed
92
93
	    << "  -N    display the never clain for Spin "
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
94
            << "  -p    branching postponement (implies -f)" << std::endl
95
96
	    << "  -Pfile  multiply the formula with the automaton from `file'."
	    << std::endl
martinez's avatar
martinez committed
97
	    << "  -r    display the relation BDD, not the reachability graph"
98
	    << std::endl
martinez's avatar
martinez committed
99
100
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
101
	    << "and universality" << std::endl
martinez's avatar
martinez committed
102
	    << "  -r3   reduce formula using implication between "
103
	    << "sub-formulae" << std::endl
martinez's avatar
martinez committed
104
105
106
	    << "  -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
107
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
108
	    << "(use -L for more reduction)"
109
	    << std::endl
110
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
111
	    << "(use -L for more reduction)"
112
	    << std::endl
113
114
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
115
	    << std::endl
116
117
118
	    << "  -R3   use SCC to reduce the automata" << std::endl
	    << "  -Rd   display the simulation relation" << std::endl
	    << "  -RD   display the parity game (dot format)" << std::endl
martinez's avatar
martinez committed
119
	    << "  -s    convert to explicit automata, and number states "
120
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
121
	    << "  -S    convert to explicit automata, and number states "
122
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
123
	    << "  -t    display reachable states in LBTT's format" << std::endl
124
125
            << "  -U[PROPS]  consider atomic properties PROPS as exclusive "
	    << "events (implies -f)" << std::endl
martinez's avatar
martinez committed
126
127
128
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
129
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
130
	    << "  -X    do not compute an automaton, read it from a file"
131
	    << std::endl
martinez's avatar
martinez committed
132
	    << "  -y    do not merge states with same symbolic representation "
133
134
135
	    << "(implies -f)" << std::endl
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
136
137
138
	    << "  Cou99 (the default)" << std::endl
	    << "  Cou99_shy-" << std::endl
	    << "  Cou99_shy" << std::endl
139
140
141
	    << "  Cou99_rem" << std::endl
	    << "  Cou99_rem_shy-" << std::endl
	    << "  Cou99_rem_shy" << std::endl
142
143
144
	    << "  CVWY90" << std::endl
	    << "  CVWY90_repeated" << std::endl
	    << "  CVWY90_bsh[(heap size in Mo - 10Mo by default)]"
145
            << std::endl
146
	    << "  CVWY90_bsh_repeated[(heap size in MB - 10MB"
147
            << " by default)]" << std::endl
148
149
150
151
	    << "  GV04" << std::endl
	    << "  SE05" << std::endl
	    << "  SE05_repeated" << std::endl
	    << "  SE05_bsh[(heap size in MB - 10MB by default)]"
152
            << std::endl
153
	    << "  SE05_bsh_repeated[(heap size in MB - 10MB"
154
            << " by default)]" << std::endl
155
156
	    << "  Tau03" << std::endl
	    << "  Tau03_opt" << std::endl;
157
158
159
160
161
162
163
164
  exit(2);
}

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

165
  bool debug_opt = false;
166
  bool paper_opt = false;
167
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
168
  bool degeneralize_maybe = false;
169
  bool fm_opt = false;
170
  bool fm_exprop_opt = false;
171
  bool fm_symb_merge_opt = true;
172
  bool file_opt = false;
173
  int output = 0;
174
  int formula_index = 0;
175
  std::string echeck_algo;
176
  enum { None, Couvreur, Couvreur2, MagicSearch, Se05Search,
177
	 Tau03Search, Tau03OptSearch, Gv04 } echeck = None;
178
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
179
  bool couv_group = true;
180
  bool poprem = false;
181
  bool search_many = false;
182
183
  bool bit_state_hashing = false;
  int heap_size = 10*1024*1024;
184
  bool expect_counter_example = false;
185
  bool from_file = false;
186
  int reduc_aut = spot::Reduce_None;
187
  int redopt = spot::ltl::Reduce_None;
188
189
  bool display_reduce_form = false;
  bool display_rel_sim = false;
190
  bool display_parity_game = false;
191
  bool post_branching = false;
192
  bool fair_loop_approx = false;
193
  bool graph_run_opt = false;
194
  bool graph_run_tgba_opt = false;
195
  bool opt_reduce = false;
196
197
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
198
199
  spot::tgba_explicit* system = 0;
  spot::tgba* product = 0;
200
  spot::tgba* product_to_free = 0;
201
  spot::bdd_dict* dict = new spot::bdd_dict();
202

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

      ++formula_index;

210
211
212
213
214
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
215
216
217
	{
	  output = 2;
	}
218
      else if (!strcmp(argv[formula_index], "-A"))
219
	{
220
	  output = 4;
221
	}
222
      else if (!strcmp(argv[formula_index], "-b"))
223
	{
224
	  output = 7;
225
226
	}
      else if (!strcmp(argv[formula_index], "-d"))
227
228
229
	{
	  debug_opt = true;
	}
230
231
      else if (!strcmp(argv[formula_index], "-D"))
	{
232
233
234
235
236
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
237
	}
238
      else if (!strncmp(argv[formula_index], "-e", 2))
239
240
241
242
243
244
245
246
247
        {
          if (argv[formula_index][2] != 0)
            {
              char *p = strchr(argv[formula_index], '(');
              if (p && sscanf(p+1, "%d)", &heap_size) == 1)
                *p = '\0';
              echeck_algo = argv[formula_index] + 2;
            }
          else
248
            echeck_algo = "Cou99";
249
250
251
          expect_counter_example = true;
          output = -1;
        }
252
      else if (!strncmp(argv[formula_index], "-E", 2))
253
254
255
256
257
258
259
260
261
        {
          if (argv[formula_index][2] != 0)
            {
              char *p = strchr(argv[formula_index], '(');
              if (p && sscanf(p+1, "%d)", &heap_size) == 1)
                *p = '\0';
              echeck_algo = argv[formula_index] + 2;
            }
          else
262
            echeck_algo = "Cou99";
263
264
265
          expect_counter_example = false;
          output = -1;
        }
266
267
268
269
270
271
272
273
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
274
275
276
277
      else if (!strcmp(argv[formula_index], "-g"))
	{
	  graph_run_opt = true;
	}
278
279
280
281
      else if (!strcmp(argv[formula_index], "-G"))
	{
	  graph_run_tgba_opt = true;
	}
282
283
284
285
286
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
287
288
      else if (!strcmp(argv[formula_index], "-m"))
	{
289
	  opt_reduce = true;
290
	}
martinez's avatar
martinez committed
291
292
      else if (!strcmp(argv[formula_index], "-N"))
	{
293
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
294
295
	  output = 8;
	}
296
297
298
299
300
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
301
302
303
304
305
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
				     pel, dict, env, debug_opt);
306
307
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
308
309
310
311
	    return 2;
	  system->merge_transitions();
	  std::clog << argv[formula_index] + 2 << " read" << std::endl;
	}
312
313
      else if (!strcmp(argv[formula_index], "-r"))
	{
314
315
	  output = 1;
	}
316
317
318
319
320
321
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
322
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
323
324
325
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
326
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
327
328
329
330
331
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
332
333
334
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
335
	}
martinez's avatar
martinez committed
336
337
338
339
340
341
342
343
344
      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"))
345
	{
martinez's avatar
martinez committed
346
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
347
	}
martinez's avatar
martinez committed
348
      else if (!strcmp(argv[formula_index], "-R2t"))
349
	{
martinez's avatar
martinez committed
350
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
	}
      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;
	}
368
369
370
371
372
373
374
375
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
376
377
378
379
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
380
381
382
383
384
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
	  fm_opt = true;
	  // Parse -U's argument.
385
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
386
387
388
389
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
390
	      tok = strtok(0, ", \t;");
391
392
	    }
	}
393
394
395
396
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
397
398
399
400
401
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
402
403
404
405
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
406
407
408
409
410
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
411
412
413
414
      else
	{
	  break;
	}
415
416
    }

417
  if (echeck_algo != "")
418
    {
419
      if (echeck_algo == "Cou99")
420
421
422
	{
	  echeck = Couvreur;
	}
423
      else if (echeck_algo == "Cou99_shy")
424
425
	{
	  echeck = Couvreur2;
426
427
	  couv_group = true;
	}
428
      else if (echeck_algo == "Cou99_shy-")
429
430
431
	{
	  echeck = Couvreur2;
	  couv_group = false;
432
	}
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
      else if (echeck_algo == "Cou99_rem")
	{
	  echeck = Couvreur;
	  poprem = true;
	}
      else if (echeck_algo == "Cou99_rem_shy")
	{
	  echeck = Couvreur2;
	  couv_group = true;
	  poprem = true;
	}
      else if (echeck_algo == "Cou99_rem_shy-")
	{
	  echeck = Couvreur2;
	  couv_group = false;
	  poprem = true;
	}
450
      else if (echeck_algo == "CVWY90")
451
452
	{
	  echeck = MagicSearch;
453
	  degeneralize_maybe = true;
454
	}
455
      else if (echeck_algo == "CVWY90_repeated")
456
457
	{
	  echeck = MagicSearch;
458
	  degeneralize_maybe = true;
459
	  search_many = true;
460
	}
461
      else if (echeck_algo == "CVWY90_bsh")
462
463
	{
	  echeck = MagicSearch;
464
	  degeneralize_maybe = true;
465
466
          bit_state_hashing = true;
	}
467
      else if (echeck_algo == "CVWY90_bsh_repeated")
468
469
	{
	  echeck = MagicSearch;
470
	  degeneralize_maybe = true;
471
          bit_state_hashing = true;
472
	  search_many = true;
473
	}
474
      else if (echeck_algo == "SE05")
475
	{
476
	  echeck = Se05Search;
477
	  degeneralize_maybe = true;
478
	}
479
      else if (echeck_algo == "SE05_repeated")
480
	{
481
	  echeck = Se05Search;
482
	  degeneralize_maybe = true;
483
	  search_many = true;
484
	}
485
      else if (echeck_algo == "SE05_bsh")
486
487
	{
	  echeck = Se05Search;
488
	  degeneralize_maybe = true;
489
490
          bit_state_hashing = true;
	}
491
      else if (echeck_algo == "SE05_bsh_repeated")
492
493
	{
	  echeck = Se05Search;
494
	  degeneralize_maybe = true;
495
          bit_state_hashing = true;
496
497
	  search_many = true;
	}
498
      else if (echeck_algo == "Tau03")
499
500
	{
	  echeck = Tau03Search;
501
	}
502
      else if (echeck_algo == "Tau03_opt")
503
504
505
	{
	  echeck = Tau03OptSearch;
	}
506
      else if (echeck_algo == "GV04")
507
508
509
510
	{
	  echeck = Gv04;
	  degeneralize_maybe = true;
	}
511
512
513
514
515
      else
	{
	  std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl;
	  syntax(argv[0]);
	}
516
517
    }

518
519
  if ((graph_run_opt || graph_run_tgba_opt)
      && (echeck_algo == "" || !expect_counter_example))
520
    {
521
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
522
523
524
      exit(1);
    }

525
526
527
528
  std::string input;

  if (file_opt)
    {
529
      if (strcmp(argv[formula_index], "-"))
530
	{
531
	  std::ifstream fin(argv[formula_index]);
532
	  if (!fin)
533
534
535
536
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
537

538
	  if (!std::getline(fin, input, '\0'))
539
540
541
542
543
544
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
545
	{
546
	  std::getline(std::cin, input, '\0');
547
548
549
550
551
552
553
	}
    }
  else
    {
      input = argv[formula_index];
    }

554
555
556
557
558
559
560
561
  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)
562
    {
563
564
565
566
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

567
568
569
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
570
571
	  spot::tgba_explicit* e;
	  to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
572
	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
573
574
575
576
577
	    {
	      delete to_free;
	      delete dict;
	      return 2;
	    }
578
	  e->merge_transitions();
579
	}
580
      else
581
	{
582
	  if (redopt != spot::ltl::Reduce_None)
583
	    {
584
585
586
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
587
588
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
589
	    }
590

591
	  if (fm_opt)
592
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
593
					       fm_symb_merge_opt,
594
					       post_branching,
595
					       fair_loop_approx, unobservables);
596
597
598
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
599

600
      spot::tgba_tba_proxy* degeneralized = 0;
601

602
603
604
605
606
      if (degeneralize_maybe
	  && degeneralize_opt == NoDegen
	  && a->number_of_acceptance_conditions() > 1)
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
607
	a = degeneralized = new spot::tgba_tba_proxy(a);
608
609
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
610

611
612
613
614
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
615
616
617
618

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

martinez's avatar
martinez committed
619
620
621
622
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
623
	    {
martinez's avatar
martinez committed
624
625
626
627
628
	      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))
629
630
631
632
		rel_dir =
		  spot::get_direct_relation_simulation(a,
						       std::cout,
						       display_parity_game);
martinez's avatar
martinez committed
633
634
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
635
636
637
638
		rel_del =
		  spot::get_delayed_relation_simulation(a,
							std::cout,
							display_parity_game);
639
640

	      if (display_rel_sim)
martinez's avatar
martinez committed
641
642
643
644
645
646
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
647

martinez's avatar
martinez committed
648
649
650
651
652
653
654
655
656
657
658
659
660
	      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);
661
662
663
	    }
	}

664
665
666
667
668
669
670
671
672
673
674
675
676
      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;
	}

677
678
      spot::tgba* product_degeneralized = 0;

679
      if (system)
680
681
682
683
684
685
686
687
688
689
690
691
692
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
          if (degeneralize_maybe
              && degeneralize_opt == NoDegen
              && product->number_of_acceptance_conditions() > 1)
            degeneralize_opt = DegenTBA;
          if (degeneralize_opt == DegenTBA)
            a = product = product_degeneralized =
                                            new spot::tgba_tba_proxy(product);
          else if (degeneralize_opt == DegenSBA)
            a = product = product_degeneralized =
                                            new spot::tgba_sba_proxy(product);
        }
693

694
695
      switch (output)
	{
696
697
698
	case -1:
	  /* No output.  */
	  break;
699
700
701
702
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
703
704
705
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
706
707
	  break;
	case 2:
708
709
710
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
711
				get_core_data().acceptance_conditions);
712
713
	  break;
	case 3:
714
715
716
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
717
718
	  break;
	case 4:
719
720
721
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
722
				get_core_data().acceptance_conditions);
723
	  break;
724
	case 5:
725
	  a->get_dict()->dump(std::cout);
726
	  break;
727
728
729
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
730
731
732
	case 7:
	  spot::tgba_save_reachable(std::cout, a);
	  break;
733
	case 8:
734
735
736
737
738
739
740
	  {
	    assert(degeneralize_opt == DegenSBA);
	    const spot::tgba_sba_proxy* s =
	      static_cast<const spot::tgba_sba_proxy*>(degeneralized);
	    spot::never_claim_reachable(std::cout, s, f);
	    break;
	  }
741
742
743
	default:
	  assert(!"unknown output option");
	}
744

745
      spot::emptiness_check* ec = 0;
746
747
748
749
      switch (echeck)
	{
	case None:
	  break;
martinez's avatar
martinez committed
750

751
	case Couvreur:
752
	  ec = new spot::couvreur99_check(a, poprem);
753
754
	  break;

755
	case Couvreur2:
756
	  ec = new spot::couvreur99_check_shy(a, poprem, couv_group);
757
	  break;
martinez's avatar
martinez committed
758

759
760
        case MagicSearch:
          if (bit_state_hashing)
761
            ec = spot::bit_state_hashing_magic_search(a, heap_size);
762
          else
763
            ec = spot::explicit_magic_search(a);
764
          break;
765

766
767
        case Se05Search:
          if (bit_state_hashing)
768
            ec = spot::bit_state_hashing_se05_search(a, heap_size);
769
          else
770
            ec = spot::explicit_se05_search(a);
771
          break;
772
773
774
775

	case Tau03Search:
          if (a->number_of_acceptance_conditions() == 0)
            {
776
              if (!paper_opt)
777
                std::cout << "To apply Tau03, the automaton must have at"
778
779
780
781
                          << " least one accepting condition. Try with another"
                          << " algorithm." << std::endl;
              else
                std::cout << std::endl;
782
783
784
785
786
            }
          else
            {
              ec = spot::explicit_tau03_search(a);
            }
787
          break;
788
	case Tau03OptSearch:
789
          ec = spot::explicit_tau03_opt_search(a);
790
	  break;
791
792
793
	case Gv04:
	  ec = spot::explicit_gv04_check(a);
	  break;
794
	}
martinez's avatar
martinez committed
795

796
797
798
799
800
      if (ec)
	{
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
                  std::cout << std::left << std::setw(20)
                            << echeck_algo << ", ";
                  spot::tgba_statistics a_size =
                                        spot::stats_reachable(ec->automaton());
                  std::cout << std::right << std::setw(10)
                            << a_size.states << ", "
                            << std::right << std::setw(10)
                            << a_size.transitions << ", ";
                  std::cout <<
                            ec->automaton()->number_of_acceptance_conditions()
                            << ", ";
                  const spot::ec_statistics* ecs =
                        dynamic_cast<const spot::ec_statistics*>(ec);
                  if (ecs)
                    std::cout << std::right << std::setw(10)
                              << ecs->states() << ", "
                              << std::right << std::setw(10)
                              << ecs->transitions() << ", "
                              << std::right << std::setw(10)
                              << ecs->max_depth();
                  else
825
                    std::cout << "no stats, , ";
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
                  if (res)
                    std::cout << ", accepting run found";
                  else
                    std::cout << ", no accepting run found";
                  std::cout << std::endl;
                  std::cout << std::setiosflags(old);
                }
              else
                {
                  if (!graph_run_opt && !graph_run_tgba_opt)
                    ec->print_stats(std::cout);
                  if (expect_counter_example != !!res &&
                          (!bit_state_hashing || !expect_counter_example))
                    exit_code = 1;

                  if (!res)
842
                    {
843
844
845
846
847
848
849
850
851
852
853
854
                      std::cout << "no accepting run found";
                      if (bit_state_hashing && expect_counter_example)
                        {
                          std::cout << " even if expected" << std::endl;
                          std::cout << "this is maybe due to the use of the bit"
                                    << " state hashing technic" << std::endl;
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
855
                    }
856
857
                  else
                    {
858

859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
                      spot::tgba_run* run = res->accepting_run();
                      if (!run)
                        {
                          std::cout << "an accepting run exists" << std::endl;
                        }
                      else
                        {
                          if (opt_reduce)
                            {
                              spot::tgba_run* redrun =
                                spot::reduce_run(res->automaton(), run);
                              delete run;
                              run = redrun;
                            }
                          if (graph_run_opt)
                            {
                              spot::tgba_run_dotty_decorator deco(run);
                              spot::dotty_reachable(std::cout, a, &deco);
                            }
                          else if (graph_run_tgba_opt)
                            {
                              spot::tgba* ar = spot::tgba_run_to_tgba(a, run);
                              spot::dotty_reachable(std::cout, ar);
                              delete ar;
                            }
                          else
                            {
                              spot::print_tgba_run(std::cout, a, run);
                              if (!spot::replay_tgba_run(std::cout, a, run,
                                                                        true))
                                exit_code = 1;
                            }
                          delete run;
                        }
                    }
                }
895
896
	      delete res;
	    }
897
	  while (search_many);
898
	  delete ec;
martinez's avatar
martinez committed
899
900
	}

901
902
      if (f)
        spot::ltl::destroy(f);
903
904
      delete product_degeneralized;
      delete product_to_free;
905
      delete system;
906
907
908
      delete expl;
      delete degeneralized;
      delete aut_red;
909
      delete to_free;
910
911
912
913
914
915
916
917
918
919
    }
  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);
920
  delete dict;
921
922
  return exit_code;
}