ltl2tgba.cc 40 KB
Newer Older
1
// Copyright (C) 2007, 2008, 2009, 2010, 2011 Laboratoire de Recherche et
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
2
// 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
#include "tgbaalgos/safety.hh"
57
#include "tgbaalgos/eltl2tgba_lacim.hh"
58
#include "tgbaalgos/gtec/gtec.hh"
59
#include "eltlparse/public.hh"
60
#include "misc/timer.hh"
61
#include "tgbaalgos/stats.hh"
62
#include "tgbaalgos/scc.hh"
63
#include "tgbaalgos/emptiness_stats.hh"
64
65
#include "tgbaalgos/scc.hh"
#include "kripkeparse/public.hh"
66

67
68
69
70
71
72
73
74
75
76
77
78
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)	   \
79
80
81
W=G($0)|U($0, $1)  \
R=!U(!$0, !$1)     \
M=F($0)&R($0, $1)";
82
83
84
  return s;
}

85
86
87
void
syntax(char* prog)
{
88
89
90
91
92
  // 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;

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

100
101
            << "Translate an LTL formula into an automaton, or read the "
	    << "automaton from a file." << std::endl
102
103
104
105
	    << "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
106
	    << std::endl
107
108
109

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
110
	    << std::endl
111
	    << "  -X    do not compute an automaton, read it from a file"
112
	    << std::endl
113
114
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
115
116
117
118
	    << "  -Pfile  multiply the formula automaton with the TGBA read"
	    << " from `file'\n"
	    << "  -KPfile multiply the formula automaton with the Kripke"
	    << " structure from `file'\n"
119
120
121
	    << std::endl

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

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
134
135
136
137
	    << "  -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
138
139
140
	    << "  -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
141
142
143
144
145
            << "  -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)"
146
	    << std::endl
147
148
149
150
            << "  -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
151
	    << std::endl
152

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

	    << "Options for Tauriainen's TAA-based algorithm (-taa):"
169
	    << std::endl
170
	    << "  -c    enable language containment checks (implies -taa)"
171
	    << std::endl
172
	    << std::endl
173
174

	    << "Formula simplification (before translation):"
175
	    << std::endl
martinez's avatar
martinez committed
176
177
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
178
	    << "universality" << std::endl
martinez's avatar
martinez committed
179
	    << "  -r3   reduce formula using implication between "
180
	    << "sub-formulae" << std::endl
181
182
183
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
184
	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
185
186
187
188
189
190
191
192
193
194
195
196
197
	    << "  -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
198
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
199
	    << "(use -L for more reduction)"
200
	    << std::endl
201
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
202
	    << "(use -L for more reduction)"
203
	    << std::endl
204
205
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
206
	    << std::endl
207
	    << "  -R3   use SCC to reduce the automata" << std::endl
208
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
209
210
211
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
212
213
	    << "  -Rd   display the simulation relation" << std::endl
	    << "  -RD   display the parity game (dot format)" << std::endl
Felix Abecassis's avatar
Felix Abecassis committed
214
            << "  -Rm   attempt to minimize the automata" << std::endl
215
	    << std::endl
216

217
            << "Automaton conversion:" << std::endl
218
219
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
220
221
222
223
	    << "  -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
224
225
	    << std::endl

226
227
228
229
	    << "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
230
	    << std::endl
231
232
233
234
	    << "  -C    compute an accepting run (Counterexample) if it exists"
	    << std::endl
	    << "  -CR   compute and replay an accepting run (implies -C)"
	    << std::endl
235
	    << "  -g    graph the accepting run on the automaton (requires -e)"
236
	    << std::endl
237
238
239
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
	    << "  -m    try to reduce accepting runs, in a second pass"
240
241
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
242
243
244
245
246
	    << "  Cou99(OPTIONS) (the default)" << std::endl
	    << "  CVWY90(OPTIONS)" << std::endl
	    << "  GV04(OPTIONS)" << std::endl
	    << "  SE05(OPTIONS)" << std::endl
	    << "  Tau03(OPTIONS)" << std::endl
247
248
249
250
251
252
253
254
255
256
257
258
259
	    << "  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
260
261
262
	    << "  -k    display statistics on the automaton (size and SCCs)"
	    << std::endl
	    << "  -ks   display statistics on the automaton (size only)"
263
	    << std::endl
264
265
266
	    << "  -kt   display statistics on the automaton (size + "
	    << "subtransitions)"
	    << std::endl
267
268
269
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
	    << std::endl
270
	    << "  -N    output the never clain for Spin (implies -DS)"
271
272
	    << std::endl
	    << "  -NN   output the never clain for Spin, with commented states"
273
	    << " (implies -DS)" << std::endl
274
275
	    << "  -O    tell if a formula represents a safety, guarantee, "
	    << "or obligation property"
276
	    << std::endl
277
278
279
280
281
282
283
284
285
286
287
	    << "  -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
            << "  -T    time the different phases of the translation"
	    << std::endl
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl;
288
289
290
291
292
293
294
295
  exit(2);
}

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

