ltl2tgba.cc 26.3 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
	    << "  couvreur99 (the default)" << std::endl
137
	    << "  couvreur99_shy-" << std::endl
138
139
	    << "  couvreur99_shy" << std::endl
	    << "  magic_search" << std::endl
140
	    << "  magic_search_repeated" << std::endl
141
142
143
144
	    << "  bsh_magic_search[(heap size in Mo - 10Mo by default)]"
            << std::endl
	    << "  bsh_magic_search_repeated[(heap size in MB - 10MB"
            << " by default)]" << std::endl
145
	    << "  gv04" << std::endl
146
	    << "  se05_search" << std::endl
147
148
149
150
	    << "  se05_search_repeated" << std::endl
	    << "  bsh_se05_search[(heap size in MB - 10MB by default)]"
            << std::endl
	    << "  bsh_se05_search_repeated[(heap size in MB - 10MB"
151
            << " by default)]" << std::endl
152
153
	    << "  tau03_search" << std::endl
	    << "  tau03_opt_search" << std::endl;
154
155
156
157
158
159
160
161
  exit(2);
}

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

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

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

      ++formula_index;

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

413
  if (echeck_algo != "")
414
    {
415
416
417
418
419
420
421
      if (echeck_algo == "couvreur99")
	{
	  echeck = Couvreur;
	}
      else if (echeck_algo == "couvreur99_shy")
	{
	  echeck = Couvreur2;
422
423
424
425
426
427
	  couv_group = true;
	}
      else if (echeck_algo == "couvreur99_shy-")
	{
	  echeck = Couvreur2;
	  couv_group = false;
428
429
430
431
	}
      else if (echeck_algo == "magic_search")
	{
	  echeck = MagicSearch;
432
	  degeneralize_maybe = true;
433
434
435
436
	}
      else if (echeck_algo == "magic_search_repeated")
	{
	  echeck = MagicSearch;
437
	  degeneralize_maybe = true;
438
	  search_many = true;
439
	}
440
441
442
      else if (echeck_algo == "bsh_magic_search")
	{
	  echeck = MagicSearch;
443
	  degeneralize_maybe = true;
444
445
446
447
448
          bit_state_hashing = true;
	}
      else if (echeck_algo == "bsh_magic_search_repeated")
	{
	  echeck = MagicSearch;
449
	  degeneralize_maybe = true;
450
          bit_state_hashing = true;
451
	  search_many = true;
452
	}
453
454
      else if (echeck_algo == "se05_search")
	{
455
	  echeck = Se05Search;
456
	  degeneralize_maybe = true;
457
458
459
	}
      else if (echeck_algo == "se05_search_repeated")
	{
460
	  echeck = Se05Search;
461
	  degeneralize_maybe = true;
462
	  search_many = true;
463
464
465
466
	}
      else if (echeck_algo == "bsh_se05_search")
	{
	  echeck = Se05Search;
467
	  degeneralize_maybe = true;
468
469
470
471
472
          bit_state_hashing = true;
	}
      else if (echeck_algo == "bsh_se05_search_repeated")
	{
	  echeck = Se05Search;
473
	  degeneralize_maybe = true;
474
          bit_state_hashing = true;
475
476
477
478
479
	  search_many = true;
	}
      else if (echeck_algo == "tau03_search")
	{
	  echeck = Tau03Search;
480
	}
481
482
483
484
      else if (echeck_algo == "tau03_opt_search")
	{
	  echeck = Tau03OptSearch;
	}
485
486
487
488
489
      else if (echeck_algo == "gv04")
	{
	  echeck = Gv04;
	  degeneralize_maybe = true;
	}
490
491
492
493
494
      else
	{
	  std::cerr << "unknown emptiness-check: " << echeck_algo << std::endl;
	  syntax(argv[0]);
	}
495
496
    }

497
498
  if ((graph_run_opt || graph_run_tgba_opt)
      && (echeck_algo == "" || !expect_counter_example))
499
    {
500
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
501
502
503
      exit(1);
    }

504
505
506
507
  std::string input;

  if (file_opt)
    {
508
      if (strcmp(argv[formula_index], "-"))
509
	{
510
	  std::ifstream fin(argv[formula_index]);
511
	  if (!fin)
512
513
514
515
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
516

517
	  if (!std::getline(fin, input, '\0'))
518
519
520
521
522
523
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
524
	{
525
	  std::getline(std::cin, input, '\0');
526
527
528
529
530
531
532
	}
    }
  else
    {
      input = argv[formula_index];
    }

533
534
535
536
537
538
539
540
  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)
