ltl2tgba.cc 38 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
5
6
// Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
//
// 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.

25
#include <iostream>
26
#include <iomanip>
27
#include <cassert>
28
29
#include <fstream>
#include <string>
30
#include <cstdlib>
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/replayrun.hh"
53
#include "tgbaalgos/rundotdec.hh"
54
#include "tgbaalgos/sccfilter.hh"
55
#include "tgbaalgos/safety.hh"
56
#include "tgbaalgos/eltl2tgba_lacim.hh"
57
#include "tgbaalgos/gtec/gtec.hh"
58
#include "eltlparse/public.hh"
59
#include "misc/timer.hh"
60
#include "tgbaalgos/stats.hh"
61
#include "tgbaalgos/scc.hh"
62
#include "tgbaalgos/emptiness_stats.hh"
63
64
#include "tgbaalgos/scc.hh"
#include "kripkeparse/public.hh"
Thomas Badie's avatar
Thomas Badie committed
65
#include "tgbaalgos/simulation.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)" << std::endl
124
            << "  -l    use Couvreur's LaCIM algorithm for LTL "
125
	    << std::endl
126
127
128
	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
	    << std::endl
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
129
	    << std::endl
130
131
132
	    << std::endl

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
133
134
	    << "  -fr   reduce formula at each step of FM" << std::endl
	    << "          as specified with the -r{1..7} options" << std::endl
135
136
137
138
139
            << "  -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)"
140
	    << std::endl
141
142
143
144
            << "  -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
145
	    << std::endl
146

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

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

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

	    << "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
193
	    << "  -R3   use SCC to reduce the automata" << std::endl
194
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
195
196
197
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
198
199
200
	    << "  -RDS  minimize the automaton with direct simulation"
	    << std::endl
            << "  -Rm   attempt to WDBA-minimize the automata" << std::endl
201
	    << std::endl
202

203
            << "Automaton conversion:" << std::endl
204
205
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
206
207
208
209
	    << "  -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
210
211
	    << std::endl

212
213
214
215
	    << "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
216
	    << std::endl
217
218
219
220
	    << "  -C    compute an accepting run (Counterexample) if it exists"
	    << std::endl
	    << "  -CR   compute and replay an accepting run (implies -C)"
	    << std::endl
221
	    << "  -g    graph the accepting run on the automaton (requires -e)"
222
	    << std::endl
223
224
225
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
	    << "  -m    try to reduce accepting runs, in a second pass"
226
227
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
228
229
230
231
232
	    << "  Cou99(OPTIONS) (the default)" << std::endl
	    << "  CVWY90(OPTIONS)" << std::endl
	    << "  GV04(OPTIONS)" << std::endl
	    << "  SE05(OPTIONS)" << std::endl
	    << "  Tau03(OPTIONS)" << std::endl
233
234
235
236
237
238
239
240
241
242
243
244
245
	    << "  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
246
247
248
	    << "  -k    display statistics on the automaton (size and SCCs)"
	    << std::endl
	    << "  -ks   display statistics on the automaton (size only)"
249
	    << std::endl
250
251
252
	    << "  -kt   display statistics on the automaton (size + "
	    << "subtransitions)"
	    << std::endl
253
254
255
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
	    << std::endl
256
	    << "  -N    output the never clain for Spin (implies -DS)"
257
258
	    << std::endl
	    << "  -NN   output the never clain for Spin, with commented states"
259
	    << " (implies -DS)" << std::endl
260
261
	    << "  -O    tell if a formula represents a safety, guarantee, "
	    << "or obligation property"
262
	    << std::endl
263
264
265
266
267
268
	    << "  -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
269
	    << "  -8    output UTF-8 formulae" << std::endl
270
271
272
273
274
	    << "  -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;
275
276
277
278
279
280
281
282
  exit(2);
}

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

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

333

334
  for (;;)
335
    {
336
      if (argc < formula_index + 2)
337
	syntax(argv[0]);
338
339
340

      ++formula_index;

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

535
	  spot::tgba_parse_error_list pel;
536
537
538
	  spot::tgba_explicit_string* s;
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, env, debug_opt);
539
540
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
541
	    return 2;
542
	  s->merge_transitions();
543
	  tm.stop("reading -P's argument");
544
	  system = s;
545
	}
546
547
      else if (!strcmp(argv[formula_index], "-r"))
	{
548
549
	  output = 1;
	}
550
551
      else if (!strcmp(argv[formula_index], "-r1"))
	{
552
553
	  simpltl = true;
	  redopt.reduce_basics = true;
554
555
556
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
557
558
	  simpltl = true;
	  redopt.event_univ = true;
559
560
561
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
562
563
	  simpltl = true;
	  redopt.synt_impl = true;
564
565
566
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
567
568
569
570
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
571
	}
