ltl2tgba.cc 26.3 KB
Newer Older
1
2
3
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008 Laboratoire
// d'Informatique de Paris 6 (LIP6), dpartement Systmes Rpartis
// Coopratifs (SRC), Universit Pierre et Marie Curie.
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
//
// 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 <cstdlib>
28
#include "ltlvisit/destroy.hh"
29
#include "ltlvisit/contain.hh"
30
#include "ltlvisit/tostring.hh"
31
#include "ltlvisit/apcollect.hh"
32
#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/reducerun.hh"
42
#include "tgbaparse/public.hh"
43
#include "tgbaalgos/dupexp.hh"
44
#include "tgbaalgos/neverclaim.hh"
45
#include "tgbaalgos/reductgba_sim.hh"
46
#include "tgbaalgos/replayrun.hh"
47
#include "tgbaalgos/rundotdec.hh"
48

49
#include "tgbaalgos/stats.hh"
50
#include "tgbaalgos/scc.hh"
51
52
#include "tgbaalgos/emptiness_stats.hh"

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

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

164
  bool debug_opt = false;
165
  bool paper_opt = false;
166
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
167
  bool fm_opt = false;
168
  int fm_red = spot::ltl::Reduce_None;
169
  bool fm_exprop_opt = false;
170
  bool fm_symb_merge_opt = true;
171
  bool file_opt = false;
172
  int output = 0;
173
  int formula_index = 0;
174
175
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
176
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
177
  bool expect_counter_example = false;
178
  bool from_file = false;
179
  int reduc_aut = spot::Reduce_None;
180
  int redopt = spot::ltl::Reduce_None;
181
182
  bool display_reduce_form = false;
  bool display_rel_sim = false;
183
  bool display_parity_game = false;
184
  bool post_branching = false;
185
  bool fair_loop_approx = false;
186
  bool graph_run_opt = false;
187
  bool graph_run_tgba_opt = false;
188
  bool opt_reduce = false;
189
  bool containment = false;
190
191
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
192
193
  spot::tgba_explicit* system = 0;
  spot::tgba* product = 0;
194
  spot::tgba* product_to_free = 0;
195
  spot::bdd_dict* dict = new spot::bdd_dict();
196

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

      ++formula_index;

204
205
206
207
208
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
209
210
211
	{
	  output = 2;
	}
212
      else if (!strcmp(argv[formula_index], "-A"))
213
	{
214
	  output = 4;
215
	}
216
      else if (!strcmp(argv[formula_index], "-b"))
217
	{
218
	  output = 7;
219
	}
220
221
222
223
224
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
	  fm_opt = true;
	}
225
      else if (!strcmp(argv[formula_index], "-d"))
226
227
228
	{
	  debug_opt = true;
	}
229
230
      else if (!strcmp(argv[formula_index], "-D"))
	{
231
232
233
234
235
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
236
	}
237
      else if (!strncmp(argv[formula_index], "-e", 2))
238
        {
239
240
241
242
243
244
245
246
247
248
249
250
251
	  echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
	    spot::emptiness_check_instantiator::construct(echeck_algo, &err);
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
			<< err <<  "'" << std::endl;
	      exit(2);
	    }
252
253
254
          expect_counter_example = true;
          output = -1;
        }
255
      else if (!strncmp(argv[formula_index], "-E", 2))
256
        {
257
258
259
260
261
262
263
264
265
266
267
268
269
	  const char* echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
	    spot::emptiness_check_instantiator::construct(echeck_algo, &err);
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
			<< err <<  "'" << std::endl;
	      exit(2);
	    }
270
271
272
          expect_counter_example = false;
          output = -1;
        }
273
274
275
276
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
      else if (!strcmp(argv[formula_index], "-fr1"))
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-fr2"))
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_Eventuality_And_Universality;
	}
      else if (!strcmp(argv[formula_index], "-fr3"))
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr4"))
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
	{
	  fm_opt = true;
 	  fm_red |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr5"))
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_Containment_Checks;
	}
      else if (!strcmp(argv[formula_index], "-fr6"))
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger;
	}
      else if (!strcmp(argv[formula_index], "-fr7"))
310
311
312
313
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_All;
	}
314
315
316
317
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
318
319
320
321
      else if (!strcmp(argv[formula_index], "-g"))
	{
	  graph_run_opt = true;
	}
322
323
324
325
      else if (!strcmp(argv[formula_index], "-G"))
	{
	  graph_run_tgba_opt = true;
	}
326
327
328
329
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
330
331
332
333
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
334
335
336
337
338
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
339
340
      else if (!strcmp(argv[formula_index], "-m"))
	{
341
	  opt_reduce = true;
342
	}
martinez's avatar
martinez committed
343
344
      else if (!strcmp(argv[formula_index], "-N"))
	{
345
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
346
347
	  output = 8;
	}
348
349
350
351
352
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
353
354
355
356
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
357
				    pel, dict, env, env, debug_opt);
358
359
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
360
361
	    return 2;
	  system->merge_transitions();
