ltl2tgba.cc 36.8 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
// Copyright (C) 2007, 2008, 2009, 2010 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
3
4
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis
5
// Coopratifs (SRC), Universit Pierre et Marie Curie.
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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.

24
#include <iostream>
25
#include <iomanip>
26
#include <cassert>
27
28
#include <fstream>
#include <string>
29
#include <cstdlib>
30
#include "ltlvisit/contain.hh"
31
#include "ltlvisit/tostring.hh"
32
#include "ltlvisit/apcollect.hh"
33
#include "ltlast/allnodes.hh"
34
#include "ltlparse/public.hh"
35
#include "tgbaalgos/ltl2tgba_lacim.hh"
36
#include "tgbaalgos/ltl2tgba_fm.hh"
37
#include "tgbaalgos/ltl2taa.hh"
38
#include "tgba/bddprint.hh"
39
#include "tgbaalgos/save.hh"
40
#include "tgbaalgos/dotty.hh"
41
#include "tgbaalgos/lbtt.hh"
42
#include "tgba/tgbatba.hh"
43
#include "tgba/tgbasgba.hh"
44
#include "tgba/tgbaproduct.hh"
45
#include "tgba/futurecondcol.hh"
46
#include "tgbaalgos/reducerun.hh"
47
#include "tgbaparse/public.hh"
48
#include "neverparse/public.hh"
49
#include "tgbaalgos/dupexp.hh"
Felix Abecassis's avatar
Felix Abecassis committed
50
#include "tgbaalgos/minimize.hh"
51
#include "tgbaalgos/neverclaim.hh"
52
#include "tgbaalgos/reductgba_sim.hh"
53
#include "tgbaalgos/replayrun.hh"
54
#include "tgbaalgos/rundotdec.hh"
55
#include "tgbaalgos/sccfilter.hh"
56
57
#include "tgbaalgos/eltl2tgba_lacim.hh"
#include "eltlparse/public.hh"
58
#include "misc/timer.hh"
59

60
#include "tgbaalgos/stats.hh"
61
#include "tgbaalgos/scc.hh"
62
63
#include "tgbaalgos/emptiness_stats.hh"

64
65
66
67
68
69
70
71
72
73
74
75
std::string
ltl_defs()
{
  std::string s = "\
X=(0 1 true	   \
   1 2 $0	   \
   accept 2)	   \
U=(0 0 $0	   \
   0 1 $1	   \
   accept 1)	   \
G=(0 0 $0)	   \
F=U(true, $0)	   \
76
77
78
W=G($0)|U($0, $1)  \
R=!U(!$0, !$1)     \
M=F($0)&R($0, $1)";
79
80
81
  return s;
}