572
573
      else if (!strcmp(argv[formula_index], "-r5"))
	{
574
575
	  simpltl = true;
	  redopt.containment_checks = true;
576
577
578
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
579
580
581
	  simpltl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
582
583
584
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
585
586
587
588
589
590
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
591
	}
592
593
594
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
595
	}
596
597
598
599
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
600
	{
601
	  // For backward compatibility, make all these options
602
	  // equal to -RDS.
603
	  reduction_dir_sim = true;
604
605
606
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
607
	  scc_filter = true;
608
	}
609
610
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
611
	  scc_filter = true;
612
613
	  scc_filter_all = true;
	}
614
615
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
616
	  symbolic_scc_pruning = true;
617
	}
618
619
      else if (!strcmp(argv[formula_index], "-rd"))
	{
620
	  display_reduced_form = true;
621
	}
622
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
623
        {
624
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
625
        }
626
      else if (!strcmp(argv[formula_index], "-rL"))
627
628
629
630
631
        {
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.reduce_size_strictly = true;
        }
632
633
634
635
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
636
637
638
639
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
640
641
642
643
644
645
646
647
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
648
649
650
651
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
652
653
654
655
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
656
657
658
659
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
660
661
662
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
663
	  translation = TransFM;
664
	  // Parse -U's argument.
665
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
666
667
668
	  while (tok)
	    {
	      unobservables->insert
669
		(static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
670
	      tok = strtok(0, ", \t;");
671
672
	    }
	}
673
674
675
676
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
677
678
      else if (!strcmp(argv[formula_index], "-x"))
	{
679
	  translation = TransFM;
680
681
	  fm_exprop_opt = true;
	}
682
683
684
685
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
686
687
688
689
690
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  read_neverclaim = true;
	}
691
692
      else if (!strcmp(argv[formula_index], "-y"))
	{
693
	  translation = TransFM;
694
695
	  fm_symb_merge_opt = false;
	}
696
697
698
699
      else
	{
	  break;
	}
700
701
    }

702
  if ((graph_run_opt || graph_run_tgba_opt)
703
      && (!echeck_inst || !expect_counter_example))
704
    {
705
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
706
707
708
      exit(1);
    }

709
710
711
712
  std::string input;

  if (file_opt)
    {
713
      tm.start("reading formula");
714
      if (strcmp(argv[formula_index], "-"))
715
	{
716
	  std::ifstream fin(argv[formula_index]);
717
	  if (!fin)
718
719
720
721
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
722

723
	  if (!std::getline(fin, input, '\0'))
724
725
726
727
728
729
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
730
	{
731
	  std::getline(std::cin, input, '\0');
732
	}
733
      tm.stop("reading formula");
734
735
736
737
738
739
    }
  else
    {
      input = argv[formula_index];
    }

740
  const spot::ltl::formula* f = 0;
741
  if (!from_file) // Reading a formula, not reading an automaton from a file.
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
771
772
773
774
775
776
777
778
779
780
781
782
783
      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;
784
	}
785
    }
786

787
  if (f || from_file)
788
    {
789
      spot::tgba_bdd_concrete* concrete = 0;
790
      const spot::tgba* to_free = 0;
791
      spot::tgba* a = 0;
792

793
794
      if (from_file)
	{
795
	  spot::tgba_explicit_string* e;
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
	  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
811
	    {
812
	      spot::neverclaim_parse_error_list pel;
813
	      tm.start("parsing neverclaim");
814
815
	      to_free = a = e = spot::neverclaim_parse(input, pel, dict,
						       env, debug_opt);
816
	      tm.stop("parsing neverclaim");
817
818
819
820
821
	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
822
		}
823
	    }
824
	  e->merge_transitions();
825
	}
826
      else
827
	{
828
829
	  spot::ltl::ltl_simplifier* simp = 0;
	  if (simpltl)
830
	    simp = new spot::ltl::ltl_simplifier(redopt, dict);
831
832

	  if (simp)
833
	    {
834
	      tm.start("reducing formula");
835
	      const spot::ltl::formula* t = simp->simplify(f);
836
	      f->destroy();
837
	      tm.stop("reducing formula");
838
	      f = t;
839
840
841
842
843
844
845
	      if (display_reduced_form)
		{
		  if (utf8_opt)
		    std::cout << spot::ltl::to_utf8_string(f) << std::endl;
		  else
		    std::cout << spot::ltl::to_string(f) << std::endl;
		}
846
	    }
847

848
849
850
851
852
853
854
855
856
	  if (f->is_psl_formula()
	      && !f->is_ltl_formula()
	      && translation != TransFM)
	    {
	      std::cerr << "Only the FM algorithm can translate PSL formulae;"
			<< " I'm using it for this formula." << std::endl;
	      translation = TransFM;
	    }

857
	  tm.start("translating formula");
858
859
860
861
862
863
864
865
	  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,
866
				       fm_red ? simp : 0);
