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

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

506
      spot::tgba_tba_proxy* degeneralized = 0;
507

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

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

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

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

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

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

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

585
586
      spot::tgba* product_degeneralized = 0;

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

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

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

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

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

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

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
                      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;
                        }
                    }
                }
776
777
	      delete res;
	    }
778
	  while (search_many);
779
	  delete ec;
martinez's avatar
martinez committed
780
781
	}

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