ltl2tgba.cc 24.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/contain.hh"
30
#include "ltlvisit/tostring.hh"
31
#include "ltlvisit/apcollect.hh"
32
33
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
34
#include "tgbaalgos/ltl2tgba_lacim.hh"
35
#include "tgbaalgos/ltl2tgba_fm.hh"
36
#include "tgba/bddprint.hh"
37
#include "tgbaalgos/save.hh"
38
#include "tgbaalgos/dotty.hh"
39
#include "tgbaalgos/lbtt.hh"
40
#include "tgba/tgbatba.hh"
41
#include "tgba/tgbaproduct.hh"
42
#include "tgbaalgos/reducerun.hh"
43
#include "tgbaparse/public.hh"
44
#include "tgbaalgos/dupexp.hh"
45
#include "tgbaalgos/neverclaim.hh"
46
#include "tgbaalgos/reductgba_sim.hh"
47
#include "tgbaalgos/replayrun.hh"
48
#include "tgbaalgos/rundotdec.hh"
49

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

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

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

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

188
  for (;;)
189
    {
190
      if (argc < formula_index + 2)
191
	syntax(argv[0]);
192
193
194

      ++formula_index;

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

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

450
  if ((graph_run_opt || graph_run_tgba_opt)
451
      && (!echeck_inst || !expect_counter_example))
452
    {
453
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
454
455
456
      exit(1);
    }

457
458
459
460
  std::string input;

  if (file_opt)
    {
461
      if (strcmp(argv[formula_index], "-"))
462
	{
463
	  std::ifstream fin(argv[formula_index]);
464
	  if (!fin)
465
466
467
468
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
469

470
	  if (!std::getline(fin, input, '\0'))
471
472
473
474
475
476
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
477
	{
478
	  std::getline(std::cin, input, '\0');
479
480
481
482
483
484
485
	}
    }
  else
    {
      input = argv[formula_index];
    }

486
487
488
489
490
491
492
493
  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)
494
    {
495
496
497
498
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

499
500
501
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
502
	  spot::tgba_explicit* e;
503
504
	  to_free = a = e = spot::tgba_parse(input, pel, dict,
					     env, env, debug_opt);
505
	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
506
507
508
509
510
	    {
	      delete to_free;
	      delete dict;
	      return 2;
	    }
511
	  e->merge_transitions();
512
	}
513
      else
514
	{
515
	  if (redopt != spot::ltl::Reduce_None)
516
	    {
517
518
519
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
520
521
522
523
524
525
526
527
	      if (display_reduce_form && !redtau)
		std::cout << spot::ltl::to_string(f) << std::endl;
	    }
	  if (redtau)
	    {
	      spot::ltl::formula* t = spot::ltl::reduce_tau03(f, stronger);
	      spot::ltl::destroy(f);
	      f = t;
528
529
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
530
	    }
531

532
	  if (fm_opt)
533
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
534
					       fm_symb_merge_opt,
535
					       post_branching,
536
					       fair_loop_approx, unobservables,
537
					       fm_red, containment);
538
539
540
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
541

542
      spot::tgba_tba_proxy* degeneralized = 0;
543

544
545
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
546
	  && degeneralize_opt == NoDegen
547
548
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
549
550
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
551
	a = degeneralized = new spot::tgba_tba_proxy(a);
552
553
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
554

555
556
557
558
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
559
560
561
562

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

martinez's avatar
martinez committed
563
564
565
566
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
567
	    {
martinez's avatar
martinez committed
568
569
570
571
572
	      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))
573
574
575
576
		rel_dir =
		  spot::get_direct_relation_simulation(a,
						       std::cout,
						       display_parity_game);
martinez's avatar
martinez committed
577
578
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
579
580
581
582
		rel_del =
		  spot::get_delayed_relation_simulation(a,
							std::cout,
							display_parity_game);
583
584

	      if (display_rel_sim)
martinez's avatar
martinez committed
585
586
587
588
589
590
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
591

martinez's avatar
martinez committed
592
593
594
595
596
597
598
599
600
601
602
603
604
	      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);
605
606
607
	    }
	}

608
609
610
611
612
613
614
615
616
617
618
619
620
      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;
	}

621
622
      spot::tgba* product_degeneralized = 0;

623
      if (system)
624
625
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
626
627
628
629
630
631

	  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)
632
633
634
635
636
637
638
639
            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);
        }
640

641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
      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);
	    }
	}

659
660
      switch (output)
	{
661
662
663
	case -1:
	  /* No output.  */
	  break;
664
665
666
667
	case 0:
	  spot::dotty_reachable(std::cout, a);
	  break;
	case 1:
668
669
670
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
671
672
	  break;
	case 2:
673
674
675
	  if (concrete)
	    spot::bdd_print_dot(std::cout, concrete->get_dict(),
				concrete->
676
				get_core_data().acceptance_conditions);
677
678
	  break;
	case 3:
679
680
681
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->get_core_data().relation);
682
683
	  break;
	case 4:
684
685
686
	  if (concrete)
	    spot::bdd_print_set(std::cout, concrete->get_dict(),
				concrete->
687
				get_core_data().acceptance_conditions);
688
	  break;
689
	case 5:
690
	  a->get_dict()->dump(std::cout);
691
	  break;
692
693
694
	case 6:
	  spot::lbtt_reachable(std::cout, a);
	  break;
695
696
697
	case 7:
	  spot::tgba_save_reachable(std::cout, a);
	  break;
698
	case 8:
699
700
701
702
703
704
705
	  {
	    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;
	  }
706
707
708
	default:
	  assert(!"unknown output option");
	}
709

710
      if (echeck_inst)
711
	{
712
713
714
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
715
716
717
	  do
	    {
	      spot::emptiness_check_result* res = ec->check();
718
719
720
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
721
                  std::cout << std::left << std::setw(25)
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
                            << 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
742
                    std::cout << "no stats, , ";
743
744
745
746
747
748
749
750
751
752
753
754
                  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 &&
755
		      (!expect_counter_example || ec->safe()))
756
757
758
                    exit_code = 1;

                  if (!res)
759
                    {
760
                      std::cout << "no accepting run found";
761
                      if (!ec->safe() && expect_counter_example)
762
763
                        {
                          std::cout << " even if expected" << std::endl;
764
765
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
766
767
768
769
770
771
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
772
                    }
773
774
                  else
                    {
775

776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
                      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;
                        }
                    }
                }
812
813
	      delete res;
	    }
814
	  while (search_many);
815
	  delete ec;
martinez's avatar
martinez committed
816
817
	}

818
819
      if (f)
        spot::ltl::destroy(f);
820
821
      delete product_degeneralized;
      delete product_to_free;
822
      delete system;
823
824
      delete expl;
      delete aut_red;
825
      delete degeneralized;
826
      delete to_free;
827
      delete echeck_inst;
828
829
830
831
832
833
834
835
836
837
    }
  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);
838
  delete dict;
839
840
  return exit_code;
}