ltl2tgba.cc 23 KB
Newer Older
1
// Copyright (C) 2003, 2004, 2005  Laboratoire d'Informatique de Paris 6 (LIP6),
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
// et Marie Curie.
//
// 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 "ltlvisit/destroy.hh"
28
#include "ltlvisit/reduce.hh"
29
#include "ltlvisit/tostring.hh"
30
#include "ltlvisit/apcollect.hh"
31
32
#include "ltlast/allnodes.hh"
#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
martinez's avatar
martinez committed
68
	    << "  -d    turn on traces during parsing" << std::endl
69
70
	    << "  -D    degeneralize the automaton as a TBA" << std::endl
	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
71
72
73
	    << "  -e[ALGO]  emptiness-check, expect and compute an "
	    << "accepting run" << std::endl
	    << "  -E[ALGO]  emptiness-check, expect no accepting run"
74
	    << std::endl
martinez's avatar
martinez committed
75
76
77
            << "  -f    use Couvreur's FM algorithm for translation"
	    << std::endl
            << "  -F    read the formula from the file" << std::endl
78
	    << "  -g    graph the accepting run on the automaton (requires -e)"
79
	    << std::endl
80
81
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
martinez's avatar
martinez committed
82
            << "  -L    fair-loop approximation (implies -f)" << std::endl
83
	    << "  -m    try to reduce accepting runs, in a second pass"
84
	    << std::endl
martinez's avatar
martinez committed
85
86
	    << "  -N    display the never clain for Spin "
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
87
            << "  -p    branching postponement (implies -f)" << std::endl
88
89
	    << "  -Pfile  multiply the formula with the automaton from `file'."
	    << std::endl
martinez's avatar
martinez committed
90
	    << "  -r    display the relation BDD, not the reachability graph"
91
	    << std::endl
martinez's avatar
martinez committed
92
93
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
94
	    << "and universality" << std::endl
martinez's avatar
martinez committed
95
	    << "  -r3   reduce formula using implication between "
96
	    << "sub-formulae" << std::endl
martinez's avatar
martinez committed
97
98
99
	    << "  -r4   reduce formula using all rules" << std::endl
	    << "  -rd   display the reduce formula" << std::endl
	    << "  -R    same as -r, but as a set" << std::endl
100
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
101
	    << "(use -L for more reduction)"
102
	    << std::endl
103
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
104
	    << "(use -L for more reduction)"
105
	    << std::endl
106
107
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
108
	    << std::endl
109
110
111
	    << "  -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
112
	    << "  -s    convert to explicit automata, and number states "
113
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
114
	    << "  -S    convert to explicit automata, and number states "
115
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
116
	    << "  -t    display reachable states in LBTT's format" << std::endl
117
118
            << "  -U[PROPS]  consider atomic properties PROPS as exclusive "
	    << "events (implies -f)" << std::endl
martinez's avatar
martinez committed
119
120
121
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
122
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
123
	    << "  -X    do not compute an automaton, read it from a file"
124
	    << std::endl
martinez's avatar
martinez committed
125
	    << "  -y    do not merge states with same symbolic representation "
126
127
128
	    << "(implies -f)" << std::endl
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
129
130
131
132
133
134
	    << "  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;
135
136
137
138
139
140
141
142
  exit(2);
}

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

143
  bool debug_opt = false;
144
  bool paper_opt = false;
145
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
146
  bool fm_opt = false;
147
  bool fm_exprop_opt = false;
148
  bool fm_symb_merge_opt = true;
149
  bool file_opt = false;
150
  int output = 0;
151
  int formula_index = 0;
152
153
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
154
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
155
  bool expect_counter_example = false;
156
  bool from_file = false;
157
  int reduc_aut = spot::Reduce_None;
158
  int redopt = spot::ltl::Reduce_None;
159
160
  bool display_reduce_form = false;
  bool display_rel_sim = false;
161
  bool display_parity_game = false;
162
  bool post_branching = false;
163
  bool fair_loop_approx = false;
164
  bool graph_run_opt = false;
165
  bool graph_run_tgba_opt = false;
166
  bool opt_reduce = false;
167
168
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
169
170
  spot::tgba_explicit* system = 0;
  spot::tgba* product = 0;