362
363
364

	  if (!paper_opt)
	    std::clog << argv[formula_index] + 2 << " read" << std::endl;
365
	}
366
367
      else if (!strcmp(argv[formula_index], "-r"))
	{
368
369
	  output = 1;
	}
370
371
372
373
374
375
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
376
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
377
378
379
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
380
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
381
382
383
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
384
385
386
 	  redopt |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
387
	}
388
389
      else if (!strcmp(argv[formula_index], "-r5"))
	{
390
	  redopt |= spot::ltl::Reduce_Containment_Checks;
391
392
393
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
394
	  redopt |= spot::ltl::Reduce_Containment_Checks_Stronger;
395
396
397
398
399
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
400
401
402
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
403
	}
martinez's avatar
martinez committed
404
405
406
407
408
409
410
411
412
      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"))
413
	{
martinez's avatar
martinez committed
414
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
415
	}
martinez's avatar
martinez committed
416
      else if (!strcmp(argv[formula_index], "-R2t"))
417
	{
martinez's avatar
martinez committed
418
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
	}
      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;
	}
436
437
438
439
440
441
442
443
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
444
445
446
447
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
448
449
450
451
452
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
	  fm_opt = true;
	  // Parse -U's argument.
453
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
454
455
456
457
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
458
	      tok = strtok(0, ", \t;");
459
460
	    }
	}
461
462
463
464
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
465
466
467
468
469
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
470
471
472
473
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
474
475
476
477
478
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
479
480
481
482
      else
	{
	  break;
	}
483
484
    }

485
  if ((graph_run_opt || graph_run_tgba_opt)
486
      && (!echeck_inst || !expect_counter_example))
487
    {
488
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
489
490
491
      exit(1);
    }

492
493
494
495
  std::string input;

  if (file_opt)
    {
496
      if (strcmp(argv[formula_index], "-"))
497
	{
498
	  std::ifstream fin(argv[formula_index]);
499
	  if (!fin)
500
501
502
503
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
504

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

521
522
523
524
525
526
527
528
  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)
529
    {
530
531
532
533
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

559
	  if (fm_opt)
560
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
561
					       fm_symb_merge_opt,
562
					       post_branching,
563
					       fair_loop_approx, unobservables,
564
					       fm_red, containment);
565
566
567
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
568

569
      spot::tgba_tba_proxy* degeneralized = 0;
570

571
572
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
573
	  && degeneralize_opt == NoDegen
574
575
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
576
577
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
578
	a = degeneralized = new spot::tgba_tba_proxy(a);
579
580
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
581

582
583
584
585
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
586
587
588
589

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

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

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

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

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

654
655
      spot::tgba* product_degeneralized = 0;

656
      if (system)
657
658
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
659
660
661
662
663
664

	  unsigned int n_acc = a->number_of_acceptance_conditions();
	  if (echeck_inst
	      && degeneralize_opt == NoDegen
	      && n_acc > 1
	      && echeck_inst->max_acceptance_conditions() < n_acc)
665
666
667
668
669
670
671
672
            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);
        }
673

674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
      if (echeck_inst
	  && (a->number_of_acceptance_conditions()
	      < echeck_inst->min_acceptance_conditions()))
	{
	  if (!paper_opt)
	    {
	      std::cerr << echeck_algo << " requires at least "
			<< echeck_inst->min_acceptance_conditions()
			<< " acceptance conditions." << std::endl;
	      exit(1);
	    }
	  else
	    {
	      std::cout << std::endl;
	      exit(0);
	    }
	}

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

750
      if (echeck_inst)
751
	{
752
753
754
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
755
756
757
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
758
759
760
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
761
                  std::cout << std::left << std::setw(25)
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
                            << 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
782
                    std::cout << "no stats, , ";
783
784
785
786
787
788
789
790
791
792
793
794
                  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 &&
795
		      (!expect_counter_example || ec->safe()))
796
797
798
                    exit_code = 1;

                  if (!res)
799
                    {
800
                      std::cout << "no accepting run found";
801
                      if (!ec->safe() && expect_counter_example)
802
803
                        {
                          std::cout << " even if expected" << std::endl;
804
805
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
806
807
808
809
810
811
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
812
                    }
813
814
                  else
                    {
815

816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
                      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;
                        }
                    }
                }
852
853
	      delete res;
	    }
854
	  while (search_many);
855
	  delete ec;
martinez's avatar
martinez committed
856
857
	}

858
859
      if (f)
        spot::ltl::destroy(f);
860
861
      delete product_degeneralized;
      delete product_to_free;
862
      delete system;
863
864
      delete expl;
      delete aut_red;
865
      delete degeneralized;
866
      delete to_free;
867
      delete echeck_inst;
868
869
870
871
872
873
    }
  else
    {
      exit_code = 1;
    }

874
875
876
877
878
879
880
881
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
	spot::ltl::destroy(*i);
      delete unobservables;
    }

882
883
884
885
  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);
886
  delete dict;
887
888
  return exit_code;
}