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

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

155
  bool debug_opt = false;
156
  bool paper_opt = false;
157
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
158
  bool fm_opt = false;
159
  int fm_red = spot::ltl::Reduce_None;
160
  bool fm_exprop_opt = false;
161
  bool fm_symb_merge_opt = true;
162
  bool file_opt = false;
163
  int output = 0;
164
  int formula_index = 0;
165
166
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
167
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
168
  bool expect_counter_example = false;
169
  bool from_file = false;
170
  int reduc_aut = spot::Reduce_None;
171
  int redopt = spot::ltl::Reduce_None;
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
      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"))
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
	{
	  fm_opt = true;
 	  fm_red |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr5"))
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_Containment_Checks;
	}
      else if (!strcmp(argv[formula_index], "-fr6"))
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger;
	}
      else if (!strcmp(argv[formula_index], "-fr7"))
301
302
303
304
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_All;
	}
305
306
307
308
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
309
310
311
312
      else if (!strcmp(argv[formula_index], "-g"))
	{
	  graph_run_opt = true;
	}
313
314
315
316
      else if (!strcmp(argv[formula_index], "-G"))
	{
	  graph_run_tgba_opt = true;
	}
317
318
319
320
321
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
322
323
      else if (!strcmp(argv[formula_index], "-m"))
	{
324
	  opt_reduce = true;
325
	}
martinez's avatar
martinez committed
326
327
      else if (!strcmp(argv[formula_index], "-N"))
	{
328
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
329
330
	  output = 8;
	}
331
332
333
334
335
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
336
337
338
339
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
340
				    pel, dict, env, env, debug_opt);
341
342
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
343
344
	    return 2;
	  system->merge_transitions();
345
346
347

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

468
  if ((graph_run_opt || graph_run_tgba_opt)
469
      && (!echeck_inst || !expect_counter_example))
470
    {
471
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
472
473
474
      exit(1);
    }

475
476
477
478
  std::string input;

  if (file_opt)
    {
479
      if (strcmp(argv[formula_index], "-"))
480
	{
481
	  std::ifstream fin(argv[formula_index]);
482
	  if (!fin)
483
484
485
486
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
487

488
	  if (!std::getline(fin, input, '\0'))
489
490
491
492
493
494
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
495
	{
496
	  std::getline(std::cin, input, '\0');
497
498
499
500
501
502
503
	}
    }
  else
    {
      input = argv[formula_index];
    }

504
505
506
507
508
509
510
511
  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)
512
    {
513
514
515
516
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

517
518
519
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
520
	  spot::tgba_explicit* e;
521
522
	  to_free = a = e = spot::tgba_parse(input, pel, dict,
					     env, env, debug_opt);
523
	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
524
525
526
527
528
	    {
	      delete to_free;
	      delete dict;
	      return 2;
	    }
529
	  e->merge_transitions();
530
	}
531
      else
532
	{
533
	  if (redopt != spot::ltl::Reduce_None)
534
	    {
535
536
537
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
	      spot::ltl::destroy(f);
	      f = t;
538
539
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
540
	    }
541

542
	  if (fm_opt)
543
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
544
					       fm_symb_merge_opt,
545
					       post_branching,
546
					       fair_loop_approx, unobservables,
547
					       fm_red, containment);
548
549
550
	  else
	    to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	}
551

552
      spot::tgba_tba_proxy* degeneralized = 0;
553

554
555
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
556
	  && degeneralize_opt == NoDegen
557
558
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
559
560
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
561
	a = degeneralized = new spot::tgba_tba_proxy(a);
562
563
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
564

565
566
567
568
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
	  a = aut_red = new spot::tgba_reduc(a);
569
570
571
572

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

martinez's avatar
martinez committed
573
574
575
576
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
577
	    {
martinez's avatar
martinez committed
578
579
580
581
582
	      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))
583
584
585
586
		rel_dir =
		  spot::get_direct_relation_simulation(a,
						       std::cout,
						       display_parity_game);
martinez's avatar
martinez committed
587
588
	      else if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
				    spot::Reduce_transition_Del_Sim))
589
590
591
592
		rel_del =
		  spot::get_delayed_relation_simulation(a,
							std::cout,
							display_parity_game);
593
594

	      if (display_rel_sim)
martinez's avatar
martinez committed
595
596
597
598
599
600
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
601

martinez's avatar
martinez committed
602
603
604
605
606
607
608
609
610
611
612
613
614
	      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);
615
616
617
	    }
	}

618
619
620
621
622
623
624
625
626
627
628
629
630
      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;
	}

631
632
      spot::tgba* product_degeneralized = 0;

633
      if (system)
634
635
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
636
637
638
639
640
641

	  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)
642
643
644
645
646
647
648
649
            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);
        }
650

651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
      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);
	    }
	}

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

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

                  if (!res)
769
                    {
770
                      std::cout << "no accepting run found";
771
                      if (!ec->safe() && expect_counter_example)
772
773
                        {
                          std::cout << " even if expected" << std::endl;
774
775
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
776
777
778
779
780
781
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
782
                    }
783
784
                  else
                    {
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
812
813
814
815
816
817
818
819
820
821
                      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;
                        }
                    }
                }
822
823
	      delete res;
	    }
824
	  while (search_many);
825
	  delete ec;
martinez's avatar
martinez committed
826
827
	}

828
829
      if (f)
        spot::ltl::destroy(f);
830
831
      delete product_degeneralized;
      delete product_to_free;
832
      delete system;
833
834
      delete expl;
      delete aut_red;
835
      delete degeneralized;
836
      delete to_free;
837
      delete echeck_inst;
838
839
840
841
842
843
844
845
846
847
    }
  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);
848
  delete dict;
849
850
  return exit_code;
}