82
83
84
void
syntax(char* prog)
{
85
86
87
88
89
  // Display the supplied name unless it appears to be a libtool wrapper.
  char* slash = strrchr(prog, '/');
  if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
    prog = slash + 4;

90
  std::cerr << "Usage: "<< prog << " [-f|-l|-le|-taa] [OPTIONS...] formula"
91
	    << std::endl
92
            << "       "<< prog << " [-f|-l|-le|-taa] -F [OPTIONS...] file"
93
	    << std::endl
94
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
95
	    << std::endl
96

97
98
            << "Translate an LTL formula into an automaton, or read the "
	    << "automaton from a file." << std::endl
99
100
101
102
	    << "Optionally multiply this automaton by another"
	    << " automaton read from a file." << std::endl
            << "Output the result in various formats, or perform an emptiness "
            << "check." << std::endl
103
	    << std::endl
104
105
106

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
107
	    << std::endl
108
	    << "  -X    do not compute an automaton, read it from a file"
109
	    << std::endl
110
111
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
112
113
	    << "  -Pfile  multiply the formula automaton with the automaton"
	    << " from `file'"
114
	    << std::endl
115
116
117
	    << std::endl

	    << "Translation algorithm:" << std::endl
118
            << "  -f    use Couvreur's FM algorithm for LTL"
119
	    << "(default)"
120
	    << std::endl
121
            << "  -l    use Couvreur's LaCIM algorithm for LTL "
122
	    << std::endl
123
124
125
	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
	    << std::endl
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
126
	    << std::endl
127
128
129
	    << std::endl

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
130
131
132
133
	    << "  -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
134
135
136
	    << "  -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
137
138
139
140
141
            << "  -L    fair-loop approximation (implies -f)" << std::endl
            << "  -p    branching postponement (implies -f)" << std::endl
            << "  -U[PROPS]  consider atomic properties of the formula as "
	    << "exclusive events, and" << std::endl
	    << "        PROPS as unobservables events (implies -f)"
142
	    << std::endl
143
144
145
146
            << "  -x    try to produce a more deterministic automaton "
	    << "(implies -f)" << std::endl
	    << "  -y    do not merge states with same symbolic representation "
	    << "(implies -f)" << std::endl
147
	    << std::endl
148

149
150
	    << "Options for Couvreur's LaCIM algorithm (-l or -le):"
	    << std::endl
151
152
	    << "  -a    display the acceptance_conditions BDD, not the "
	    << "reachability graph"
153
	    << std::endl
154
	    << "  -A    same as -a, but as a set" << std::endl
155
156
	    << "  -lo   pre-define standard LTL operators as automata "
	    << "(implies -le)" << std::endl
157
	    << "  -r    display the relation BDD, not the reachability graph"
158
	    << std::endl
159
	    << "  -R    same as -r, but as a set" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
160
161
	    << "  -R3b  symbolically prune unaccepting SCC from BDD relation"
	    << std::endl
162
	    << std::endl
163
164

	    << "Options for Tauriainen's TAA-based algorithm (-taa):"
165
	    << std::endl
166
	    << "  -c    enable language containment checks (implies -taa)"
167
	    << std::endl
168
	    << std::endl
169
170

	    << "Formula simplification (before translation):"
171
	    << std::endl
martinez's avatar
martinez committed
172
173
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
174
	    << "universality" << std::endl
martinez's avatar
martinez committed
175
	    << "  -r3   reduce formula using implication between "
176
	    << "sub-formulae" << std::endl
177
178
179
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
180
	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
181
182
183
184
185
186
187
188
189
190
191
192
193
194
	    << "  -rd   display the reduced formula" << std::endl
	    << std::endl

	    << "Automaton degeneralization (after translation):"
	    << std::endl
            << "  -lS   move generalized acceptance conditions to states "
	    << "(SGBA)" << std::endl
	    << "  -D    degeneralize the automaton as a TBA" << std::endl
	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
	    << std::endl


	    << "Automaton simplifications (after translation):"
	    << std::endl
195
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
196
	    << "(use -L for more reduction)"
197
	    << std::endl
198
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
199
	    << "(use -L for more reduction)"
200
	    << std::endl
201
202
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
203
	    << std::endl
204
	    << "  -R3   use SCC to reduce the automata" << std::endl
205
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
206
207
208
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
209
210
	    << "  -Rd   display the simulation relation" << std::endl
	    << "  -RD   display the parity game (dot format)" << std::endl
Felix Abecassis's avatar
Felix Abecassis committed
211
            << "  -Rm   attempt to minimize the automata" << std::endl
212
	    << std::endl
213
214
215
216
217

	    << "Options for performing emptiness checks:" << std::endl
	    << "  -e[ALGO]  run emptiness check, expect and compute an "
	    << "accepting run" << std::endl
	    << "  -E[ALGO]  run emptiness check, expect no accepting run"
martinez's avatar
martinez committed
218
	    << std::endl
219
220
221
222
	    << "  -C    compute an accepting run (Counterexample) if it exists"
	    << std::endl
	    << "  -CR   compute and replay an accepting run (implies -C)"
	    << std::endl
223
	    << "  -g    graph the accepting run on the automaton (requires -e)"
224
	    << std::endl
225
226
227
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
	    << "  -m    try to reduce accepting runs, in a second pass"
228
229
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
230
231
232
233
234
	    << "  Cou99(OPTIONS) (the default)" << std::endl
	    << "  CVWY90(OPTIONS)" << std::endl
	    << "  GV04(OPTIONS)" << std::endl
	    << "  SE05(OPTIONS)" << std::endl
	    << "  Tau03(OPTIONS)" << std::endl
235
236
237
238
239
240
241
242
243
244
245
246
247
	    << "  Tau03_opt(OPTIONS)" << std::endl
	    << std::endl

	    << "If no emptiness check is run, the automaton will be output "
	    << "in dot format" << std::endl << "by default.  This can be "
	    << "changed with the following options." << std::endl
	    << std::endl

	    << "Output options (if no emptiness check):" << std::endl
	    << "  -b    output the automaton in the format of spot"
            << std::endl
            << "  -FC   dump the automaton showing future conditions on states"
	    << std::endl
248
249
250
	    << "  -k    display statistics on the automaton (size and SCCs)"
	    << std::endl
	    << "  -ks   display statistics on the automaton (size only)"
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
	    << std::endl
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
	    << std::endl
	    << "  -N    output the never clain for Spin (implies -D)"
	    << std::endl
	    << "  -NN   output the never clain for Spin, with commented states"
	    << " (implies -D)" << std::endl
	    << "  -t    output automaton in LBTT's format" << std::endl
	    << std::endl

	    << "Miscellaneous options:" << std::endl
	    << "  -0    produce minimal output dedicated to the paper"
	    << std::endl
	    << "  -d    turn on traces during parsing" << std::endl
	    << "  -s    convert to explicit automata, and number states "
	    << "in DFS order" << std::endl
	    << "  -S    convert to explicit automata, and number states "
	    << "in BFS order" << std::endl
            << "  -T    time the different phases of the translation"
	    << std::endl
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl;
274
275
276
277
278
279
280
281
  exit(2);
}

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