296
  bool debug_opt = false;
297
  bool paper_opt = false;
298
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
299
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
300
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
301
    translation = TransFM;
302
  int fm_red = spot::ltl::Reduce_None;
303
  bool fm_exprop_opt = false;
304
  bool fm_symb_merge_opt = true;
305
  bool file_opt = false;
306
  int output = 0;
307
  int formula_index = 0;
308
309
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
310
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
311
  bool expect_counter_example = false;
312
313
  bool accepting_run = false;
  bool accepting_run_replay = false;
314
  bool from_file = false;
315
  bool read_neverclaim = false;
316
  int reduc_aut = spot::Reduce_None;
317
  int redopt = spot::ltl::Reduce_None;
318
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
319
  bool symbolic_scc_pruning = false;
320
321
  bool display_reduce_form = false;
  bool display_rel_sim = false;
322
  bool display_parity_game = false;
323
  bool post_branching = false;
324
  bool fair_loop_approx = false;
325
  bool graph_run_opt = false;
326
  bool graph_run_tgba_opt = false;
327
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
328
  bool opt_minimize = false;
329
  bool opt_monitor = false;
330
  bool containment = false;
331
  bool show_fc = false;
332
  bool spin_comments = false;
333
334
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
335
  spot::tgba* system = 0;
336
337
  const spot::tgba* product = 0;
  const spot::tgba* product_to_free = 0;
338
  spot::bdd_dict* dict = new spot::bdd_dict();
339
340
  spot::timer_map tm;
  bool use_timer = false;
341
  bool assume_sba = false;
342

343
  for (;;)
344
    {
345
      if (argc < formula_index + 2)
346
	syntax(argv[0]);
347
348
349

      ++formula_index;

350
351
352
353
354
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
355
356
357
	{
	  output = 2;
	}
358
      else if (!strcmp(argv[formula_index], "-A"))
359
	{
360
	  output = 4;
361
	}
362
      else if (!strcmp(argv[formula_index], "-b"))
363
	{
364
	  output = 7;
365
	}
366
367
368
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
369
	  translation = TransTAA;
370
	}
371
372
373
374
375
376
377
378
379
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
380
      else if (!strcmp(argv[formula_index], "-d"))
381
382
383
	{
	  debug_opt = true;
	}
384
385
      else if (!strcmp(argv[formula_index], "-D"))
	{
386
387
388
389
390
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
391
	}
392
      else if (!strncmp(argv[formula_index], "-e", 2))
393
        {
394
395
396
397
398
399
400
401
402
403
404
405
406
	  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);
	    }
407
408
409
          expect_counter_example = true;
          output = -1;
        }
410
      else if (!strncmp(argv[formula_index], "-E", 2))
411
        {
412
413
414
415
416
417
418
419
420
421
422
423
424
	  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);
	    }
425
426
427
          expect_counter_example = false;
          output = -1;
        }
428
429
      else if (!strcmp(argv[formula_index], "-f"))
	{
430
	  translation = TransFM;
431
	}
432
433
      else if (!strcmp(argv[formula_index], "-fr1"))
	{
434
	  translation = TransFM;
435
436
437
438
	  fm_red |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-fr2"))
	{
439
	  translation = TransFM;
440
441
442
443
	  fm_red |= spot::ltl::Reduce_Eventuality_And_Universality;
	}
      else if (!strcmp(argv[formula_index], "-fr3"))
	{
444
	  translation = TransFM;
445
446
447
	  fm_red |= spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr4"))
448
	{
449
	  translation = TransFM;
450
451
452
453
454
455
 	  fm_red |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr5"))
	{
456
	  translation = TransFM;
457
458
459
460
	  fm_red |= spot::ltl::Reduce_Containment_Checks;
	}
      else if (!strcmp(argv[formula_index], "-fr6"))
	{
461
	  translation = TransFM;
462
463
464
	  fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger;
	}
      else if (!strcmp(argv[formula_index], "-fr7"))
465
	{
466
	  translation = TransFM;
467
468
	  fm_red |= spot::ltl::Reduce_All;
	}
469
470
471
472
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
473
474
475
476
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
477
478
      else if (!strcmp(argv[formula_index], "-g"))
	{
479
	  accepting_run = true;
480
481
	  graph_run_opt = true;
	}
482
483
      else if (!strcmp(argv[formula_index], "-G"))
	{
484
	  accepting_run = true;
485
486
	  graph_run_tgba_opt = true;
	}
487
488
489
490
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
491
492
493
494
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
495
496
497
498
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
499
500
501
502
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
503
504
505
506
507
508
509
510
511
512
513
514
      else if (!strncmp(argv[formula_index], "-KP", 3))
	{
	  tm.start("reading -KP's argument");

	  spot::kripke_parse_error_list pel;
	  system = spot::kripke_parse(argv[formula_index] + 3,
				      pel, dict, env, debug_opt);
	  if (spot::format_kripke_parse_errors(std::cerr,
					       argv[formula_index] + 2, pel))
	    return 2;
	  tm.stop("reading -KP's argument");
	}
515
516
517
518
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
519
520
521
522
      else if (!strcmp(argv[formula_index], "-l"))
	{
	  translation = TransLaCIM;
	}
523
524
525
526
527
528
529
530
531
532
      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;
	}
533
534
535
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
536
	  translation = TransFM;
537
	}
538
539
540
541
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
542
543
      else if (!strcmp(argv[formula_index], "-m"))
	{
544
	  opt_reduce = true;
545
	}
martinez's avatar
martinez committed
546
547
      else if (!strcmp(argv[formula_index], "-N"))
	{
548
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
549
550
	  output = 8;
	}
551
552
553
554
555
556
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
	  spin_comments = true;
	}
