ltl2tgba.cc 29.7 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
105
106
            << "  -l    use Couvreur's LaCIM algorithm for translation"
	    << std::endl
martinez's avatar
martinez committed
107
            << "  -L    fair-loop approximation (implies -f)" << std::endl
108
            << "  -lS   label acceptance conditions on states" << std::endl
109
	    << "  -m    try to reduce accepting runs, in a second pass"
110
	    << std::endl
111
112
113
114
	    << "  -N    display the never clain for Spin (implies -D)"
	    << std::endl
	    << "  -NN   display the never clain for Spin, with commented states"
	    << " (implies -D)" << std::endl
martinez's avatar
martinez committed
115
            << "  -p    branching postponement (implies -f)" << std::endl
116
117
	    << "  -Pfile  multiply the formula with the automaton from `file'."
	    << std::endl
martinez's avatar
martinez committed
118
	    << "  -r    display the relation BDD, not the reachability graph"
119
	    << std::endl
martinez's avatar
martinez committed
120
121
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
122
	    << "universality" << std::endl
martinez's avatar
martinez committed
123
	    << "  -r3   reduce formula using implication between "
124
	    << "sub-formulae" << std::endl
125
126
127
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
128
	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
martinez's avatar
martinez committed
129
130
	    << "  -rd   display the reduce formula" << std::endl
	    << "  -R    same as -r, but as a set" << std::endl
131
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
132
	    << "(use -L for more reduction)"
133
	    << std::endl
134
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
135
	    << "(use -L for more reduction)"
136
	    << std::endl
137
138
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
139
	    << std::endl
140
141
142
	    << "  -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
143
	    << "  -s    convert to explicit automata, and number states "
144
	    << "in DFS order" << std::endl
martinez's avatar
martinez committed
145
	    << "  -S    convert to explicit automata, and number states "
146
	    << "in BFS order" << std::endl
martinez's avatar
martinez committed
147
	    << "  -t    display reachable states in LBTT's format" << std::endl
148
149
            << "  -T    time the different phases of the translation"
	    << std::endl
150
151
152
153
            << "  -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
154
155
156
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl
            << "  -x    try to produce a more deterministic automata "
157
	    << "(implies -f)" << std::endl
martinez's avatar
martinez committed
158
	    << "  -X    do not compute an automaton, read it from a file"
159
	    << std::endl
martinez's avatar
martinez committed
160
	    << "  -y    do not merge states with same symbolic representation "
161
162
163
	    << "(implies -f)" << std::endl
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
164
165
166
167
168
169
	    << "  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;
170
171
172
173
174
175
176
177
  exit(2);
}

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

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

216
  for (;;)
217
    {
218
      if (argc < formula_index + 2)
219
	syntax(argv[0]);
220
221
222

      ++formula_index;

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

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

535
  if ((graph_run_opt || graph_run_tgba_opt)
536
      && (!echeck_inst || !expect_counter_example))
537
    {
538
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
539
540
541
      exit(1);
    }

542
543
544
545
  std::string input;

  if (file_opt)
    {
546
      tm.start("reading formula");
547
      if (strcmp(argv[formula_index], "-"))
548
	{
549
	  std::ifstream fin(argv[formula_index]);
550
	  if (!fin)
551
552
553
554
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
555

556
	  if (!std::getline(fin, input, '\0'))
557
558
559
560
561
562
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
563
	{
564
	  std::getline(std::cin, input, '\0');
565
	}
566
      tm.stop("reading formula");
567
568
569
570
571
572
    }
  else
    {
      input = argv[formula_index];
    }

573
574
575
576
  spot::ltl::formula* f = 0;
  if (!from_file)
    {
      spot::ltl::parse_error_list pel;
577
      tm.start("parsing formula");
578
      f = spot::ltl::parse(input, pel, env, debug_opt);
579
      tm.stop("parsing formula");
580
581
582
      exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
    }
  if (f || from_file)
583
    {
584
585
586
587
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

588
589
590
      if (from_file)
	{
	  spot::tgba_parse_error_list pel;
591
	  spot::tgba_explicit_string* e;
592
	  tm.start("parsing automaton");
593
594
	  to_free = a = e = spot::tgba_parse(input, pel, dict,
					     env, env, debug_opt);
595
	  tm.stop("parsing automaton");
596
	  if (spot::format_tgba_parse_errors(std::cerr, input, pel))
597
598
599
600
601
	    {
	      delete to_free;
	      delete dict;
	      return 2;
	    }
602
	  e->merge_transitions();
603
	}
604
      else
605
	{
606
	  if (redopt != spot::ltl::Reduce_None)
607
	    {
608
	      tm.start("reducing formula");
609
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
610
	      f->destroy();
611
	      tm.stop("reducing formula");
612
	      f = t;
613
614
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
615
	    }
616

617
	  tm.start("translating formula");
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
	  switch (translation)
	    {
	    case TransFM:
	      a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
				       fm_symb_merge_opt,
				       post_branching,
				       fair_loop_approx,
				       unobservables,
				       fm_red, containment);
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
	      a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	      break;
	    }
635
	  tm.stop("translating formula");
636
	  to_free = a;
637
	}
638

639
      spot::tgba_tba_proxy* degeneralized = 0;
640
      spot::tgba_sgba_proxy* state_labeled = 0;
641

642
643
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
644
	  && degeneralize_opt == NoDegen
645
646
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
647
648
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
649
	a = degeneralized = new spot::tgba_tba_proxy(a);
650
651
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
652
653
654
655
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
656

657
658
659
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
660
	  tm.start("reducing formula automaton");
661
	  a = aut_red = new spot::tgba_reduc(a);
662
663
664
665

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

martinez's avatar
martinez committed
666
667
668
669
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
670
	    {
martinez's avatar
martinez committed
671
672
673
674
675
	      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))
676
677
678
679
680
681
682
683
		{
		  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
684
				    spot::Reduce_transition_Del_Sim))