282
  bool debug_opt = false;
283
  bool paper_opt = false;
284
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
285
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
286
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
287
    translation = TransFM;
288
  int fm_red = spot::ltl::Reduce_None;
289
  bool fm_exprop_opt = false;
290
  bool fm_symb_merge_opt = true;
291
  bool file_opt = false;
292
  int output = 0;
293
  int formula_index = 0;
294
295
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
296
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
297
  bool expect_counter_example = false;
298
299
  bool accepting_run = false;
  bool accepting_run_replay = false;
300
  bool from_file = false;
301
  bool read_neverclaim = false;
302
  int reduc_aut = spot::Reduce_None;
303
  int redopt = spot::ltl::Reduce_None;
304
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
305
  bool symbolic_scc_pruning = false;
306
307
  bool display_reduce_form = false;
  bool display_rel_sim = false;
308
  bool display_parity_game = false;
309
  bool post_branching = false;
310
  bool fair_loop_approx = false;
311
  bool graph_run_opt = false;
312
  bool graph_run_tgba_opt = false;
313
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
314
  bool opt_minimize = false;
315
  bool containment = false;
316
  bool show_fc = false;
317
  bool spin_comments = false;
318
319
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
320
  spot::tgba_explicit_string* system = 0;
321
  spot::tgba* product = 0;
322
  spot::tgba* product_to_free = 0;
323
  spot::bdd_dict* dict = new spot::bdd_dict();
324
325
  spot::timer_map tm;
  bool use_timer = false;
326

327
  for (;;)
328
    {
329
      if (argc < formula_index + 2)
330
	syntax(argv[0]);
331
332
333

      ++formula_index;

334
335
336
337
338
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
339
340
341
	{
	  output = 2;
	}
342
      else if (!strcmp(argv[formula_index], "-A"))
343
	{
344
	  output = 4;
345
	}
346
      else if (!strcmp(argv[formula_index], "-b"))
347
	{
348
	  output = 7;
349
	}
350
351
352
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
353
	  translation = TransTAA;
354
	}
355
356
357
358
359
360
361
362
363
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
364
      else if (!strcmp(argv[formula_index], "-d"))
365
366
367
	{
	  debug_opt = true;
	}
368
369
      else if (!strcmp(argv[formula_index], "-D"))
	{
370
371
372
373
374
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
375
	}
376
      else if (!strncmp(argv[formula_index], "-e", 2))
377
        {
378
379
380
381
382
383
384
385
386
387
388
389
390
	  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);
	    }
391
392
393
          expect_counter_example = true;
          output = -1;
        }
394
      else if (!strncmp(argv[formula_index], "-E", 2))
395
        {
396
397
398
399
400
401
402
403
404
405
406
407
408
	  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);
	    }
409
410
411
          expect_counter_example = false;
          output = -1;
        }
412
413
      else if (!strcmp(argv[formula_index], "-f"))
	{
414
	  translation = TransFM;
415
	}
