ltl2tgba.cc 26 KB
Newer Older
1
2
3
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008 Laboratoire
// d'Informatique de Paris 6 (LIP6), dpartement Systmes Rpartis
// Coopratifs (SRC), Universit Pierre et Marie Curie.
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

22
#include <iostream>
23
#include <iomanip>
24
#include <cassert>
25
26
#include <fstream>
#include <string>
27
#include <cstdlib>
28
#include "ltlvisit/destroy.hh"
29
#include "ltlvisit/contain.hh"
30
#include "ltlvisit/tostring.hh"
31
#include "ltlvisit/apcollect.hh"
32
#include "ltlparse/public.hh"
33
#include "tgbaalgos/ltl2tgba_lacim.hh"
34
#include "tgbaalgos/ltl2tgba_fm.hh"
35
#include "tgba/bddprint.hh"
36
#include "tgbaalgos/save.hh"
37
#include "tgbaalgos/dotty.hh"
38
#include "tgbaalgos/lbtt.hh"
39
#include "tgba/tgbatba.hh"
40
#include "tgba/tgbaproduct.hh"
41
#include "tgbaalgos/reducerun.hh"
42
#include "tgbaparse/public.hh"
43
#include "tgbaalgos/dupexp.hh"
44
#include "tgbaalgos/neverclaim.hh"
45
#include "tgbaalgos/reductgba_sim.hh"
46
#include "tgbaalgos/replayrun.hh"
47
#include "tgbaalgos/rundotdec.hh"
48

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

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

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

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

194
  for (;;)
195
    {
196
      if (argc < formula_index + 2)
197
	syntax(argv[0]);
198
199
200

      ++formula_index;

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

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

478
  if ((graph_run_opt || graph_run_tgba_opt)
479
      && (!echeck_inst || !expect_counter_example))
480
    {
481
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
482
483
484
      exit(1);
    }

485
486
487
488
  std::string input;

  if (file_opt)
    {
489
      if (strcmp(argv[formula_index], "-"))
490
	{
491
	  std::ifstream fin(argv[formula_index]);
492
	  if (!fin)
493
494
495
496
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
497

498
	  if (!std::getline(fin, input, '\0'))
499
500
501
502
503
504
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
505
	{
506
	  std::getline(std::cin, input, '\0');
507
508
509
510
511
512
513
	}
    }
  else
    {
      input = argv[formula_index];
    }

514
515
516
517
518
519
520
521
  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)
522
    {
523
524
525
526
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

552
	  if (fm_opt)
553
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
554
					       fm_symb_merge_opt,
555
					       post_branching,
556
					       fair_loop_approx, unobservables,
557
					       fm_red, containment);
558
559
560
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
561

562
      spot::tgba_tba_proxy* degeneralized = 0;
563

564
565
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
566
	  && degeneralize_opt == NoDegen
567
568
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
569
570
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
571
	a = degeneralized = new spot::tgba_tba_proxy(a);
572
573
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
574

575
576
577
578
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
579
580
581
582

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

martinez's avatar
martinez committed
583
584
585
586
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
587
	    {
martinez's avatar
martinez committed
588
589
590
591
592
	      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))
593
594
595
596
597
598
599
600
		{
		  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
601
				    spot::Reduce_transition_Del_Sim))
602
603
604
605
606
607
608
		{
		  rel_del =
		    spot::get_delayed_relation_simulation(a,
							  std::cout,
							  display_parity_game);
		  assert(rel_del);
		}
609
610

	      if (display_rel_sim)
martinez's avatar
martinez committed
611
612
613
614
615
616
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
617

martinez's avatar
martinez committed
618
619
620
621
622
623
624
625
626
627
628
629
630
	      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);
631
632
633
	    }
	}

634
635
636
637
638
639
640
641
642
643
644
645
646
      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;
	}

647
648
      spot::tgba* product_degeneralized = 0;

649
      if (system)
650
651
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
652
653
654
655
656
657

	  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)
658
659
660
661
662
663
664
665
            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);
        }
666

667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
      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);
	    }
	}

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

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

                  if (!res)
788
                    {
789
                      std::cout << "no accepting run found";
790
                      if (!ec->safe() && expect_counter_example)
791
792
                        {
                          std::cout << " even if expected" << std::endl;
793
794
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
795
796
797
798
799
800
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
801
                    }
802
803
                  else
                    {
804

805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
                      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;
                        }
                    }
                }
841
842
	      delete res;
	    }
843
	  while (search_many);
844
	  delete ec;
martinez's avatar
martinez committed
845
846
	}

847
848
      if (f)
        spot::ltl::destroy(f);
849
850
      delete product_degeneralized;
      delete product_to_free;
851
      delete system;
852
853
      delete expl;
      delete aut_red;
854
      delete degeneralized;
855
      delete to_free;
856
      delete echeck_inst;
857
858
859
860
861
862
    }
  else
    {
      exit_code = 1;
    }

863
864
865
866
867
868
869
870
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
	spot::ltl::destroy(*i);
      delete unobservables;
    }

871
872
873
874
  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);
875
  delete dict;
876
877
  return exit_code;
}