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

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

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

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

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

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

      ++formula_index;

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

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

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

480
481
482
483
  std::string input;

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

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

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

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

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

557
      spot::tgba_tba_proxy* degeneralized = 0;
558

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

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

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

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

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

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

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

642
643
      spot::tgba* product_degeneralized = 0;

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

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

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

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

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

                  if (!res)
780
                    {
781
                      std::cout << "no accepting run found";
782
                      if (!ec->safe() && expect_counter_example)
783
784
                        {
                          std::cout << " even if expected" << std::endl;
785
786
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
787
788
789
790
791
792
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
793
                    }
794
795
                  else
                    {
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
832
                      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;
                        }
                    }
                }
833
834
	      delete res;
	    }
835
	  while (search_many);
836
	  delete ec;
martinez's avatar
martinez committed
837
838
	}

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

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

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