416
417
      else if (!strcmp(argv[formula_index], "-fr1"))
	{
418
	  translation = TransFM;
419
420
421
422
	  fm_red |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-fr2"))
	{
423
	  translation = TransFM;
424
425
426
427
	  fm_red |= spot::ltl::Reduce_Eventuality_And_Universality;
	}
      else if (!strcmp(argv[formula_index], "-fr3"))
	{
428
	  translation = TransFM;
429
430
431
	  fm_red |= spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr4"))
432
	{
433
	  translation = TransFM;
434
435
436
437
438
439
 	  fm_red |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr5"))
	{
440
	  translation = TransFM;
441
442
443
444
	  fm_red |= spot::ltl::Reduce_Containment_Checks;
	}
      else if (!strcmp(argv[formula_index], "-fr6"))
	{
445
	  translation = TransFM;
446
447
448
	  fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger;
	}
      else if (!strcmp(argv[formula_index], "-fr7"))
449
	{
450
	  translation = TransFM;
451
452
	  fm_red |= spot::ltl::Reduce_All;
	}
453
454
455
456
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
457
458
459
460
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
461
462
      else if (!strcmp(argv[formula_index], "-g"))
	{
463
	  accepting_run = true;
464
465
	  graph_run_opt = true;
	}
466
467
      else if (!strcmp(argv[formula_index], "-G"))
	{
468
	  accepting_run = true;
469
470
	  graph_run_tgba_opt = true;
	}
471
472
473
474
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
475
476
477
478
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
479
480
481
482
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
483
484
485
486
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
487
488
489
490
      else if (!strcmp(argv[formula_index], "-l"))
	{
	  translation = TransLaCIM;
	}
491
492
493
494
495
496
497
498
499
500
      else if (!strcmp(argv[formula_index], "-le"))
	{
	  /* -lo is documented to imply -le, so do not overwrite it. */
	  if (translation != TransLaCIM_ELTL_ops)
	    translation = TransLaCIM_ELTL;
	}
      else if (!strcmp(argv[formula_index], "-lo"))
	{
	  translation = TransLaCIM_ELTL_ops;
	}
501
502
503
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
504
	  translation = TransFM;
505
	}
506
507
508
509
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
510
511
      else if (!strcmp(argv[formula_index], "-m"))
	{
512
	  opt_reduce = true;
513
	}
martinez's avatar
martinez committed
514
515
      else if (!strcmp(argv[formula_index], "-N"))
	{
516
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
517
518
	  output = 8;
	}
519
520
521
522
523
524
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
	  spin_comments = true;
	}
525
526
527
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
528
	  translation = TransFM;
529
	}
530
531
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
532
533
	  tm.start("reading -P's argument");

534
535
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
536
				    pel, dict, env, env, debug_opt);
537
538
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
539
540
	    return 2;
	  system->merge_transitions();
541

542
	  tm.stop("reading -P's argument");
543
	}
544
545
      else if (!strcmp(argv[formula_index], "-r"))
	{
546
547
	  output = 1;
	}
548
549
550
551
552
553
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
554
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
555
556
557
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
558
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
559
560
561
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
562
563
564
 	  redopt |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
565
	}
566
567
      else if (!strcmp(argv[formula_index], "-r5"))
	{
568
	  redopt |= spot::ltl::Reduce_Containment_Checks;
569
570
571
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
572
	  redopt |= spot::ltl::Reduce_Containment_Checks_Stronger;
573
574
575
576
577
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
578
579
580
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
581
	}
martinez's avatar
martinez committed
582
583
584
585
586
587
588
589
590
      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"))
591
	{
martinez's avatar
martinez committed
592
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
593
	}
martinez's avatar
martinez committed
594
      else if (!strcmp(argv[formula_index], "-R2t"))
595
	{
martinez's avatar
martinez committed
596
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
597
598
599
600
601
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	}
602
603
604
605
606
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	  scc_filter_all = true;
	}
607
608
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
609
	  symbolic_scc_pruning = true;
610
	}
611
612
613
614
615
616
617
618
619
620
621
622
      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;
	}
Felix Abecassis's avatar
Felix Abecassis committed
623
624
625
626
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
627
628
629
630
631
632
633
634
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
635
636
637
638
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
639
640
641
642
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
643
644
645
646
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
647
648
649
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
650
	  translation = TransFM;
651
	  // Parse -U's argument.
652
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
653
654
655
656
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
657
	      tok = strtok(0, ", \t;");
658
659
	    }
	}
660
661
662
663
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
664
665
      else if (!strcmp(argv[formula_index], "-x"))
	{
666
	  translation = TransFM;
667
668
	  fm_exprop_opt = true;
	}
669
670
671
672
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
673
674
675
676
677
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  read_neverclaim = true;
	}
678
679
      else if (!strcmp(argv[formula_index], "-y"))
	{
680
	  translation = TransFM;
681
682
	  fm_symb_merge_opt = false;
	}
