ltl2tgba.cc 23.9 KB
Newer Older
1
2
3
// Copyright (C) 2003, 2004, 2005, 2006 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 "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
            << "  -f    use Couvreur's FM algorithm for translation"
	    << std::endl
77
78
79
80
	    << "  -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
martinez's avatar
martinez committed
81
            << "  -F    read the formula from the file" << std::endl
82
	    << "  -g    graph the accepting run on the automaton (requires -e)"
83
	    << std::endl
84
85
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
martinez's avatar
martinez committed
86
            << "  -L    fair-loop approximation (implies -f)" << std::endl
87
	    << "  -m    try to reduce accepting runs, in a second pass"
88
	    << std::endl
martinez's avatar
martinez committed
89
90
	    << "  -N    display the never clain for Spin "
	    << "(implies -D)" << std::endl
martinez's avatar
martinez committed
91
            << "  -p    branching postponement (implies -f)" << std::endl
92
93
	    << "  -Pfile  multiply the formula with the automaton from `file'."
	    << std::endl
martinez's avatar
martinez committed
94
	    << "  -r    display the relation BDD, not the reachability graph"
95
	    << std::endl
martinez's avatar
martinez committed
96
97
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
98
	    << "and universality" << std::endl
martinez's avatar
martinez committed
99
	    << "  -r3   reduce formula using implication between "
100
	    << "sub-formulae" << std::endl
martinez's avatar
martinez committed
101
102
103
	    << "  -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
104
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
105
	    << "(use -L for more reduction)"
106
	    << std::endl
107
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
108
	    << "(use -L for more reduction)"
109
	    << std::endl
110
111
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
112
	    << std::endl
113
114
115
	    << "  -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
116
	    << "  -s    convert to explicit automata, and number states "
117
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
118
	    << "  -S    convert to explicit automata, and number states "
119
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
120
	    << "  -t    display reachable states in LBTT's format" << std::endl
121
122
            << "  -U[PROPS]  consider atomic properties PROPS as exclusive "
	    << "events (implies -f)" << std::endl
martinez's avatar
martinez committed
123
124
125
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
126
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
127
	    << "  -X    do not compute an automaton, read it from a file"
128
	    << std::endl
martinez's avatar
martinez committed
129
	    << "  -y    do not merge states with same symbolic representation "
130
131
132
	    << "(implies -f)" << std::endl
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
133
134
135
136
137
138
	    << "  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;
139
140
141
142
143
144
145
146
  exit(2);
}

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

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

179
  for (;;)
180
    {
181
      if (argc < formula_index + 2)
182
	syntax(argv[0]);
183
184
185

      ++formula_index;

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

	  if (!paper_opt)
	    std::clog << argv[formula_index] + 2 << " read" << std::endl;
317
	}
318
319
      else if (!strcmp(argv[formula_index], "-r"))
	{
320
321
	  output = 1;
	}
322
323
324
325
326
327
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
328
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
329
330
331
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
332
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
333
334
335
336
337
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
338
339
340
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
341
	}
martinez's avatar
martinez committed
342
343
344
345
346
347
348
349
350
      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"))
351
	{
martinez's avatar
martinez committed
352
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
353
	}
martinez's avatar
martinez committed
354
      else if (!strcmp(argv[formula_index], "-R2t"))
355
	{
martinez's avatar
martinez committed
356
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
	}
      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;
	}
374
375
376
377
378
379
380
381
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
382
383
384
385
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
386
387
388
389
390
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
	  fm_opt = true;
	  // Parse -U's argument.
391
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
392
393
394
395
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
396
	      tok = strtok(0, ", \t;");
397
398
	    }
	}
399
400
401
402
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
403
404
405
406
407
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
408
409
410
411
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
412
413
414
415
416
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
417
418
419
420
      else
	{
	  break;
	}
421
422
    }

423
  if ((graph_run_opt || graph_run_tgba_opt)
424
      && (!echeck_inst || !expect_counter_example))
425
    {
426
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
427
428
429
      exit(1);
    }

430
431
432
433
  std::string input;

  if (file_opt)
    {
434
      if (strcmp(argv[formula_index], "-"))
435
	{
436
	  std::ifstream fin(argv[formula_index]);
437
	  if (!fin)
438
439
440
441
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
442

443
	  if (!std::getline(fin, input, '\0'))
444
445
446
447
448
449
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
450
	{
451
	  std::getline(std::cin, input, '\0');
452
453
454
455
456
457
458
	}
    }
  else
    {
      input = argv[formula_index];
    }

459
460
461
462
463
464
465
466
  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)