171
  spot::tgba* product_to_free = 0;
172
  spot::bdd_dict* dict = new spot::bdd_dict();
173

174
  for (;;)
175
    {
176
      if (argc < formula_index + 2)
177
	syntax(argv[0]);
178
179
180

      ++formula_index;

181
182
183
184
185
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
186
187
188
	{
	  output = 2;
	}
189
      else if (!strcmp(argv[formula_index], "-A"))
190
	{
191
	  output = 4;
192
	}
193
      else if (!strcmp(argv[formula_index], "-b"))
194
	{
195
	  output = 7;
196
197
	}
      else if (!strcmp(argv[formula_index], "-d"))
198
199
200
	{
	  debug_opt = true;
	}
201
202
      else if (!strcmp(argv[formula_index], "-D"))
	{
203
204
205
206
207
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
208
	}
209
      else if (!strncmp(argv[formula_index], "-e", 2))
210
        {
211
212
213
214
215
216
217
218
219
220
221
222
223
	  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);
	    }
224
225
226
          expect_counter_example = true;
          output = -1;
        }
227
      else if (!strncmp(argv[formula_index], "-E", 2))
228
        {
229
230
231
232
233
234
235
236
237
238
239
240
241
	  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);
	    }
242
243
244
          expect_counter_example = false;
          output = -1;
        }
245
246
247
248
249
250
251
252
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
253
254
255
256
      else if (!strcmp(argv[formula_index], "-g"))
	{
	  graph_run_opt = true;
	}
257
258
259
260
      else if (!strcmp(argv[formula_index], "-G"))
	{
	  graph_run_tgba_opt = true;
	}
261
262
263
264
265
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
266
267
      else if (!strcmp(argv[formula_index], "-m"))
	{
268
	  opt_reduce = true;
269
	}
martinez's avatar
martinez committed
270
271
      else if (!strcmp(argv[formula_index], "-N"))
	{
272
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
273
274
	  output = 8;
	}
275
276
277
278
279
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
280
281
282
283
284
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
				     pel, dict, env, debug_opt);
285
286
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
287
288
	    return 2;
	  system->merge_transitions();
289
290
291

	  if (!paper_opt)
	    std::clog << argv[formula_index] + 2 << " read" << std::endl;
292
	}
293
294
      else if (!strcmp(argv[formula_index], "-r"))
	{
295
296
	  output = 1;
	}
297
298
299
300
301
302
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
303
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
304
305
306
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
307
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
308
309
310
311
312
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
313
314
315
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
316
	}
martinez's avatar
martinez committed
317
318
319
320
321
322
323
324
325
      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"))
326
	{
martinez's avatar
martinez committed
327
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
328
	}
martinez's avatar
martinez committed
329
      else if (!strcmp(argv[formula_index], "-R2t"))
330
	{
martinez's avatar
martinez committed
331
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
	}
      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;
	}
349
350
351
352
353
354
355
356
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
357
358
359
360
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
361
362
363
364
365
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
	  fm_opt = true;
	  // Parse -U's argument.
366
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
367
368
369
370
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
371
	      tok = strtok(0, ", \t;");
372
373
	    }
	}
374
375
376
377
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
378
379
380
381
382
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
383
384
385
386
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
387
388
389
390
391
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
392
393
394
395
      else
	{
	  break;
	}
396
397
    }

398
  if ((graph_run_opt || graph_run_tgba_opt)
399
      && (!echeck_inst || !expect_counter_example))
400
    {
401
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
402
403
404
      exit(1);
    }

405
406
407
408
  std::string input;

  if (file_opt)
    {
409
      if (strcmp(argv[formula_index], "-"))
410
	{
411
	  std::ifstream fin(argv[formula_index]);
412
	  if (!fin)
413
414
415
416
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
417

418
	  if (!std::getline(fin, input, '\0'))
419
420
421
422
423
424
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
425
	{
426
	  std::getline(std::cin, input, '\0');
427
428
429
430
431
432
433
	}
    }
  else
    {
      input = argv[formula_index];
    }

434
435
436
437
438
439
440
441
  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)