683
684
685
686
      else
	{
	  break;
	}
687
688
    }

689
  if ((graph_run_opt || graph_run_tgba_opt)
690
      && (!echeck_inst || !expect_counter_example))
691
    {
692
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
693
694
695
      exit(1);
    }

696
697
698
699
  std::string input;

  if (file_opt)
    {
700
      tm.start("reading formula");
701
      if (strcmp(argv[formula_index], "-"))
702
	{
703
	  std::ifstream fin(argv[formula_index]);
704
	  if (!fin)
705
706
707
708
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
709

710
	  if (!std::getline(fin, input, '\0'))
711
712
713
714
715
716
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
717
	{
718
	  std::getline(std::cin, input, '\0');
719
	}
720
      tm.stop("reading formula");
721
722
723
724
725
726
    }
  else
    {
      input = argv[formula_index];
    }

727
  spot::ltl::formula* f = 0;
728
  if (!from_file) // Reading a formula, not reading an automaton from a file.
729
    {
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
      switch (translation)
	{
	case TransFM:
	case TransLaCIM:
	case TransTAA:
	  {
	    spot::ltl::parse_error_list pel;
	    tm.start("parsing formula");
	    f = spot::ltl::parse(input, pel, env, debug_opt);
	    tm.stop("parsing formula");
	    exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
	  }
	  break;
	case TransLaCIM_ELTL:
	  {
	    spot::eltl::parse_error_list p;
	    tm.start("parsing formula");
	    f = spot::eltl::parse_string(input, p, env, false);
	    tm.stop("parsing formula");
	    exit_code = spot::eltl::format_parse_errors(std::cerr, p);
	  }
	  break;
	case TransLaCIM_ELTL_ops:
	  {
	    // Call the LTL parser first to handle operators such as
	    // [] or <> and rewrite the output as a string with G or F.
	    // Then prepend definitions of usual LTL operators, and parse
	    // the result again as an ELTL formula.
	    spot::ltl::parse_error_list pel;
	    tm.start("parsing formula");
	    f = spot::ltl::parse(input, pel, env, debug_opt);
	    input = ltl_defs();
	    input += "%";
	    input += spot::ltl::to_string(f, true);
	    f->destroy();
	    spot::eltl::parse_error_list p;
	    f = spot::eltl::parse_string(input, p, env, debug_opt);
	    tm.stop("parsing formula");
	    exit_code = spot::eltl::format_parse_errors(std::cerr, p);
	  }
	  break;
771
	}
772
773
    }
  if (f || from_file)
774
    {
775
776
777
778
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

779
780
      if (from_file)
	{
781
	  spot::tgba_explicit_string* e;
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
	  if (!read_neverclaim)
	    {
	      spot::tgba_parse_error_list pel;
	      tm.start("parsing automaton");
	      to_free = a = e = spot::tgba_parse(input, pel, dict,
						 env, env, debug_opt);
	      tm.stop("parsing automaton");
	      if (spot::format_tgba_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
		}
	    }
	  else
797
	    {
798
	      spot::neverclaim_parse_error_list pel;
799
	      tm.start("parsing neverclaim");
800
801
	      to_free = a = e = spot::neverclaim_parse(input, pel, dict,
						       env, debug_opt);
802
	      tm.stop("parsing neverclaim");
803
804
805
806
807
	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
808
		}
809
	    }
810
	  e->merge_transitions();
811
	}
812
      else
813
	{
814
	  if (redopt != spot::ltl::Reduce_None)
815
	    {
816
	      tm.start("reducing formula");
817
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
818
	      f->destroy();
819
	      tm.stop("reducing formula");
820
	      f = t;
821
822
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
823
	    }
824

825
	  tm.start("translating formula");
826
827
828
829
830
831
832
833
	  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,
834
				       fm_red);
835
836
837
838
839
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
840
841
842
843
844
	      a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	      break;
	    case TransLaCIM_ELTL:
	    case TransLaCIM_ELTL_ops:
	      a = concrete = spot::eltl_to_tgba_lacim(f, dict);
845
846
	      break;
	    }
847
	  tm.stop("translating formula");
848
	  to_free = a;
849
	}
