ltl2tgba.cc 25.8 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
martinez's avatar
martinez committed
92
            << "  -L    fair-loop approximation (implies -f)" << std::endl
93
	    << "  -m    try to reduce accepting runs, in a second pass"
94
	    << std::endl
martinez's avatar
martinez committed
95
96
	    << "  -N    display the never clain for Spin "
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
97
            << "  -p    branching postponement (implies -f)" << std::endl
98
99
	    << "  -Pfile  multiply the formula with the automaton from `file'."
	    << std::endl
martinez's avatar
martinez committed
100
	    << "  -r    display the relation BDD, not the reachability graph"
101
	    << std::endl
martinez's avatar
martinez committed
102
103
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
104
	    << "and universality" << std::endl
martinez's avatar
martinez committed
105
	    << "  -r3   reduce formula using implication between "
106
	    << "sub-formulae" << std::endl
107
108
109
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
110
111
	    << "  -r7   reduce formula using tau03+ and -r1" << std::endl
	    << "  -r8   reduce formula using tau03+ and -r4" << std::endl
martinez's avatar
martinez committed
112
113
	    << "  -rd   display the reduce formula" << std::endl
	    << "  -R    same as -r, but as a set" << std::endl
114
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
115
	    << "(use -L for more reduction)"
116
	    << std::endl
117
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
118
	    << "(use -L for more reduction)"
119
	    << std::endl
120
121
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
122
	    << std::endl
123
124
125
	    << "  -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
126
	    << "  -s    convert to explicit automata, and number states "
127
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
128
	    << "  -S    convert to explicit automata, and number states "
129
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
130
	    << "  -t    display reachable states in LBTT's format" << std::endl
131
132
133
134
            << "  -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
135
136
137
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
138
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
139
	    << "  -X    do not compute an automaton, read it from a file"
140
	    << std::endl
martinez's avatar
martinez committed
141
	    << "  -y    do not merge states with same symbolic representation "
142
143
144
	    << "(implies -f)" << std::endl
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
145
146
147
148
149
150
	    << "  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;
151
152
153
154
155
156
157
158
  exit(2);
}

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

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

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

      ++formula_index;

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

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

472
  if ((graph_run_opt || graph_run_tgba_opt)
473
      && (!echeck_inst || !expect_counter_example))
474
    {
475
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
476
477
478
      exit(1);
    }

479
480
481
482
  std::string input;

  if (file_opt)
    {
483
      if (strcmp(argv[formula_index], "-"))
484
	{
485
	  std::ifstream fin(argv[formula_index]);
486
	  if (!fin)
487
488
489
490
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
491

492
	  if (!std::getline(fin, input, '\0'))
493
494
495
496
497
498
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
499
	{
500
	  std::getline(std::cin, input, '\0');
501
502
503
504
505
506
507
	}
    }
  else
    {
      input = argv[formula_index];
    }

508
509
510
511
512
513
514
515
  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)
516
    {
517
518
519
520
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

546
	  if (fm_opt)
547
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
548
					       fm_symb_merge_opt,
549
					       post_branching,
550
					       fair_loop_approx, unobservables,
551
					       fm_red, containment);
552
553
554
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
555

556
      spot::tgba_tba_proxy* degeneralized = 0;
557

558
559
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
560
	  && degeneralize_opt == NoDegen
561
562
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
563
564
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
565
	a = degeneralized = new spot::tgba_tba_proxy(a);
566
567
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
568

569
570
571
572
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
573
574
575
576

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

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

	      if (display_rel_sim)
martinez's avatar
martinez committed
605
606
607
608
609
610
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
611

martinez's avatar
martinez committed
612
613
614
615
616
617
618
619
620
621
622
623
624
	      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);
625
626
627
	    }
	}

628
629
630
631
632
633
634
635
636
637
638
639
640
      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;
	}

641
642
      spot::tgba* product_degeneralized = 0;

643
      if (system)
644
645
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
646
647
648
649
650
651

	  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)
652
653
654
655
656
657
658
659
            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);
        }
660

661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
      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);
	    }
	}

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

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

                  if (!res)
779
                    {
780
                      std::cout << "no accepting run found";
781
                      if (!ec->safe() && expect_counter_example)
782
783
                        {
                          std::cout << " even if expected" << std::endl;
784
785
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
786
787
788
789
790
791
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
792
                    }
793
794
                  else
                    {
795

796
797
798
799
800
801
802
803
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
                      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;
                        }
                    }
                }
832
833
	      delete res;
	    }
834
	  while (search_many);
835
	  delete ec;
martinez's avatar
martinez committed
836
837
	}

838
839
      if (f)
        spot::ltl::destroy(f);
840
841
      delete product_degeneralized;
      delete product_to_free;
842
      delete system;
843
844
      delete expl;
      delete aut_red;
845
      delete degeneralized;
846
      delete to_free;
847
      delete echeck_inst;
848
849
850
851
852
853
    }
  else
    {
      exit_code = 1;
    }

854
855
856
857
858
859
860
861
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
	spot::ltl::destroy(*i);
      delete unobservables;
    }

862
863
864
865
  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);
866
  delete dict;
867
868
  return exit_code;
}