ltl2tgba.cc 27.5 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/contain.hh"
29
#include "ltlvisit/tostring.hh"
30
#include "ltlvisit/apcollect.hh"
31
#include "ltlast/allnodes.hh"
32
#include "ltlparse/public.hh"
33
#include "tgbaalgos/ltl2tgba_lacim.hh"
34
#include "tgbaalgos/ltl2tgba_fm.hh"
35
#include "tgbaalgos/ltl2taa.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
            << "  -f    use Couvreur's FM algorithm for translation"
82
	    << std::endl
83
            << "  -taa  use Tauriainen's TAA-based algorithm for translation"
martinez's avatar
martinez committed
84
	    << std::endl
85
86
87
88
	    << "  -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
89
90
91
	    << "  -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
martinez's avatar
martinez committed
92
            << "  -F    read the formula from the file" << std::endl
93
94
            << "  -FC   dump the automaton showing future conditions on states"
	    << std::endl
95
	    << "  -g    graph the accepting run on the automaton (requires -e)"
96
	    << std::endl
97
98
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
99
100
	    << "  -k    display statistics on the TGBA instead of dumping it"
	    << std::endl
101
102
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
103
	    << std::endl
martinez's avatar
martinez committed
104
            << "  -L    fair-loop approximation (implies -f)" << std::endl
105
            << "  -lS   label acceptance conditions on states" << std::endl
106
	    << "  -m    try to reduce accepting runs, in a second pass"
107
	    << std::endl
martinez's avatar
martinez committed
108
109
	    << "  -N    display the never clain for Spin "
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
110
            << "  -p    branching postponement (implies -f)" << std::endl
111
112
	    << "  -Pfile  multiply the formula with the automaton from `file'."
	    << std::endl
martinez's avatar
martinez committed
113
	    << "  -r    display the relation BDD, not the reachability graph"
114
	    << std::endl
martinez's avatar
martinez committed
115
116
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
117
	    << "universality" << std::endl
martinez's avatar
martinez committed
118
	    << "  -r3   reduce formula using implication between "
119
	    << "sub-formulae" << std::endl
120
121
122
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
123
	    << "  -r7   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 taa_opt = false;
176
  bool fm_opt = false;
177
  int fm_red = spot::ltl::Reduce_None;
178
  bool fm_exprop_opt = false;
179
  bool fm_symb_merge_opt = true;
180
  bool file_opt = false;
181
  int output = 0;
182
  int formula_index = 0;
183
184
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
185
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
186
  bool expect_counter_example = false;
187
  bool from_file = false;
188
  int reduc_aut = spot::Reduce_None;
189
  int redopt = spot::ltl::Reduce_None;
190
191
  bool display_reduce_form = false;
  bool display_rel_sim = false;
192
  bool display_parity_game = false;
193
  bool post_branching = false;
194
  bool fair_loop_approx = false;
195
  bool graph_run_opt = false;
196
  bool graph_run_tgba_opt = false;
197
  bool opt_reduce = false;
198
  bool containment = false;
199
  bool show_fc = false;
200
201
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
202
203
  spot::tgba_explicit* system = 0;
  spot::tgba* product = 0;
204
  spot::tgba* product_to_free = 0;
205
  spot::bdd_dict* dict = new spot::bdd_dict();
206

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

      ++formula_index;

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

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

512
  if ((graph_run_opt || graph_run_tgba_opt)
513
      && (!echeck_inst || !expect_counter_example))
514
    {
515
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
516
517
518
      exit(1);
    }

519
520
521
522
  std::string input;

  if (file_opt)
    {
523
      if (strcmp(argv[formula_index], "-"))
524
	{
525
	  std::ifstream fin(argv[formula_index]);
526
	  if (!fin)
527
528
529
530
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
531

532
	  if (!std::getline(fin, input, '\0'))
533
534
535
536
537
538
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
539
	{
540
	  std::getline(std::cin, input, '\0');
541
542
543
544
545
546
547
	}
    }
  else
    {
      input = argv[formula_index];
    }

548
549
550
551
552
553
554
555
  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)