850

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
      if (symbolic_scc_pruning)
        {
	  spot::tgba_bdd_concrete* bc =
	    dynamic_cast<spot::tgba_bdd_concrete*>(a);
	  if (!bc)
	    {
	      std::cerr << ("Error: Automaton is not symbolic: cannot "
			    "prune SCCs symbolically.\n"
			    "       Try -R3 instead of -R3b, or use "
			    "another translation.")
			<< std::endl;
	      exit(2);
	    }
	  else
	    {
	      tm.start("reducing A_f w/ symbolic SCC pruning");
	      if (bc)
		bc->delete_unaccepting_scc();
	      tm.stop("reducing A_f w/ symbolic SCC pruning");
	    }
	}

873
874
875
876
877
878
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.
      spot::tgba* aut_scc = 0;
      if (reduc_aut & spot::Reduce_Scc)
	{
	  tm.start("reducing A_f w/ SCC");
879
	  a = aut_scc = spot::scc_filter(a, scc_filter_all);
880
881
882
	  tm.stop("reducing A_f w/ SCC");
	}

883
      spot::tgba_tba_proxy* degeneralized = 0;
884
      spot::tgba_sgba_proxy* state_labeled = 0;
885

886
887
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
888
	  && degeneralize_opt == NoDegen
889
890
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
891
892
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
893
	a = degeneralized = new spot::tgba_tba_proxy(a);
894
895
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
896
897
898
899
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
900

Felix Abecassis's avatar
Felix Abecassis committed
901
902
903
904
      spot::tgba_explicit* minimized = 0;
      if (opt_minimize)
        a = minimized = minimize(a);

905
906
907
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
908
	  if (reduc_aut & ~spot::Reduce_Scc)
909
	    {
910
	      tm.start("reducing A_f w/ sim.");
911
	      a = aut_red = new spot::tgba_reduc(a);
martinez's avatar
martinez committed
912
913

	      if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
914
915
916
			       spot::Reduce_transition_Dir_Sim |
			       spot::Reduce_quotient_Del_Sim |
			       spot::Reduce_transition_Del_Sim))
917
		{
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
		  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))
		    {
		      rel_dir =
			spot::get_direct_relation_simulation
			  (a, std::cout, display_parity_game);
		      assert(rel_dir);
		    }
		  if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
					spot::Reduce_transition_Del_Sim))
		    {
		      rel_del =
			spot::get_delayed_relation_simulation
			  (a, std::cout, display_parity_game);
		      assert(rel_del);
		    }

		  if (display_rel_sim)
		    {
		      if (rel_dir)
			aut_red->display_rel_sim(rel_dir, std::cout);
		      if (rel_del)
			aut_red->display_rel_sim(rel_del, std::cout);
		    }

		  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);
954

martinez's avatar
martinez committed
955
		  if (rel_dir)
956
		    spot::free_relation_simulation(rel_dir);
martinez's avatar
martinez committed
957
		  if (rel_del)
958
		    spot::free_relation_simulation(rel_del);
martinez's avatar
martinez committed
959
		}
960
	      tm.stop("reducing A_f w/ sim.");
961
962
963
	    }
	}

964
965
966
967
968
969
970
971
972
973
974
975
976
      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;
	}

977
978
      spot::tgba* product_degeneralized = 0;

979
      if (system)
980
981
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
982
983
984
985
986
987

	  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)
988
989
990
991
992
993
994
995
            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);
        }
996

997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
      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);
	    }
	}

1015
1016
1017
1018
1019
      if (show_fc)
	{
	  a = new spot::future_conditions_collector(a, true);
	}

1020
      if (output != -1)
1021
	{
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
	  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 =
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
		  dynamic_cast<const spot::tgba_sba_proxy*>(a);
		if (s)
		  spot::never_claim_reachable(std::cout, s, f, spin_comments);
		else
		  {
		    // It is possible that we have applied other
		    // operations to the automaton since its initial
		    // degeneralization.  Let's degeneralize again!
		    s = new spot::tgba_sba_proxy(a);
		    spot::never_claim_reachable(std::cout, s, f, spin_comments);
		    delete s;
		  }
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
		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;
1087
1088
1089
	    case 12:
	      stats_reachable(a).dump(std::cout);
	      break;
1090
1091
1092
1093
	    default:
	      assert(!"unknown output option");
	    }
	  tm.stop("producing output");
1094
	}
1095

1096
      if (echeck_inst)
1097
	{
1098
1099
1100
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
1101
1102
	  do
	    {
1103
	      tm.start("running emptiness check");
1104
	      spot::emptiness_check_result* res = ec->check();
1105
1106
	      tm.stop("running emptiness check");