ltl2tgba.cc 38.8 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
	    << "  -rD   dump statistics about the simplifier cache" << std::endl
181
182
	    << "  -rL   disable basic rewritings producing larger formulas"
	    << std::endl << std::endl
183
184
185
186
187
188
189
190
191
192
193

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

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

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

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

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

335

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

      ++formula_index;

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

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

708
  if ((graph_run_opt || graph_run_tgba_opt)
709
      && (!echeck_inst || !expect_counter_example))
710
    {
711
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
712
713
714
      exit(1);
    }

715
716
717
718
  std::string input;

  if (file_opt)
    {
719
      tm.start("reading formula");
720
      if (strcmp(argv[formula_index], "-"))
721
	{
722
	  std::ifstream fin(argv[formula_index]);
723
	  if (!fin)
724
725
726
727
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
728

729
	  if (!std::getline(fin, input, '\0'))
730
731
732
733
734
735
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
736
	{
737
	  std::getline(std::cin, input, '\0');
738
	}
739
      tm.stop("reading formula");
740
741
742
743
744
745
    }
  else
    {
      input = argv[formula_index];
    }

746
  const spot::ltl::formula* f = 0;
747
  if (!from_file) // Reading a formula, not reading an automaton from a file.
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
784
785
786
787
788
789
      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;
790
	}
791
    }
792

793
  if (f || from_file)
794
    {
795
      spot::tgba_bdd_concrete* concrete = 0;
796
      const spot::tgba* to_free = 0;
797
      spot::tgba* a = 0;
798

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

	  if (simp)
839
	    {
840
	      tm.start("reducing formula");
841
	      const spot::ltl::formula* t = simp->simplify(f);
842
	      f->destroy();
843
	      tm.stop("reducing formula");
844
	      f = t;
845
846
847
848
849
850
851
	      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;
		}
852
853
854
	      // This helps ltl_to_tgba_fm() to order BDD variables in
	      // a more natural way.
	      simp->clear_as_bdd_cache();
855
	    }
856

857
858
859
860
861
862
863
864
865
	  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;
	    }

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

891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
	  if (simp && simpcache_stats)
	    {
	      simp->print_stats(std::cerr);
	      bddStat s;
	      bdd_stats(&s);
	      std::cerr << "BDD produced: " << s.produced
			<< "\n    nodenum: " << s.nodenum
			<< "\n    maxnodenum: " << s.maxnodenum
			<< "\n    freenodes: " <<  s.freenodes
			<< "\n    minfreenodes: " << s.minfreenodes
			<< "\n    varnum: " <<  s.varnum
			<< "\n    cachesize: " << s.cachesize
			<< "\n    gbcnum: " << s.gbcnum
			<< std::endl;
	      bdd_fprintstat(stderr);
	      dict->dump(std::cerr);
	    }
908
	  delete simp;
909
	}
910

911
      if (opt_monitor && !scc_filter)
912
	{
913
	  if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
914
915
	    symbolic_scc_pruning = true;
	  else
916
	    scc_filter = true;
917
918
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
919
920
      if (symbolic_scc_pruning)
        {
921
922
	  const spot::tgba_bdd_concrete* bc =
	    dynamic_cast<const spot::tgba_bdd_concrete*>(a);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
923
924
925
926
927
928
929
930
931
932
933
934
935
	  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)
936
937
		const_cast<spot::tgba_bdd_concrete*>(bc)
		  ->delete_unaccepting_scc();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
938
939
940
941
	      tm.stop("reducing A_f w/ symbolic SCC pruning");
	    }
	}

942
943
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.
944
      const spot::tgba* aut_scc = 0;
945
      if (scc_filter)
946
947
	{
	  tm.start("reducing A_f w/ SCC");
948
	  aut_scc = a = spot::scc_filter(a, scc_filter_all);
949
950
951
	  tm.stop("reducing A_f w/ SCC");
	}

952
      const spot::tgba* degeneralized = 0;
953

954
      spot::tgba* minimized = 0;
Felix Abecassis's avatar
Felix Abecassis committed
955
      if (opt_minimize)
956
	{
957
958
959
960
961
	  tm.start("obligation minimization");
	  minimized = minimize_obligation(a, f);
	  tm.stop("obligation minimization");

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

Thomas Badie's avatar
Thomas Badie committed
984
985
986
987
988
989
990
991
992
993

      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");
        }


994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
      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)
	    {
1008
	      degeneralized = a = new spot::tgba_tba_proxy(a);
1009
1010
1011
	    }
	  else if (degeneralize_opt == DegenSBA)
	    {
1012
	      degeneralized = a = new spot::tgba_sba_proxy(a);
1013
1014
1015
1016
	      assume_sba = true;
	    }
	  else if (labeling_opt == StateLabeled)
	    {
1017
	      degeneralized = a = new spot::tgba_sgba_proxy(a);
1018
1019
1020
	    }
	}

1021