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

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

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

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

      ++formula_index;

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

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

530
  if ((graph_run_opt || graph_run_tgba_opt)
531
      && (!echeck_inst || !expect_counter_example))
532
    {
533
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
534
535
536
      exit(1);
    }

537
538
539
540
  std::string input;

  if (file_opt)
    {
541
      tm.start("reading formula");
542
      if (strcmp(argv[formula_index], "-"))
543
	{
544
	  std::ifstream fin(argv[formula_index]);
545
	  if (!fin)
546
547
548
549
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
550

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

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

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

612
	  tm.start("translating formula");
613
	  if (fm_opt)
614
	    to_free = a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
615
					       fm_symb_merge_opt,
616
					       post_branching,
617
					       fair_loop_approx, unobservables,
618
					       fm_red, containment);
619
	  else
620
	    if (taa_opt)
Damien Lefortier's avatar
Damien Lefortier committed
621
	      to_free = a = spot::ltl_to_taa(f, dict, containment);
622
623
	    else
	      to_free = a = concrete = spot::ltl_to_tgba_lacim(f, dict);
624
	  tm.stop("translating formula");
625
	}
626

627
      spot::tgba_tba_proxy* degeneralized = 0;
628
      spot::tgba_sgba_proxy* state_labeled = 0;
629

630
631
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
632
	  && degeneralize_opt == NoDegen
633
634
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
635
636
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
637
	a = degeneralized = new spot::tgba_tba_proxy(a);
638
639
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
640
641
642
643
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
644

645
646
647
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
648
	  tm.start("reducing formula automaton");
649
	  a = aut_red = new spot::tgba_reduc(a);
650
651
652
653

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

martinez's avatar
martinez committed
654
655
656
657
	  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
			   spot::Reduce_transition_Dir_Sim |
			   spot::Reduce_quotient_Del_Sim |
			   spot::Reduce_transition_Del_Sim))
658
	    {
martinez's avatar
martinez committed
659
660
661
662
663
	      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))
664
665
666
667
668
669
670
671
		{
		  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
672
				    spot::Reduce_transition_Del_Sim))
673
674
675
676
677
678
679
		{
		  rel_del =
		    spot::get_delayed_relation_simulation(a,
							  std::cout,
							  display_parity_game);
		  assert(rel_del);
		}
680
681

	      if (display_rel_sim)
martinez's avatar
martinez committed
682
683
684
685
686
687
		{
		  if (rel_dir)
		    aut_red->display_rel_sim(rel_dir, std::cout);
		  if (rel_del)
		    aut_red->display_rel_sim(rel_del, std::cout);
		}
688

martinez's avatar
martinez committed
689
690
691
692
693
694
695
696
697
698
699
700
701
	      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);
702
	    }
703
	  tm.stop("reducing formula automaton");
704
705
	}

706
707
708
709
710
711
712
713
714
715
716
717
718
      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;
	}

719
720
      spot::tgba* product_degeneralized = 0;

721
      if (system)
722
723
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
724
725
726
727
728
729

	  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)
730
731
732
733
734
735
736
737
            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);
        }
738

739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
      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);
	    }
	}

757
758
759
760
761
      if (show_fc)
	{
	  a = new spot::future_conditions_collector(a, true);
	}

762
      if (output != -1)
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
	  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);
806
		spot::never_claim_reachable(std::cout, s, f, spin_comments);
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
		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");
823
	}
824

825
      if (echeck_inst)
826
	{
827
828
829
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
830
831
	  do
	    {
832
	      tm.start("running emptiness check");
833
	      spot::emptiness_check_result* res = ec->check();
834
835
	      tm.stop("running emptiness check");

836
837
838
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
839
                  std::cout << std::left << std::setw(25)
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
                            << 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
860
                    std::cout << "no stats, , ";
861
862
863
864
865
866
867
868
869
870
871
872
                  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 &&
873
		      (!expect_counter_example || ec->safe()))
874
875
876
                    exit_code = 1;

                  if (!res)
877
                    {
878
                      std::cout << "no accepting run found";
879
                      if (!ec->safe() && expect_counter_example)
880
881
                        {
                          std::cout << " even if expected" << std::endl;
882
883
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
884
885
886
887
888
889
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
890
                    }
891
892
                  else
                    {
893

894
		      tm.start("computing accepting run");
895
                      spot::tgba_run* run = res->accepting_run();
896
897
		      tm.stop("computing accepting run");

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

943
944
      if (show_fc)
	delete a;
945
      if (f)
946
        f->destroy();
947
948
      delete product_degeneralized;
      delete product_to_free;
949
      delete system;
950
951
      delete expl;
      delete aut_red;
952
      delete degeneralized;
953
      delete state_labeled;
954
      delete to_free;
955
      delete echeck_inst;
956
957
958
959
960
961
    }
  else
    {
      exit_code = 1;
    }

962
963
964
  if (use_timer)
    tm.print(std::cout);

965
966
967
968
  if (unobservables)
    {
      for (spot::ltl::atomic_prop_set::iterator i =
	     unobservables->begin(); i != unobservables->end(); ++i)
969
	(*i)->destroy();
970
971
972
      delete unobservables;
    }

973
974
975
976
977
  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);
978
979
980
981
  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);
982
  assert(spot::ltl::automatop::instance_count() == 0);
983
  delete dict;
984
985
  return exit_code;
}