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

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

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

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

      ++formula_index;

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

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

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

477
478
479
480
  std::string input;

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

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

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

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

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

554
      spot::tgba_tba_proxy* degeneralized = 0;
555

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

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

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

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

	      if (display_rel_sim)
martinez's avatar
martinez committed
603
604
605
606
607
608
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
609

martinez's avatar
martinez committed
610
611
612
613
614
615
616
617
618
619
620
621
622
	      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);
623
624
625
	    }
	}

626
627
628
629
630
631
632
633
634
635
636
637
638
      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;
	}

639
640
      spot::tgba* product_degeneralized = 0;

641
      if (system)
642
643
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
644
645
646
647
648
649

	  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)
650
651
652
653
654
655
656
657
            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);
        }
658

659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
      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);
	    }
	}

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

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

                  if (!res)
777
                    {
778
                      std::cout << "no accepting run found";
779
                      if (!ec->safe() && expect_counter_example)
780
781
                        {
                          std::cout << " even if expected" << std::endl;
782
783
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
784
785
786
787
788
789
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
790
                    }
791
792
                  else
                    {
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
822
823
824
825
826
827
828
829
                      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;
                        }
                    }
                }
830
831
	      delete res;
	    }
832
	  while (search_many);
833
	  delete ec;
martinez's avatar
martinez committed
834
835
	}

836
837
      if (f)
        spot::ltl::destroy(f);
838
839
      delete product_degeneralized;
      delete product_to_free;
840
      delete system;
841
842
      delete expl;
      delete aut_red;
843
      delete degeneralized;
844
      delete to_free;
845
      delete echeck_inst;
846
847
848
849
850
851
852
853
854
855
    }
  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);
856
  delete dict;
857
858
  return exit_code;
}