557
558
      else if (!strcmp(argv[formula_index], "-O"))
	{
559
	  output = 14;
560
          opt_minimize = true;
561
	}
562
563
564
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
565
	  translation = TransFM;
566
	}
567
568
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
569
570
	  tm.start("reading -P's argument");

571
	  spot::tgba_parse_error_list pel;
572
573
574
	  spot::tgba_explicit_string* s;
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, env, debug_opt);
575
576
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
577
	    return 2;
578
	  s->merge_transitions();
579
	  tm.stop("reading -P's argument");
580
	  system = s;
581
	}
582
583
      else if (!strcmp(argv[formula_index], "-r"))
	{
584
585
	  output = 1;
	}
586
587
588
589
590
591
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
592
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
593
594
595
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
596
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
597
598
599
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
600
601
602
 	  redopt |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
603
	}
604
605
      else if (!strcmp(argv[formula_index], "-r5"))
	{
606
	  redopt |= spot::ltl::Reduce_Containment_Checks;
607
608
609
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
610
	  redopt |= spot::ltl::Reduce_Containment_Checks_Stronger;
611
612
613
614
615
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
616
617
618
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
619
	}
martinez's avatar
martinez committed
620
621
622
623
624
625
626
627
628
      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"))
629
	{
martinez's avatar
martinez committed
630
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
631
	}
martinez's avatar
martinez committed
632
      else if (!strcmp(argv[formula_index], "-R2t"))
633
	{
martinez's avatar
martinez committed
634
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
635
636
637
638
639
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	}
640
641
642
643
644
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	  scc_filter_all = true;
	}
645
646
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
647
	  symbolic_scc_pruning = true;
648
	}
649
650
651
652
653
654
655
656
657
658
659
660
      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
661
662
663
664
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
665
666
667
668
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
669
670
671
672
673
674
675
676
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
677
678
679
680
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
681
682
683
684
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
685
686
687
688
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
689
690
691
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
692
	  translation = TransFM;
693
	  // Parse -U's argument.
694
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
695
696
697
698
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
699
	      tok = strtok(0, ", \t;");
700
701
	    }
	}
702
703
704
705
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
706
707
      else if (!strcmp(argv[formula_index], "-x"))
	{
708
	  translation = TransFM;
709
710
	  fm_exprop_opt = true;
	}
711
712
713
714
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
715
716
717
718
719
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  read_neverclaim = true;
	}
720
721
      else if (!strcmp(argv[formula_index], "-y"))
	{
722
	  translation = TransFM;
723
724
	  fm_symb_merge_opt = false;
	}
725
726
727
728
      else
	{
	  break;
	}
729
730
    }

731
  if ((graph_run_opt || graph_run_tgba_opt)
732
      && (!echeck_inst || !expect_counter_example))
733
    {
734
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
735
736
737
      exit(1);
    }

738
739
740
741
  std::string input;

  if (file_opt)
    {
742
      tm.start("reading formula");
743
      if (strcmp(argv[formula_index], "-"))
744
	{
745
	  std::ifstream fin(argv[formula_index]);
746
	  if (!fin)
747
748
749
750
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
751

752
	  if (!std::getline(fin, input, '\0'))
753
754
755
756
757
758
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
759
	{
760
	  std::getline(std::cin, input, '\0');
761
	}
762
      tm.stop("reading formula");
763
764
765
766
767
768
    }
  else
    {
      input = argv[formula_index];
    }

769
  spot::ltl::formula* f = 0;
770
  if (!from_file) // Reading a formula, not reading an automaton from a file.
771
    {
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
      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;
813
	}
814
815
    }
  if (f || from_file)
