ltl2tgba.cc 28.8 KB
Newer Older
1
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
2
3
// 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 <cstdlib>
28
#include "ltlvisit/contain.hh"
29
#include "ltlvisit/tostring.hh"
30
#include "ltlvisit/apcollect.hh"
31
#include "ltlast/allnodes.hh"
32
#include "ltlparse/public.hh"
33
#include "tgbaalgos/ltl2tgba_lacim.hh"
34
#include "tgbaalgos/ltl2tgba_fm.hh"
35
#include "tgbaalgos/ltl2taa.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/tgbasgba.hh"
42
#include "tgba/tgbaproduct.hh"
43
#include "tgba/futurecondcol.hh"
44
#include "tgbaalgos/reducerun.hh"
45
#include "tgbaparse/public.hh"
46
#include "tgbaalgos/dupexp.hh"
47
#include "tgbaalgos/neverclaim.hh"
48
#include "tgbaalgos/reductgba_sim.hh"
49
#include "tgbaalgos/replayrun.hh"
50
#include "tgbaalgos/rundotdec.hh"
51
#include "misc/timer.hh"
52

53
#include "tgbaalgos/stats.hh"
54
#include "tgbaalgos/scc.hh"
55
56
#include "tgbaalgos/emptiness_stats.hh"

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

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

174
  bool debug_opt = false;
175
  bool paper_opt = false;
176
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
177
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
178
  bool taa_opt = false;
179
  bool fm_opt = false;
180
  int fm_red = spot::ltl::Reduce_None;
181
  bool fm_exprop_opt = false;
182
  bool fm_symb_merge_opt = true;
183
  bool file_opt = false;
184
  int output = 0;
185
  int formula_index = 0;
186
187
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
188
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
189
  bool expect_counter_example = false;
190
  bool from_file = false;
191
  int reduc_aut = spot::Reduce_None;
192
  int redopt = spot::ltl::Reduce_None;
193
194
  bool display_reduce_form = false;
  bool display_rel_sim = false;
195
  bool display_parity_game = false;
196
  bool post_branching = false;
197
  bool fair_loop_approx = false;
198
  bool graph_run_opt = false;
199
  bool graph_run_tgba_opt = false;
200
  bool opt_reduce = false;
201
  bool containment = false;
202
  bool show_fc = false;
203
204
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
205
206
  spot::tgba_explicit* system = 0;
  spot::tgba* product = 0;
207
  spot::tgba* product_to_free = 0;
208
  spot::bdd_dict* dict = new spot::bdd_dict();
209
210
  spot::timer_map tm;
  bool use_timer = false;
211

212
  for (;;)
213
    {
214
      if (argc < formula_index + 2)
215
	syntax(argv[0]);
216
217
218

      ++formula_index;

219
220
221
222
223
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
224
225
226
	{
	  output = 2;
	}
227
      else if (!strcmp(argv[formula_index], "-A"))
228
	{
229
	  output = 4;
230
	}
231
      else if (!strcmp(argv[formula_index], "-b"))
232
	{
233
	  output = 7;
234
	}
235
236
237
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
Damien Lefortier's avatar
Damien Lefortier committed
238
239
	  if (!taa_opt)
	    fm_opt = true;
240
	}
241
      else if (!strcmp(argv[formula_index], "-d"))
242
243
244
	{
	  debug_opt = true;
	}
245
246
      else if (!strcmp(argv[formula_index], "-D"))
	{
247
248
249
250
251
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
252
	}
253
      else if (!strncmp(argv[formula_index], "-e", 2))
254
        {
255
256
257
258
259
260
261
262
263
264
265
266
267
	  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);
	    }
268
269
270
          expect_counter_example = true;
          output = -1;
        }
271
      else if (!strncmp(argv[formula_index], "-E", 2))
272
        {
273
274
275
276
277
278
279
280
281
282
283
284
285
	  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);
	    }
286
287
288
          expect_counter_example = false;
          output = -1;
        }
289
290
291
292
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  taa_opt = true;
	}
293
294
295
296
      else if (!strcmp(argv[formula_index], "-f"))
	{
	  fm_opt = true;
	}
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
      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"))
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
	{
	  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"))
330
331
332
333
	{
	  fm_opt = true;
	  fm_red |= spot::ltl::Reduce_All;
	}
334
335
336
337
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
338
339
340
341
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
342
343
344
345
      else if (!strcmp(argv[formula_index], "-g"))
	{
	  graph_run_opt = true;
	}
346
347
348
349
      else if (!strcmp(argv[formula_index], "-G"))
	{
	  graph_run_tgba_opt = true;
	}
350
351
352
353
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
354
355
356
357
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
358
359
360
361
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
362
363
364
365
366
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
	  fm_opt = true;
	}
367
368
369
370
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
371
372
      else if (!strcmp(argv[formula_index], "-m"))
	{
373
	  opt_reduce = true;
374
	}
martinez's avatar
martinez committed
375
376
      else if (!strcmp(argv[formula_index], "-N"))
	{
377
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
378
379
	  output = 8;
	}
380
381
382
383
384
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
	  fm_opt = true;
	}
