ltl2tgba.cc 26.3 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 "ltlast/allnodes.hh"
33
#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
#include "tgbaalgos/stats.hh"
51
#include "tgbaalgos/scc.hh"
52
53
#include "tgbaalgos/emptiness_stats.hh"

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

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

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

198
  for (;;)
199
    {
200
      if (argc < formula_index + 2)
201
	syntax(argv[0]);
202
203
204

      ++formula_index;

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

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

486
  if ((graph_run_opt || graph_run_tgba_opt)
487
      && (!echeck_inst || !expect_counter_example))
488
    {
489
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
490
491
492
      exit(1);
    }

493
494
495
496
  std::string input;

  if (file_opt)
    {
497
      if (strcmp(argv[formula_index], "-"))
498
	{
499
	  std::ifstream fin(argv[formula_index]);
500
	  if (!fin)
501
502
503
504
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
505

506
	  if (!std::getline(fin, input, '\0'))
507
508
509
510
511
512
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
513
	{
514
	  std::getline(std::cin, input, '\0');
515
516
517
518
519
520
521
	}
    }
  else
    {
      input = argv[formula_index];
    }

522
523
524
525
526
527
528
529
  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)
530
    {
531
532
533
534
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

560
	  if (fm_opt)
561
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
562
					       fm_symb_merge_opt,
563
					       post_branching,
564
					       fair_loop_approx, unobservables,
565
					       fm_red, containment);
566
567
568
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
569

570
      spot::tgba_tba_proxy* degeneralized = 0;
571

572
573
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
574
	  && degeneralize_opt == NoDegen
575
576
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
577
578
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
579
	a = degeneralized = new spot::tgba_tba_proxy(a);
580
581
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
582

583
584
585
586
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
587
588
589
590

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

martinez's avatar
martinez committed
591
592
593
594
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
595
	    {
martinez's avatar
martinez committed
596
597
598
599
600
	      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))
601
602
603
604
605
606
607
608
		{
		  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
609
				    spot::Reduce_transition_Del_Sim))
610
611
612
613
614
615
616
		{
		  rel_del =
		    spot::get_delayed_relation_simulation(a,
							  std::cout,
							  display_parity_game);
		  assert(rel_del);
		}
617
618

	      if (display_rel_sim)
martinez's avatar
martinez committed
619
620
621
622
623
624
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
625

martinez's avatar
martinez committed
626
627
628
629
630
631
632
633
634
635
636
637
638
	      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);
639
640
641
	    }
	}

642
643
644
645
646
647
648
649
650
651
652
653
654
      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;
	}

655
656
      spot::tgba* product_degeneralized = 0;

657
      if (system)
658
659
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
660
661
662
663
664
665

	  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)
666
667
668
669
670
671
672
673
            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);
        }
674

675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
      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);
	    }
	}

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

751
      if (echeck_inst)
752
	{
753
754
755
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
756
757
758
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
759
760
761
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
762
                  std::cout << std::left << std::setw(25)
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
                            << 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
783
                    std::cout << "no stats, , ";
784
785
786
787
788
789
790
791
792
793
794
795
                  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 &&
796
		      (!expect_counter_example || ec->safe()))
797
798
799
                    exit_code = 1;

                  if (!res)
800
                    {
801
                      std::cout << "no accepting run found";
802
                      if (!ec->safe() && expect_counter_example)
803
804
                        {
                          std::cout << " even if expected" << std::endl;
805
806
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
807
808
809
810
811
812
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
813
                    }
814
815
                  else
                    {
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
841
842
843
844
845
846
847
848
849
850
851
852
                      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;
                        }
                    }
                }
853
854
	      delete res;
	    }
855
	  while (search_many);
856
	  delete ec;
martinez's avatar
martinez committed
857
858
	}

859
860
      if (f)
        spot::ltl::destroy(f);
861
862
      delete product_degeneralized;
      delete product_to_free;
863
      delete system;
864
865
      delete expl;
      delete aut_red;
866
      delete degeneralized;
867
      delete to_free;
868
      delete echeck_inst;
869
870
871
872
873
874
    }
  else
    {
      exit_code = 1;
    }

875
876
877
878
879
880
881
882
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
	spot::ltl::destroy(*i);
      delete unobservables;
    }

883
884
885
886
  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);
887
  delete dict;
888
889
  return exit_code;
}