685
686
687
688
689
690
691
		{
		  rel_del =
		    spot::get_delayed_relation_simulation(a,
							  std::cout,
							  display_parity_game);
		  assert(rel_del);
		}
692
693

	      if (display_rel_sim)
martinez's avatar
martinez committed
694
695
696
697
698
699
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
700

martinez's avatar
martinez committed
701
702
703
704
705
706
707
708
709
710
711
712
713
	      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);
714
	    }
715
	  tm.stop("reducing formula automaton");
716
717
	}

718
719
720
721
722
723
724
725
726
727
728
729
730
      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;
	}

731
732
      spot::tgba* product_degeneralized = 0;

733
      if (system)
734
735
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
736
737
738
739
740
741

	  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)
742
743
744
745
746
747
748
749
            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);
        }
750

751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
      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);
	    }
	}

769
770
771
772
773
      if (show_fc)
	{
	  a = new spot::future_conditions_collector(a, true);
	}

774
      if (output != -1)
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
814
815
816
817
	  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);
818
		spot::never_claim_reachable(std::cout, s, f, spin_comments);
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
		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");
835
	}
836

837
      if (echeck_inst)
838
	{
839
840
841
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
842
843
	  do
	    {
844
	      tm.start("running emptiness check");
845
	      spot::emptiness_check_result* res = ec->check();
846
847
	      tm.stop("running emptiness check");

848
849
850
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
851
                  std::cout << std::left << std::setw(25)
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
                            << 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
872
                    std::cout << "no stats, , ";
873
874
875
876
877
878
879
880
881
882
883
884
                  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 &&
885
		      (!expect_counter_example || ec->safe()))
886
887
888
                    exit_code = 1;

                  if (!res)
889
                    {
890
                      std::cout << "no accepting run found";
891
                      if (!ec->safe() && expect_counter_example)
892
893
                        {
                          std::cout << " even if expected" << std::endl;
894
895
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
896
897
898
899
900
901
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
902
                    }
903
904
                  else
                    {
905

906
		      tm.start("computing accepting run");
907
                      spot::tgba_run* run = res->accepting_run();
908
909
		      tm.stop("computing accepting run");

910
911
912
913
914
915
916
917
                      if (!run)
                        {
                          std::cout << "an accepting run exists" << std::endl;
                        }
                      else
                        {
                          if (opt_reduce)
                            {
918
			      tm.start("reducing accepting run");
919
920
                              spot::tgba_run* redrun =
                                spot::reduce_run(res->automaton(), run);
921
			      tm.stop("reducing accepting run");
922
923
924
                              delete run;
                              run = redrun;
                            }
925
			  tm.start("printing accepting run");
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
                          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;
945
			  tm.stop("printing accepting run");
946
947
948
                        }
                    }
                }
949
950
	      delete res;
	    }
951
	  while (search_many);
952
	  delete ec;
martinez's avatar
martinez committed
953
954
	}

955
956
      if (show_fc)
	delete a;
957
      if (f)
958
        f->destroy();
959
960
      delete product_degeneralized;
      delete product_to_free;
961
      delete system;
962
963
      delete expl;
      delete aut_red;
964
      delete degeneralized;
965
      delete state_labeled;
966
      delete to_free;
967
      delete echeck_inst;
968
969
970
971
972
973
    }
  else
    {
      exit_code = 1;
    }

974
975
976
  if (use_timer)
    tm.print(std::cout);

977
978
979
980
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
981
	(*i)->destroy();
982
983
984
      delete unobservables;
    }

985
986
987
988
989
  spot::ltl::atomic_prop::dump_instances(std::cerr);
  spot::ltl::unop::dump_instances(std::cerr);
  spot::ltl::binop::dump_instances(std::cerr);
  spot::ltl::multop::dump_instances(std::cerr);
  spot::ltl::automatop::dump_instances(std::cerr);
990
991
992
993
  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);
994
  assert(spot::ltl::automatop::instance_count() == 0);
995
  delete dict;
996
997
  return exit_code;
}