442
    {
443
444
445
446
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

447
448
449
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
450
451
	  spot::tgba_explicit* e;
	  to_free = a = e = spot::tgba_parse(input, pel, dict, env, debug_opt);
452
	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
453
454
455
456
457
	    {
	      delete to_free;
	      delete dict;
	      return 2;
	    }
458
	  e->merge_transitions();
459
	}
460
      else
461
	{
462
	  if (redopt != spot::ltl::Reduce_None)
463
	    {
464
465
466
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
467
468
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
469
	    }
470

471
	  if (fm_opt)
472
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
473
					       fm_symb_merge_opt,
474
					       post_branching,
475
					       fair_loop_approx, unobservables);
476
477
478
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
479

480
      spot::tgba_tba_proxy* degeneralized = 0;
481

482
483
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
484
	  && degeneralize_opt == NoDegen
485
486
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
487
488
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
489
	a = degeneralized = new spot::tgba_tba_proxy(a);
490
491
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
492

493
494
495
496
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
497
498
499
500

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

martinez's avatar
martinez committed
501
502
503
504
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
505
	    {
martinez's avatar
martinez committed
506
507
508
509
510
	      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))
511
512
513
514
		rel_dir =
		  spot::get_direct_relation_simulation(a,
						       std::cout,
						       display_parity_game);
martinez's avatar
martinez committed
515
516
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
517
518
519
520
		rel_del =
		  spot::get_delayed_relation_simulation(a,
							std::cout,
							display_parity_game);
521
522

	      if (display_rel_sim)
martinez's avatar
martinez committed
523
524
525
526
527
528
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
529

martinez's avatar
martinez committed
530
531
532
533
534
535
536
537
538
539
540
541
542
	      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);
543
544
545
	    }
	}

546
547
548
549
550
551
552
553
554
555
556
557
558
      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;
	}

559
560
      spot::tgba* product_degeneralized = 0;

561
      if (system)
562
563
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
564
565
566
567
568
569

	  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)
570
571
572
573
574
575
576
577
            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);
        }
578

579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
      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);
	    }
	}

597
598
      switch (output)
	{
599
600
601
	case -1:
	  /* No output.  */
	  break;
602
603
604
605
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
606
607
608
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
609
610
	  break;
	case 2:
611
612
613
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
614
				get_core_data().acceptance_conditions);
615
616
	  break;
	case 3:
617
618
619
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
620
621
	  break;
	case 4:
622
623
624
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
625
				get_core_data().acceptance_conditions);
626
	  break;
627
	case 5:
628
	  a->get_dict()->dump(std::cout);
629
	  break;
630
631
632
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
633
634
635
	case 7:
	  spot::tgba_save_reachable(std::cout, a);
	  break;
636
	case 8:
637
638
639
640
641
642
643
	  {
	    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;
	  }
644
645
646
	default:
	  assert(!"unknown output option");
	}
647

648
      if (echeck_inst)
649
	{
650
651
652
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
653
654
655
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
656
657
658
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
659
                  std::cout << std::left << std::setw(25)
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
                            << 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
680
                    std::cout << "no stats, , ";
681
682
683
684
685
686
687
688
689
690
691
692
                  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 &&
693
		      (!expect_counter_example || ec->safe()))
694
695
696
                    exit_code = 1;

                  if (!res)
697
                    {
698
                      std::cout << "no accepting run found";
699
                      if (!ec->safe() && expect_counter_example)
700
701
                        {
                          std::cout << " even if expected" << std::endl;
702
703
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
704
705
706
707
708
709
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
710
                    }
711
712
                  else
                    {
713

714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
                      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;
                        }
                    }
                }
750
751
	      delete res;
	    }
752
	  while (search_many);
753
	  delete ec;
martinez's avatar
martinez committed
754
755
	}

756
757
      if (f)
        spot::ltl::destroy(f);
758
759
      delete product_degeneralized;
      delete product_to_free;
760
      delete system;
761
762
      delete expl;
      delete aut_red;
763
      delete degeneralized;
764
      delete to_free;
765
      delete echeck_inst;
766
767
768
769
770
771
772
773
774
775
    }
  else
    {
      exit_code = 1;
    }

  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);
776
  delete dict;
777
778
  return exit_code;
}