385
386
387
388
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
389
				    pel, dict, env, env, debug_opt);
390
391
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
392
393
	    return 2;
	  system->merge_transitions();
394
395
396

	  if (!paper_opt)
	    std::clog << argv[formula_index] + 2 << " read" << std::endl;
397
	}
398
399
      else if (!strcmp(argv[formula_index], "-r"))
	{
400
401
	  output = 1;
	}
402
403
404
405
406
407
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
408
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
409
410
411
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
412
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
413
414
415
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
416
417
418
 	  redopt |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
419
	}
420
421
      else if (!strcmp(argv[formula_index], "-r5"))
	{
422
	  redopt |= spot::ltl::Reduce_Containment_Checks;
423
424
425
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
426
	  redopt |= spot::ltl::Reduce_Containment_Checks_Stronger;
427
428
429
430
431
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
432
433
434
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
435
	}
martinez's avatar
martinez committed
436
437
438
439
440
441
442
443
444
      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"))
445
	{
martinez's avatar
martinez committed
446
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
447
	}
martinez's avatar
martinez committed
448
      else if (!strcmp(argv[formula_index], "-R2t"))
449
	{
martinez's avatar
martinez committed
450
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
	}
      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;
	}
468
469
470
471
472
473
474
475
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
476
477
478
479
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
480
481
482
483
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
484
485
486
487
488
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
	  fm_opt = true;
	  // Parse -U's argument.
489
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
490
491
492
493
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
494
	      tok = strtok(0, ", \t;");
495
496
	    }
	}
497
498
499
500
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
501
502
503
504
505
      else if (!strcmp(argv[formula_index], "-x"))
	{
	  fm_opt = true;
	  fm_exprop_opt = true;
	}
506
507
508
509
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
510
511
512
513
514
      else if (!strcmp(argv[formula_index], "-y"))
	{
	  fm_opt = true;
	  fm_symb_merge_opt = false;
	}
515
516
517
518
      else
	{
	  break;
	}
519
520
    }

521
  if ((graph_run_opt || graph_run_tgba_opt)
522
      && (!echeck_inst || !expect_counter_example))
523
    {
524
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
525
526
527
      exit(1);
    }

528
529
530
531
  std::string input;

  if (file_opt)
    {
532
      tm.start("reading formula");
533
      if (strcmp(argv[formula_index], "-"))
534
	{
535
	  std::ifstream fin(argv[formula_index]);
536
	  if (!fin)
537
538
539
540
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
541

542
	  if (!std::getline(fin, input, '\0'))
543
544
545
546
547
548
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
549
	{
550
	  std::getline(std::cin, input, '\0');
551
	}
552
      tm.stop("reading formula");
553
554
555
556
557
558
    }
  else
    {
      input = argv[formula_index];
    }

559
560
561
562
  spot::ltl::formula* f = 0;
  if (!from_file)
    {
      spot::ltl::parse_error_list pel;
563
      tm.start("parsing formula");
564
      f = spot::ltl::parse(input, pel, env, debug_opt);
565
      tm.stop("parsing formula");
566
567
568
      exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
    }
  if (f || from_file)
569
    {
570
571
572
573
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

574
575
576
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
577
	  spot::tgba_explicit* e;
578
	  tm.start("parsing automaton");
579
580
	  to_free = a = e = spot::tgba_parse(input, pel, dict,
					     env, env, debug_opt);
581
	  tm.stop("parsing automaton");
582
	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
583
584
585
586
587
	    {
	      delete to_free;
	      delete dict;
	      return 2;
	    }
588
	  e->merge_transitions();
589
	}
590
      else
591
	{
592
	  if (redopt != spot::ltl::Reduce_None)
593
	    {
594
	      tm.start("reducing formula");
595
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
596
	      f->destroy();
597
	      tm.stop("reducing formula");
598
	      f = t;
599
600
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
601
	    }
602

603
	  tm.start("translating formula");
604
	  if (fm_opt)
605
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
606
					       fm_symb_merge_opt,
607
					       post_branching,
608
					       fair_loop_approx, unobservables,
609
					       fm_red, containment);
610
	  else
611
	    if (taa_opt)
Damien Lefortier's avatar
Damien Lefortier committed
612
	      to_free = a = spot::ltl_to_taa(f, dict, containment);
613
614
	    else
	      to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
615
	  tm.stop("translating formula");
616
	}
617

618
      spot::tgba_tba_proxy* degeneralized = 0;
619
      spot::tgba_sgba_proxy* state_labeled = 0;
620

621
622
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
623
	  && degeneralize_opt == NoDegen
624
625
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
626
627
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
628
	a = degeneralized = new spot::tgba_tba_proxy(a);
629
630
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
631
632
633
634
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
635

636
637
638
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
639
	  tm.start("reducing formula automaton");
640
	  a = aut_red = new spot::tgba_reduc(a);
641
642
643
644

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

martinez's avatar
martinez committed
645
646
647
648
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
649
	    {
martinez's avatar
martinez committed
650
651
652
653
654
	      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))
655
656
657
658
659
660
661
662
		{
		  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
663
				    spot::Reduce_transition_Del_Sim))