467
    {
468
469
470
471
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

472
473
474
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
475
	  spot::tgba_explicit* e;
476
477
	  to_free = a = e = spot::tgba_parse(input, pel, dict,
					     env, env, debug_opt);
478
	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
479
480
481
482
483
	    {
	      delete to_free;
	      delete dict;
	      return 2;
	    }
484
	  e->merge_transitions();
485
	}
486
      else
487
	{
488
	  if (redopt != spot::ltl::Reduce_None)
489
	    {
490
491
492
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
493
494
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
495
	    }
496

497
	  if (fm_opt)
498
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
499
					       fm_symb_merge_opt,
500
					       post_branching,
501
502
					       fair_loop_approx, unobservables,
					       fm_red);
503
504
505
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
506

507
      spot::tgba_tba_proxy* degeneralized = 0;
508

509
510
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
511
	  && degeneralize_opt == NoDegen
512
513
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
514
515
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
516
	a = degeneralized = new spot::tgba_tba_proxy(a);
517
518
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
519

520
521
522
523
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
524
525
526
527

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

martinez's avatar
martinez committed
528
529
530
531
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
532
	    {
martinez's avatar
martinez committed
533
534
535
536
537
	      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))
538
539
540
541
		rel_dir =
		  spot::get_direct_relation_simulation(a,
						       std::cout,
						       display_parity_game);
martinez's avatar
martinez committed
542
543
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
544
545
546
547
		rel_del =
		  spot::get_delayed_relation_simulation(a,
							std::cout,
							display_parity_game);
548
549

	      if (display_rel_sim)
martinez's avatar
martinez committed
550
551
552
553
554
555
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
556

martinez's avatar
martinez committed
557
558
559
560
561
562
563
564
565
566
567
568
569
	      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);
570
571
572
	    }
	}

573
574
575
576
577
578
579
580
581
582
583
584
585
      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;
	}

586
587
      spot::tgba* product_degeneralized = 0;

588
      if (system)
589
590
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
591
592
593
594
595
596

	  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)
597
598
599
600
601
602
603
604
            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);
        }
605

606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
      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);
	    }
	}

624
625
      switch (output)
	{
626
627
628
	case -1:
	  /* No output.  */
	  break;
629
630
631
632
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
633
634
635
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
636
637
	  break;
	case 2:
638
639
640
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
641
				get_core_data().acceptance_conditions);
642
643
	  break;
	case 3:
644
645
646
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
647
648
	  break;
	case 4:
649
650
651
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
652
				get_core_data().acceptance_conditions);
653
	  break;
654
	case 5:
655
	  a->get_dict()->dump(std::cout);
656
	  break;
657
658
659
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
660
661
662
	case 7:
	  spot::tgba_save_reachable(std::cout, a);
	  break;
663
	case 8:
664
665
666
667
668
669
670
	  {
	    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;
	  }
671
672
673
	default:
	  assert(!"unknown output option");
	}
674

675
      if (echeck_inst)
676
	{
677
678
679
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
680
681
682
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
683
684
685
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
686
                  std::cout << std::left << std::setw(25)
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
                            << 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
707
                    std::cout << "no stats, , ";
708
709
710
711
712
713
714
715
716
717
718
719
                  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 &&
720
		      (!expect_counter_example || ec->safe()))
721
722
723
                    exit_code = 1;

                  if (!res)
724
                    {
725
                      std::cout << "no accepting run found";
726
                      if (!ec->safe() && expect_counter_example)
727
728
                        {
                          std::cout << " even if expected" << std::endl;
729
730
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
731
732
733
734
735
736
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
737
                    }
738
739
                  else
                    {
740

741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
                      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;
                        }
                    }
                }
777
778
	      delete res;
	    }
779
	  while (search_many);
780
	  delete ec;
martinez's avatar
martinez committed
781
782
	}

783
784
      if (f)
        spot::ltl::destroy(f);
785
786
      delete product_degeneralized;
      delete product_to_free;
787
      delete system;
788
789
      delete expl;
      delete aut_red;
790
      delete degeneralized;
791
      delete to_free;
792
      delete echeck_inst;
793
794
795
796
797
798
799
800
801
802
    }
  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);
803
  delete dict;
804
805
  return exit_code;
}