541
    {
542
543
544
545
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

570
	  if (fm_opt)
571
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
572
					       fm_symb_merge_opt,
573
					       post_branching,
574
					       fair_loop_approx, unobservables);
575
576
577
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
578

579
      spot::tgba_tba_proxy* degeneralized = 0;
580

581
582
583
584
585
      if (degeneralize_maybe
	  && degeneralize_opt == NoDegen
	  && a->number_of_acceptance_conditions() > 1)
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
586
	a = degeneralized = new spot::tgba_tba_proxy(a);
587
588
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
589

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

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

martinez's avatar
martinez committed
598
599
600
601
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
602
	    {
martinez's avatar
martinez committed
603
604
605
606
607
	      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))
608
609
610
611
		rel_dir =
		  spot::get_direct_relation_simulation(a,
						       std::cout,
						       display_parity_game);
martinez's avatar
martinez committed
612
613
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
614
615
616
617
		rel_del =
		  spot::get_delayed_relation_simulation(a,
							std::cout,
							display_parity_game);
618
619

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

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

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

656
657
      spot::tgba* product_degeneralized = 0;

658
      if (system)
659
660
661
662
663
664
665
666
667
668
669
670
671
        {
          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);
        }
672

673
674
      switch (output)
	{
675
676
677
	case -1:
	  /* No output.  */
	  break;
678
679
680
681
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
682
683
684
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
685
686
	  break;
	case 2:
687
688
689
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
690
				get_core_data().acceptance_conditions);
691
692
	  break;
	case 3:
693
694
695
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
696
697
	  break;
	case 4:
698
699
700
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
701
				get_core_data().acceptance_conditions);
702
	  break;
703
	case 5:
704
	  a->get_dict()->dump(std::cout);
705
	  break;
706
707
708
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
709
710
711
	case 7:
	  spot::tgba_save_reachable(std::cout, a);
	  break;
712
	case 8:
713
714
715
716
717
718
719
	  {
	    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;
	  }
720
721
722
	default:
	  assert(!"unknown output option");
	}
723

724
      spot::emptiness_check* ec = 0;
725
726
727
728
      switch (echeck)
	{
	case None:
	  break;
martinez's avatar
martinez committed
729

730
	case Couvreur:
731
732
733
	  ec = new spot::couvreur99_check(a);
	  break;

734
	case Couvreur2:
735
	  ec = new spot::couvreur99_check_shy(a, couv_group);
736
	  break;
martinez's avatar
martinez committed
737

738
739
        case MagicSearch:
          if (bit_state_hashing)
740
            ec = spot::bit_state_hashing_magic_search(a, heap_size);
741
          else
742
            ec = spot::explicit_magic_search(a);
743
          break;
744

745
746
        case Se05Search:
          if (bit_state_hashing)
747
            ec = spot::bit_state_hashing_se05_search(a, heap_size);
748
          else
749
            ec = spot::explicit_se05_search(a);
750
          break;
751
752
753
754

	case Tau03Search:
          if (a->number_of_acceptance_conditions() == 0)
            {
755
756
757
758
759
760
              if (!paper_opt)
                std::cout << "To apply tau03_search, the automaton must have at"
                          << " least one accepting condition. Try with another"
                          << " algorithm." << std::endl;
              else
                std::cout << std::endl;
761
762
763
764
765
            }
          else
            {
              ec = spot::explicit_tau03_search(a);
            }
766
          break;
767
	case Tau03OptSearch:
768
          ec = spot::explicit_tau03_opt_search(a);
769
	  break;
770
771
772
	case Gv04:
	  ec = spot::explicit_gv04_check(a);
	  break;
773
	}
martinez's avatar
martinez committed
774

775
776
777
778
779
      if (ec)
	{
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
              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
804
                    std::cout << "no stats, , ";
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
                  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)
821
                    {
822
823
824
825
826
827
828
829
830
831
832
833
                      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;
834
                    }
835
836
                  else
                    {
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
863
864
865
866
867
868
869
870
871
872
873
                      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;
                        }
                    }
                }
874
875
	      delete res;
	    }
876
	  while (search_many);
877
	  delete ec;
martinez's avatar
martinez committed
878
879
	}

880
881
      if (f)
        spot::ltl::destroy(f);
882
883
      delete product_degeneralized;
      delete product_to_free;
884
      delete system;
885
886
887
      delete expl;
      delete degeneralized;
      delete aut_red;
888
      delete to_free;
889
890
891
892
893
894
895
896
897
898
    }
  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);
899
  delete dict;
900
901
  return exit_code;
}