664
665
666
667
668
669
670
		{
		  rel_del =
		    spot::get_delayed_relation_simulation(a,
							  std::cout,
							  display_parity_game);
		  assert(rel_del);
		}
671
672

	      if (display_rel_sim)
martinez's avatar
martinez committed
673
674
675
676
677
678
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
679

martinez's avatar
martinez committed
680
681
682
683
684
685
686
687
688
689
690
691
692
	      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);
693
	    }
694
	  tm.stop("reducing formula automaton");
695
696
	}

697
698
699
700
701
702
703
704
705
706
707
708
709
      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;
	}

710
711
      spot::tgba* product_degeneralized = 0;

712
      if (system)
713
714
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
715
716
717
718
719
720

	  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)
721
722
723
724
725
726
727
728
            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);
        }
729

730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
      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);
	    }
	}

748
749
750
751
752
      if (show_fc)
	{
	  a = new spot::future_conditions_collector(a, true);
	}

753
      if (output != -1)
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
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
	  tm.start("producing output");
	  switch (output)
	    {
	    case 0:
	      spot::dotty_reachable(std::cout, a);
	      break;
	    case 1:
	      if (concrete)
		spot::bdd_print_dot(std::cout, concrete->get_dict(),
				    concrete->get_core_data().relation);
	      break;
	    case 2:
	      if (concrete)
		spot::bdd_print_dot(std::cout, concrete->get_dict(),
				    concrete->
				    get_core_data().acceptance_conditions);
	      break;
	    case 3:
	      if (concrete)
		spot::bdd_print_set(std::cout, concrete->get_dict(),
				    concrete->get_core_data().relation);
	      break;
	    case 4:
	      if (concrete)
		spot::bdd_print_set(std::cout, concrete->get_dict(),
				    concrete->
				    get_core_data().acceptance_conditions);
	      break;
	    case 5:
	      a->get_dict()->dump(std::cout);
	      break;
	    case 6:
	      spot::lbtt_reachable(std::cout, a);
	      break;
	    case 7:
	      spot::tgba_save_reachable(std::cout, a);
	      break;
	    case 8:
	      {
		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;
	      }
	    case 9:
	      stats_reachable(a).dump(std::cout);
	      build_scc_stats(a).dump(std::cout);
	      break;
	    case 10:
	      dump_scc_dot(a, std::cout, false);
	      break;
	    case 11:
	      dump_scc_dot(a, std::cout, true);
	      break;
	    default:
	      assert(!"unknown output option");
	    }
	  tm.stop("producing output");
814
	}
815

816
      if (echeck_inst)
817
	{
818
819
820
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
821
822
	  do
	    {
823
	      tm.start("running emptiness check");
824
	      spot::emptiness_check_result* res = ec->check();
825
826
	      tm.stop("running emptiness check");

827
828
829
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
830
                  std::cout << std::left << std::setw(25)
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
                            << 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
851
                    std::cout << "no stats, , ";
852
853
854
855
856
857
858
859
860
861
862
863
                  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 &&
864
		      (!expect_counter_example || ec->safe()))
865
866
867
                    exit_code = 1;

                  if (!res)
868
                    {
869
                      std::cout << "no accepting run found";
870
                      if (!ec->safe() && expect_counter_example)
871
872
                        {
                          std::cout << " even if expected" << std::endl;
873
874
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
875
876
877
878
879
880
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
881
                    }
882
883
                  else
                    {
884

885
		      tm.start("computing accepting run");
886
                      spot::tgba_run* run = res->accepting_run();
887
888
		      tm.stop("computing accepting run");

889
890
891
892
893
894
895
896
                      if (!run)
                        {
                          std::cout << "an accepting run exists" << std::endl;
                        }
                      else
                        {
                          if (opt_reduce)
                            {
897
			      tm.start("reducing accepting run");
898
899
                              spot::tgba_run* redrun =
                                spot::reduce_run(res->automaton(), run);
900
			      tm.stop("reducing accepting run");
901
902
903
                              delete run;
                              run = redrun;
                            }
904
			  tm.start("printing accepting run");
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
                          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;
924
			  tm.stop("printing accepting run");
925
926
927
                        }
                    }
                }
928
929
	      delete res;
	    }
930
	  while (search_many);
931
	  delete ec;
martinez's avatar
martinez committed
932
933
	}

934
935
      if (show_fc)
	delete a;
936
      if (f)
937
        f->destroy();
938
939
      delete product_degeneralized;
      delete product_to_free;
940
      delete system;
941
942
      delete expl;
      delete aut_red;
943
      delete degeneralized;
944
      delete state_labeled;
945
      delete to_free;
946
      delete echeck_inst;
947
948
949
950
951
952
    }
  else
    {
      exit_code = 1;
    }

953
954
955
  if (use_timer)
    tm.print(std::cout);

956
957
958
959
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
960
	(*i)->destroy();
961
962
963
      delete unobservables;
    }

964
965
966
967
  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);
968
  assert(spot::ltl::automatop::instance_count() == 0);
969
  delete dict;
970
971
  return exit_code;
}