ltl2tgba.cc 27.7 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 "tgbaalgos/ltl2taa.hh"
37
#include "tgba/bddprint.hh"
38
#include "tgbaalgos/save.hh"
39
#include "tgbaalgos/dotty.hh"
40
#include "tgbaalgos/lbtt.hh"
41
#include "tgba/tgbatba.hh"
42
#include "tgba/tgbasgba.hh"
43
#include "tgba/tgbaproduct.hh"
44
#include "tgba/futurecondcol.hh"
45
#include "tgbaalgos/reducerun.hh"
46
#include "tgbaparse/public.hh"
47
#include "tgbaalgos/dupexp.hh"
48
#include "tgbaalgos/neverclaim.hh"
49
#include "tgbaalgos/reductgba_sim.hh"
50
#include "tgbaalgos/replayrun.hh"
51
#include "tgbaalgos/rundotdec.hh"
52

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

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

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

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

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

      ++formula_index;

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

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

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

521
522
523
524
  std::string input;

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

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

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

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

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

601
      spot::tgba_tba_proxy* degeneralized = 0;
602
      spot::tgba_sgba_proxy* state_labeled = 0;
603

604
605
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
606
	  && degeneralize_opt == NoDegen
607
608
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
609
610
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
611
	a = degeneralized = new spot::tgba_tba_proxy(a);
612
613
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
614
615
616
617
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
618

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

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

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

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

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

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

691
692
      spot::tgba* product_degeneralized = 0;

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

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

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

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

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

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

                  if (!res)
844
                    {
845
                      std::cout << "no accepting run found";
846
                      if (!ec->safe() && expect_counter_example)
847
848
                        {
                          std::cout << " even if expected" << std::endl;
849
850
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
851
852
853
854
855
856
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
857
                    }
858
859
                  else
                    {
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
895
896
                      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;
                        }
                    }
                }
897
898
	      delete res;
	    }
899
	  while (search_many);
900
	  delete ec;
martinez's avatar
martinez committed
901
902
	}

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

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

930
931
932
933
  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);
934
  delete dict;
935
936
  return exit_code;
}