816
    {
817
818
819
      const spot::tgba_bdd_concrete* concrete = 0;
      const spot::tgba* to_free = 0;
      const spot::tgba* a = 0;
820

821
822
      if (from_file)
	{
823
	  spot::tgba_explicit_string* e;
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
	  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
839
	    {
840
	      spot::neverclaim_parse_error_list pel;
841
	      tm.start("parsing neverclaim");
842
843
	      to_free = a = e = spot::neverclaim_parse(input, pel, dict,
						       env, debug_opt);
844
	      tm.stop("parsing neverclaim");
845
846
847
848
849
	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
850
		}
851
	    }
852
	  e->merge_transitions();
853
	}
854
      else
855
	{
856
	  if (redopt != spot::ltl::Reduce_None)
857
	    {
858
	      tm.start("reducing formula");
859
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
860
	      f->destroy();
861
	      tm.stop("reducing formula");
862
	      f = t;
863
864
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
865
	    }
866

867
	  tm.start("translating formula");
868
869
870
871
872
873
874
875
	  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,
876
				       fm_red);
877
878
879
880
881
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
882
883
884
885
886
	      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);
887
888
	      break;
	    }
889
	  tm.stop("translating formula");
890
	  to_free = a;
891
	}
892

893
894
      if (opt_monitor && ((reduc_aut & spot::Reduce_Scc) == 0))
	{
895
	  if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
896
897
898
899
900
	    symbolic_scc_pruning = true;
	  else
	    reduc_aut |= spot::Reduce_Scc;
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
901
902
      if (symbolic_scc_pruning)
        {
903
904
	  const spot::tgba_bdd_concrete* bc =
	    dynamic_cast<const spot::tgba_bdd_concrete*>(a);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
905
906
907
908
909
910
911
912
913
914
915
916
917
	  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)
918
919
		const_cast<spot::tgba_bdd_concrete*>(bc)
		  ->delete_unaccepting_scc();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
920
921
922
923
	      tm.stop("reducing A_f w/ symbolic SCC pruning");
	    }
	}

924
925
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.
926
      const spot::tgba* aut_scc = 0;
927
928
929
      if (reduc_aut & spot::Reduce_Scc)
	{
	  tm.start("reducing A_f w/ SCC");
930
	  a = aut_scc = spot::scc_filter(a, scc_filter_all);
931
932
933
	  tm.stop("reducing A_f w/ SCC");
	}

934
935
      const spot::tgba_tba_proxy* degeneralized = 0;
      const spot::tgba_sgba_proxy* state_labeled = 0;
936

937
938
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
939
	  && degeneralize_opt == NoDegen
940
941
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
942
	degeneralize_opt = DegenTBA;
943

944
      if (degeneralize_opt == DegenTBA)
945
946
947
	{
	  a = degeneralized = new spot::tgba_tba_proxy(a);
	}
948
      else if (degeneralize_opt == DegenSBA)
949
950
951
952
	{
	  a = degeneralized = new spot::tgba_sba_proxy(a);
	  assume_sba = true;
	}
953
      else if (labeling_opt == StateLabeled)
954
955
956
	{
	  a = state_labeled = new spot::tgba_sgba_proxy(a);
	}
957

958
      const spot::tgba* minimized = 0;
Felix Abecassis's avatar
Felix Abecassis committed
959
      if (opt_minimize)
960
	{
961
962
963
964
965
	  tm.start("obligation minimization");
	  minimized = minimize_obligation(a, f);
	  tm.stop("obligation minimization");

	  if (minimized == 0)
966
	    {
967
	      // if (!f)
968
969
970
971
972
973
		{
		  std::cerr << "Error: Without a formula I cannot make "
			    << "sure that the automaton built with -Rm\n"
			    << "       is correct." << std::endl;
		  exit(2);
		}
974
	    }
975
976
977
978
979
980
981
	  else if (minimized == a)
	    {
	      minimized = 0;
	    }
	  else
	    {
	      a = minimized;
982
	      assume_sba = true;
983
	    }
984
	}
Felix Abecassis's avatar
Felix Abecassis committed
985

986
987
988
      if (opt_monitor)
	{
	  tm.start("Monitor minimization");
989
	  a = minimized = minimize_monitor(a);
990
	  tm.stop("Monitor minimization");
991
992
993
	  assume_sba = false; 	// All states are accepting, so double
				// circles in the dot output are
				// pointless.
994
995
	}

996
997
998
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
999
	  if (reduc_aut & ~spot::Reduce_Scc)
1000
	    {
1001
	      tm.start("reducing A_f w/ sim.");
1002
	      a = aut_red = new spot::tgba_reduc(a);
martinez's avatar
martinez committed
1003
1004

	      if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
1005
1006
1007
			       spot::Reduce_transition_Dir_Sim |
			       spot::Reduce_quotient_Del_Sim |
			       spot::Reduce_transition_Del_Sim))
1008
		{
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035