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

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

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

182
  for (;;)
183
    {
184
      if (argc < formula_index + 2)
185
	syntax(argv[0]);
186
187
188

      ++formula_index;

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

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

431
  if ((graph_run_opt || graph_run_tgba_opt)
432
      && (!echeck_inst || !expect_counter_example))
433
    {
434
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
435
436
437
      exit(1);
    }

438
439
440
441
  std::string input;

  if (file_opt)
    {
442
      if (strcmp(argv[formula_index], "-"))
443
	{
444
	  std::ifstream fin(argv[formula_index]);
445
	  if (!fin)
446
447
448
449
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
450

451
	  if (!std::getline(fin, input, '\0'))
452
453
454
455
456
457
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
458
	{
459
	  std::getline(std::cin, input, '\0');
460
461
462
463
464
465
466
	}
    }
  else
    {
      input = argv[formula_index];
    }

467
468
469
470
471
472
473
474
  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)
475
    {
476
477
478
479
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

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

505
	  if (fm_opt)
506
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
507
					       fm_symb_merge_opt,
508
					       post_branching,
509
					       fair_loop_approx, unobservables,
510
					       fm_red, containment);
511
512
513
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
514

515
      spot::tgba_tba_proxy* degeneralized = 0;
516

517
518
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
519
	  && degeneralize_opt == NoDegen
520
521
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
522
523
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
524
	a = degeneralized = new spot::tgba_tba_proxy(a);
525
526
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
527

528
529
530
531
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
532
533
534
535

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

martinez's avatar
martinez committed
536
537
538
539
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
540
	    {
martinez's avatar
martinez committed
541
542
543
544
545
	      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))
546
547
548
549
		rel_dir =
		  spot::get_direct_relation_simulation(a,
						       std::cout,
						       display_parity_game);
martinez's avatar
martinez committed
550
551
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
552
553
554
555
		rel_del =
		  spot::get_delayed_relation_simulation(a,
							std::cout,
							display_parity_game);
556
557

	      if (display_rel_sim)
martinez's avatar
martinez committed
558
559
560
561
562
563
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
564

martinez's avatar
martinez committed
565
566
567
568
569
570
571
572
573
574
575
576
577
	      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);
578
579
580
	    }
	}

581
582
583
584
585
586
587
588
589
590
591
592
593
      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;
	}

594
595
      spot::tgba* product_degeneralized = 0;

596
      if (system)
597
598
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
599
600
601
602
603
604

	  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)
605
606
607
608
609
610
611
612
            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);
        }
613

614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
      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);
	    }
	}

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

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

                  if (!res)
732
                    {
733
                      std::cout << "no accepting run found";
734
                      if (!ec->safe() && expect_counter_example)
735
736
                        {
                          std::cout << " even if expected" << std::endl;
737
738
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
739
740
741
742
743
744
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
745
                    }
746
747
                  else
                    {
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
777
778
779
780
781
782
783
784
                      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;
                        }
                    }
                }
785
786
	      delete res;
	    }
787
	  while (search_many);
788
	  delete ec;
martinez's avatar
martinez committed
789
790
	}

791
792
      if (f)
        spot::ltl::destroy(f);
793
794
      delete product_degeneralized;
      delete product_to_free;
795
      delete system;
796
797
      delete expl;
      delete aut_red;
798
      delete degeneralized;
799
      delete to_free;
800
      delete echeck_inst;
801
802
803
804
805
806
807
808
809
810
    }
  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);
811
  delete dict;
812
813
  return exit_code;
}