867
868
869
870
871
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
872
873
874
875
876
	      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);
877
878
	      break;
	    }
879
	  tm.stop("translating formula");
880
	  to_free = a;
881
882

	  delete simp;
883
	}
884

885
      if (opt_monitor && !scc_filter)
886
	{
887
	  if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
888
889
	    symbolic_scc_pruning = true;
	  else
890
	    scc_filter = true;
891
892
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
893
894
      if (symbolic_scc_pruning)
        {
895
896
	  const spot::tgba_bdd_concrete* bc =
	    dynamic_cast<const spot::tgba_bdd_concrete*>(a);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
897
898
899
900
901
902
903
904
905
906
907
908
909
	  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)
910
911
		const_cast<spot::tgba_bdd_concrete*>(bc)
		  ->delete_unaccepting_scc();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
912
913
914
915
	      tm.stop("reducing A_f w/ symbolic SCC pruning");
	    }
	}

916
917
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.
918
      const spot::tgba* aut_scc = 0;
919
      if (scc_filter)
920
921
	{
	  tm.start("reducing A_f w/ SCC");
922
	  aut_scc = a = spot::scc_filter(a, scc_filter_all);
923
924
925
	  tm.stop("reducing A_f w/ SCC");
	}

926
      const spot::tgba* degeneralized = 0;
927

928
      spot::tgba* minimized = 0;
Felix Abecassis's avatar
Felix Abecassis committed
929
      if (opt_minimize)
930
	{
931
932
933
934
935
	  tm.start("obligation minimization");
	  minimized = minimize_obligation(a, f);
	  tm.stop("obligation minimization");

	  if (minimized == 0)
936
	    {
937
	      // if (!f)
938
939
940
941
942
943
		{
		  std::cerr << "Error: Without a formula I cannot make "
			    << "sure that the automaton built with -Rm\n"
			    << "       is correct." << std::endl;
		  exit(2);
		}
944
	    }
945
946
947
948
949
950
951
	  else if (minimized == a)
	    {
	      minimized = 0;
	    }
	  else
	    {
	      a = minimized;
Thomas Badie's avatar
Thomas Badie committed
952
953
              // When the minimization succeed, simulation is useless.
              reduction_dir_sim = false;
954
	      assume_sba = true;
955
	    }
956
	}
Felix Abecassis's avatar
Felix Abecassis committed
957

Thomas Badie's avatar
Thomas Badie committed
958
959
960
961
962
963
964
965
966
967

      if (reduction_dir_sim)
        {
          tm.start("Reduction w/ direct simulation");
          temp_dir_sim = spot::simulation(a);
          a = temp_dir_sim;
          tm.stop("Reduction w/ direct simulation");
        }


968
969
970
971
972
973
974
975
976
977
978
979
980
981
      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)
	{
	  degeneralize_opt = DegenTBA;
	  assume_sba = false;
	}

      if (!assume_sba && !opt_monitor)
	{
	  if (degeneralize_opt == DegenTBA)
	    {
982
	      degeneralized = a = new spot::tgba_tba_proxy(a);
983
984
985
	    }
	  else if (degeneralize_opt == DegenSBA)
	    {
986
	      degeneralized = a = new spot::tgba_sba_proxy(a);
987
988
989
990
	      assume_sba = true;
	    }
	  else if (labeling_opt == StateLabeled)
	    {
991
	      degeneralized = a = new spot::tgba_sgba_proxy(a);
992
993
994
	    }
	}

995
996
997
      if (opt_monitor)
	{
	  tm.start("Monitor minimization");
998
	  minimized = a = minimize_monitor(a);
999
	  tm.stop("Monitor minimization");
1000
1001
1002
	  assume_sba = false; 	// All states are accepting, so double
				// circles in the dot output are
				// pointless.
1003
1004
	}

1005
      const spot::tgba* expl = 0;
1006
1007
1008
1009
1010
      switch (dupexp)
	{
	case NoneDup:
	  break;
	case BFS:
1011
	  expl = a = tgba_dupexp_bfs(a);
1012
1013
	  break;
	case DFS:
1014
	  expl = a =