ltl2tgba.cc 26.7 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
	    return 2;
	  system->merge_transitions();
310
311
312

	  if (!paper_opt)
	    std::clog << argv[formula_index] + 2 << " read" << std::endl;
313
	}
314
315
      else if (!strcmp(argv[formula_index], "-r"))
	{
316
317
	  output = 1;
	}
318
319
320
321
322
323
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
324
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
325
326
327
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
328
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
329
330
331
332
333
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
334
335
336
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
337
	}
martinez's avatar
martinez committed
338
339
340
341
342
343
344
345
346
      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"))
347
	{
martinez's avatar
martinez committed
348
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
349
	}
martinez's avatar
martinez committed
350
      else if (!strcmp(argv[formula_index], "-R2t"))
351
	{
martinez's avatar
martinez committed
352
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
	}
      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;
	}
370
371
372
373
374
375
376
377
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
378
379
380
381
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
382
383
384
385
386
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
	  fm_opt = true;
	  // Parse -U's argument.
387
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
388
389
390
391
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
392
	      tok = strtok(0, ", \t;");
393
394
	    }
	}
395
396
397
398
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
399
400
401
402
403
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
404
405
406
407
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
408
409
410
411
412
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
413
414
415
416
      else
	{
	  break;
	}
417
418
    }

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

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

527
528
529
530
  std::string input;

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

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

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

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

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

602
      spot::tgba_tba_proxy* degeneralized = 0;
603

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

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

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

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

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

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

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

679
680
      spot::tgba* product_degeneralized = 0;

681
      if (system)
682
683
684
685
686
687
688
689
690
691
692
693
694
        {
          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);
        }
695

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

747
748
749
750
      spot::option_map o;
      o.set("poprem", poprem);
      o.set("group", couv_group);

751
      spot::emptiness_check* ec = 0;
752
753
754
755
      switch (echeck)
	{
	case None:
	  break;
martinez's avatar
martinez committed
756

757
	case Couvreur:
758
	  ec = new spot::couvreur99_check(a, o);
759
760
	  break;

761
	case Couvreur2:
762
	  ec = new spot::couvreur99_check_shy(a, o);
763
	  break;
martinez's avatar
martinez committed
764

765
766
        case MagicSearch:
          if (bit_state_hashing)
767
            ec = spot::bit_state_hashing_magic_search(a, heap_size);
768
          else
769
            ec = spot::explicit_magic_search(a);
770
          break;
771

772
773
        case Se05Search:
          if (bit_state_hashing)
774
            ec = spot::bit_state_hashing_se05_search(a, heap_size);
775
          else
776
            ec = spot::explicit_se05_search(a);
777
          break;
778
779
780
781

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

802
803
804
805
806
      if (ec)
	{
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
              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
831
                    std::cout << "no stats, , ";
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
                  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)
848
                    {
849
850
851
852
853
854
855
856
857
858
859
860
                      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;
861
                    }
862
863
                  else
                    {
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
895
896
897
898
899
900
                      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;
                        }
                    }
                }
901
902
	      delete res;
	    }
903
	  while (search_many);
904
	  delete ec;
martinez's avatar
martinez committed
905
906
	}

907
908
      if (f)
        spot::ltl::destroy(f);
909
910
      delete product_degeneralized;
      delete product_to_free;
911
      delete system;
912
913
914
      delete expl;
      delete degeneralized;
      delete aut_red;
915
      delete to_free;
916
917
918
919
920
921
922
923
924
925
    }
  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);
926
  delete dict;
927
928
  return exit_code;
}