ltl2tgba.cc 27.3 KB
Newer Older
1
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
2
3
// 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 "ltlast/allnodes.hh"
33
#include "ltlparse/public.hh"
34
#include "tgbaalgos/ltl2tgba_lacim.hh"
35
#include "tgbaalgos/ltl2tgba_fm.hh"
36
#include "tgba/bddprint.hh"
37
#include "tgbaalgos/save.hh"
38
#include "tgbaalgos/dotty.hh"
39
#include "tgbaalgos/lbtt.hh"
40
#include "tgba/tgbatba.hh"
41
#include "tgba/tgbasgba.hh"
42
#include "tgba/tgbaproduct.hh"
43
#include "tgba/futurecondcol.hh"
44
#include "tgbaalgos/reducerun.hh"
45
#include "tgbaparse/public.hh"
46
#include "tgbaalgos/dupexp.hh"
47
#include "tgbaalgos/neverclaim.hh"
48
#include "tgbaalgos/reductgba_sim.hh"
49
#include "tgbaalgos/replayrun.hh"
50
#include "tgbaalgos/rundotdec.hh"
51

52
#include "tgbaalgos/stats.hh"
53
#include "tgbaalgos/scc.hh"
54
55
#include "tgbaalgos/emptiness_stats.hh"

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

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

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

206
  for (;;)
207
    {
208
      if (argc < formula_index + 2)
209
	syntax(argv[0]);
210
211
212

      ++formula_index;

213
214
215
216
217
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
218
219
220
	{
	  output = 2;
	}
221
      else if (!strcmp(argv[formula_index], "-A"))
222
	{
223
	  output = 4;
224
	}
225
      else if (!strcmp(argv[formula_index], "-b"))
226
	{
227
	  output = 7;
228
	}
229
230
231
232
233
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
	  fm_opt = true;
	}
234
      else if (!strcmp(argv[formula_index], "-d"))
235
236
237
	{
	  debug_opt = true;
	}
238
239
      else if (!strcmp(argv[formula_index], "-D"))
	{
240
241
242
243
244
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
245
	}
246
      else if (!strncmp(argv[formula_index], "-e", 2))
247
        {
248
249
250
251
252
253
254
255
256
257
258
259
260
	  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);
	    }
261
262
263
          expect_counter_example = true;
          output = -1;
        }
264
      else if (!strncmp(argv[formula_index], "-E", 2))
265
        {
266
267
268
269
270
271
272
273
274
275
276
277
278
	  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);
	    }
279
280
281
          expect_counter_example = false;
          output = -1;
        }
282
283
284
285
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
      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"))
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
	{
	  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"))
319
320
321
322
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_All;
	}
323
324
325
326
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
327
328
329
330
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
331
332
333
334
      else if (!strcmp(argv[formula_index], "-g"))
	{
	  graph_run_opt = true;
	}
335
336
337
338
      else if (!strcmp(argv[formula_index], "-G"))
	{
	  graph_run_tgba_opt = true;
	}
339
340
341
342
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
343
344
345
346
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
347
348
349
350
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
351
352
353
354
355
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
356
357
358
359
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
360
361
      else if (!strcmp(argv[formula_index], "-m"))
	{
362
	  opt_reduce = true;
363
	}
martinez's avatar
martinez committed
364
365
      else if (!strcmp(argv[formula_index], "-N"))
	{
366
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
367
368
	  output = 8;
	}
369
370
371
372
373
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
374
375
376
377
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
378
				    pel, dict, env, env, debug_opt);
379
380
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
381
382
	    return 2;
	  system->merge_transitions();
383
384
385

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

506
  if ((graph_run_opt || graph_run_tgba_opt)
507
      && (!echeck_inst || !expect_counter_example))
508
    {
509
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
510
511
512
      exit(1);
    }

513
514
515
516
  std::string input;

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

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

542
543
544
545
546
547
548
549
  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)
550
    {
551
552
553
554
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

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

590
      spot::tgba_tba_proxy* degeneralized = 0;
591
      spot::tgba_sgba_proxy* state_labeled = 0;
592

593
594
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
595
	  && degeneralize_opt == NoDegen
596
597
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
598
599
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
600
	a = degeneralized = new spot::tgba_tba_proxy(a);
601
602
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
603
604
605
606
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
607

608
609
610
611
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
612
613
614
615

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

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

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

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

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

680
681
      spot::tgba* product_degeneralized = 0;

682
      if (system)
683
684
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
685
686
687
688
689
690

	  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)
691
692
693
694
695
696
697
698
            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);
        }
699

700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
      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);
	    }
	}

718
719
720
721
722
      if (show_fc)
	{
	  a = new spot::future_conditions_collector(a, true);
	}

723
724
      switch (output)
	{
725
726
727
	case -1:
	  /* No output.  */
	  break;
728
729
730
731
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
732
733
734
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
735
736
	  break;
	case 2:
737
738
739
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
740
				get_core_data().acceptance_conditions);
741
742
	  break;
	case 3:
743
744
745
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
746
747
	  break;
	case 4:
748
749
750
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
751
				get_core_data().acceptance_conditions);
752
	  break;
753
	case 5:
754
	  a->get_dict()->dump(std::cout);
755
	  break;
756
757
758
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
759
760
761
	case 7:
	  spot::tgba_save_reachable(std::cout, a);
	  break;
762
	case 8:
763
764
765
766
767
768
769
	  {
	    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;
	  }
770
771
	case 9:
	  stats_reachable(a).dump(std::cout);
772
773
774
	  build_scc_stats(a).dump(std::cout);
	  break;
	case 10:
775
776
777
778
	  dump_scc_dot(a, std::cout, false);
	  break;
	case 11:
	  dump_scc_dot(a, std::cout, true);
779
	  break;
780
781
782
	default:
	  assert(!"unknown output option");
	}
783

784
      if (echeck_inst)
785
	{
786
787
788
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
789
790
791
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
792
793
794
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
795
                  std::cout << std::left << std::setw(25)
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
                            << 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
816
                    std::cout << "no stats, , ";
817
818
819
820
821
822
823
824
825
826
827
828
                  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 &&
829
		      (!expect_counter_example || ec->safe()))
830
831
832
                    exit_code = 1;

                  if (!res)
833
                    {
834
                      std::cout << "no accepting run found";
835
                      if (!ec->safe() && expect_counter_example)
836
837
                        {
                          std::cout << " even if expected" << std::endl;
838
839
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
840
841
842
843
844
845
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
846
                    }
847
848
                  else
                    {
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
874
875
876
877
878
879
880
881
882
883
884
885
                      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;
                        }
                    }
                }
886
887
	      delete res;
	    }
888
	  while (search_many);
889
	  delete ec;
martinez's avatar
martinez committed
890
891
	}

892
893
      if (show_fc)
	delete a;
894
895
      if (f)
        spot::ltl::destroy(f);
896
897
      delete product_degeneralized;
      delete product_to_free;
898
      delete system;
899
900
      delete expl;
      delete aut_red;
901
      delete degeneralized;
902
      delete state_labeled;
903
      delete to_free;
904
      delete echeck_inst;
905
906
907
908
909
910
    }
  else
    {
      exit_code = 1;
    }

911
912
913
914
915
916
917
918
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
	spot::ltl::destroy(*i);
      delete unobservables;
    }

919
920
921
922
  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);
923
  delete dict;
924
925
  return exit_code;
}