556
    {
557
558
559
560
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

586
	  if (fm_opt)
587
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
588
					       fm_symb_merge_opt,
589
					       post_branching,
590
					       fair_loop_approx, unobservables,
591
					       fm_red, containment);
592
	  else
593
	    if (taa_opt)
Damien Lefortier's avatar
Damien Lefortier committed
594
	      to_free = a = spot::ltl_to_taa(f, dict, containment);
595
596
	    else
	      to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
597
	}
598

599
      spot::tgba_tba_proxy* degeneralized = 0;
600
      spot::tgba_sgba_proxy* state_labeled = 0;
601

602
603
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
604
	  && degeneralize_opt == NoDegen
605
606
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
607
608
	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
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
616

617
618
619
620
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
621
622
623
624

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

martinez's avatar
martinez committed
625
626
627
628
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
629
	    {
martinez's avatar
martinez committed
630
631
632
633
634
	      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))
635
636
637
638
639
640
641
642
		{
		  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
643
				    spot::Reduce_transition_Del_Sim))
644
645
646
647
648
649
650
		{
		  rel_del =
		    spot::get_delayed_relation_simulation(a,
							  std::cout,
							  display_parity_game);
		  assert(rel_del);
		}
651
652

	      if (display_rel_sim)
martinez's avatar
martinez committed
653
654
655
656
657
658
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
659

martinez's avatar
martinez committed
660
661
662
663
664
665
666
667
668
669
670
671
672
	      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);
673
674
675
	    }
	}

676
677
678
679
680
681
682
683
684
685
686
687
688
      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;
	}

689
690
      spot::tgba* product_degeneralized = 0;

691
      if (system)
692
693
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
694
695
696
697
698
699

	  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)
700
701
702
703
704
705
706
707
            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);
        }
708

709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
      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);
	    }
	}

727
728
729
730
731
      if (show_fc)
	{
	  a = new spot::future_conditions_collector(a, true);
	}

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

793
      if (echeck_inst)
794
	{
795
796
797
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
798
799
800
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
801
802
803
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
804
                  std::cout << std::left << std::setw(25)
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
                            << echeck_algo << ", ";
                  spot::tgba_statistics a_size =
                                        spot::stats_reachable(ec->automaton());
                  std::cout << std::right << std::setw(10)
                            << a_size.states << ", "
                            << std::right << std::setw(10)
                            << a_size.transitions << ", ";
                  std::cout <<
                            ec->automaton()->number_of_acceptance_conditions()
                            << ", ";
                  const spot::ec_statistics* ecs =
                        dynamic_cast<const spot::ec_statistics*>(ec);
                  if (ecs)
                    std::cout << std::right << std::setw(10)
                              << ecs->states() << ", "
                              << std::right << std::setw(10)
                              << ecs->transitions() << ", "
                              << std::right << std::setw(10)
                              << ecs->max_depth();
                  else
825
                    std::cout << "no stats, , ";
826
827
828
829
830
831
832
833
834
835
836
837
                  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 &&
838
		      (!expect_counter_example || ec->safe()))
839
840
841
                    exit_code = 1;

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

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

901
902
      if (show_fc)
	delete a;
903
      if (f)
904
        f->destroy();
905
906
      delete product_degeneralized;
      delete product_to_free;
907
      delete system;
908
909
      delete expl;
      delete aut_red;
910
      delete degeneralized;
911
      delete state_labeled;
912
      delete to_free;
913
      delete echeck_inst;
914
915
916
917
918
919
    }
  else
    {
      exit_code = 1;
    }

920
921
922
923
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
924
	(*i)->destroy();
925
926
927
      delete unobservables;
    }

928
929
930
931
  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);
932
  assert(spot::ltl::automatop::instance_count() == 0);
933
  delete dict;
934
935
  return exit_code;
}