ltl2tgba.cc 43 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 "tgbaalgos/degen.hh"
45
#include "tgba/tgbaproduct.hh"
46
#include "tgba/futurecondcol.hh"
47
#include "tgbaalgos/reducerun.hh"
48
#include "tgbaparse/public.hh"
49
#include "neverparse/public.hh"
50
#include "tgbaalgos/dupexp.hh"
Felix Abecassis's avatar
Felix Abecassis committed
51
#include "tgbaalgos/minimize.hh"
52
#include "taalgos/minimize.hh"
53
#include "tgbaalgos/neverclaim.hh"
54
#include "tgbaalgos/replayrun.hh"
55
#include "tgbaalgos/rundotdec.hh"
56
#include "tgbaalgos/sccfilter.hh"
57
#include "tgbaalgos/safety.hh"
58
#include "tgbaalgos/eltl2tgba_lacim.hh"
59
#include "tgbaalgos/gtec/gtec.hh"
60
#include "eltlparse/public.hh"
61
#include "misc/timer.hh"
62
#include "tgbaalgos/stats.hh"
63
#include "tgbaalgos/scc.hh"
64
#include "tgbaalgos/emptiness_stats.hh"
65
66
#include "tgbaalgos/scc.hh"
#include "kripkeparse/public.hh"
Thomas Badie's avatar
Thomas Badie committed
67
#include "tgbaalgos/simulation.hh"
68

69
#include "taalgos/tgba2ta.hh"
70
#include "taalgos/dotty.hh"
71
#include "taalgos/stats.hh"
72

73
74
75
76
77
78
79
80
81
82
83
84
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)	   \
85
86
87
W=G($0)|U($0, $1)  \
R=!U(!$0, !$1)     \
M=F($0)&R($0, $1)";
88
89
90
  return s;
}

91
92
93
void
syntax(char* prog)
{
94
95
96
97
98
  // 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;

99
  std::cerr << "Usage: "<< prog << " [-f|-l|-le|-taa] [OPTIONS...] formula"
100
	    << std::endl
101
            << "       "<< prog << " [-f|-l|-le|-taa] -F [OPTIONS...] file"
102
	    << std::endl
103
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
104
	    << std::endl
105

106
107
            << "Translate an LTL formula into an automaton, or read the "
	    << "automaton from a file." << std::endl
108
109
110
111
	    << "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
112
	    << std::endl
113
114
115

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
116
	    << std::endl
117
	    << "  -X    do not compute an automaton, read it from a file"
118
	    << std::endl
119
120
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
121
122
123
124
	    << "  -Pfile  multiply the formula automaton with the TGBA read"
	    << " from `file'\n"
	    << "  -KPfile multiply the formula automaton with the Kripke"
	    << " structure from `file'\n"
125
126
127
	    << std::endl

	    << "Translation algorithm:" << std::endl
128
            << "  -f    use Couvreur's FM algorithm for LTL"
129
	    << " (default)" << std::endl
130
            << "  -l    use Couvreur's LaCIM algorithm for LTL "
131
	    << std::endl
132
133
134
	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
	    << std::endl
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
135
	    << std::endl
136
137
138
	    << std::endl

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
139
140
	    << "  -fr   reduce formula at each step of FM" << std::endl
	    << "          as specified with the -r{1..7} options" << 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
	    << "  -rd   display the reduced formula" << std::endl
186
	    << "  -rD   dump statistics about the simplifier cache" << std::endl
187
188
	    << "  -rL   disable basic rewritings producing larger formulas"
	    << std::endl << std::endl
189
190
191
192
193
194
195
196
197
198
199

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

210
            << "Automaton conversion:" << std::endl
211
212
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
213
214
215
216
	    << "  -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
217
218
	    << std::endl

219
220
221
222
	    << "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
223
	    << std::endl
224
225
226
227
	    << "  -C    compute an accepting run (Counterexample) if it exists"
	    << std::endl
	    << "  -CR   compute and replay an accepting run (implies -C)"
	    << std::endl
228
	    << "  -g    graph the accepting run on the automaton (requires -e)"
229
	    << std::endl
230
231
232
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
	    << "  -m    try to reduce accepting runs, in a second pass"
233
234
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
235
236
237
238
239
	    << "  Cou99(OPTIONS) (the default)" << std::endl
	    << "  CVWY90(OPTIONS)" << std::endl
	    << "  GV04(OPTIONS)" << std::endl
	    << "  SE05(OPTIONS)" << std::endl
	    << "  Tau03(OPTIONS)" << std::endl
240
241
242
243
244
245
246
247
248
249
250
251
252
	    << "  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
253
254
255
	    << "  -k    display statistics on the automaton (size and SCCs)"
	    << std::endl
	    << "  -ks   display statistics on the automaton (size only)"
256
	    << std::endl
257
258
259
	    << "  -kt   display statistics on the automaton (size + "
	    << "subtransitions)"
	    << std::endl
260
261
262
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
	    << std::endl
263
	    << "  -N    output the never clain for Spin (implies -DS)"
264
265
	    << std::endl
	    << "  -NN   output the never clain for Spin, with commented states"
266
	    << " (implies -DS)" << std::endl
267
268
	    << "  -O    tell if a formula represents a safety, guarantee, "
	    << "or obligation property"
269
	    << std::endl
270
271
272
273
274
275
	    << "  -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
276
	    << "  -8    output UTF-8 formulae" << std::endl
277
278
279
280
	    << "  -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"
281
	    << std::endl
282
	    << std::endl
283
284
  	  	<< "Options for Testing Automata:"
 	    << std::endl
285
286
 	    << "  -TA   Translate an LTL formula into a GTA (Generalized"
 	    << " Testing automata), for Testing Automata (TA) add '-DS' option"
287
 	    << std::endl
288
289
290
291
292
293
 	    << "  -lv   convert into a (G)TA with an artificial livelock state,"
 	    << " the obtained automaton is called S(G)TA "
 	    << "(Single-pass (Generalized) Testing Automata)"
 	    << std::endl
            << "  -sp   convert into a (G)TA involving a single-pass emptiness "
            << "check (without adding an artificial livelock state)"
294
            << std::endl
295
            << std::endl
296
           << "  -in   convert into a (G)TA without an artificial initial state"
297
            << std::endl
298
            << "  -TGTA Translate an LTL formula into a TGTA "
299
            << "(Transition-based Generalised Testing Automata)"
300
301
            << std::endl;

302

303
304
305
306
307
308
309
310
  exit(2);
}

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

311
  bool debug_opt = false;
312
  bool paper_opt = false;
313
  bool utf8_opt = false;
314
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
315
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
316
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
317
    translation = TransFM;
318
  bool fm_red = false;
319
  bool fm_exprop_opt = false;
320
  bool fm_symb_merge_opt = true;
321
  bool file_opt = false;
322
  int output = 0;
323
  int formula_index = 0;
324
325
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
326
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
327
  bool expect_counter_example = false;
328
329
  bool accepting_run = false;
  bool accepting_run_replay = false;
330
  bool from_file = false;
331
  bool read_neverclaim = false;
332
  bool scc_filter = false;
333
  bool simpltl = false;
334
335
  spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
					   false, false, false);
336
  bool simpcache_stats = false;
337
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
338
  bool symbolic_scc_pruning = false;
339
  bool display_reduced_form = false;
340
  bool post_branching = false;
341
  bool fair_loop_approx = false;
342
  bool graph_run_opt = false;
343
  bool graph_run_tgba_opt = false;
344
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
345
  bool opt_minimize = false;
346
  bool opt_monitor = false;
347
  bool containment = false;
348
  bool show_fc = false;
349
  bool spin_comments = false;
350
351
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
352
  spot::tgba* system = 0;
353
354
  const spot::tgba* product = 0;
  const spot::tgba* product_to_free = 0;
355
  spot::bdd_dict* dict = new spot::bdd_dict();
356
357
  spot::timer_map tm;
  bool use_timer = false;
358
  bool assume_sba = false;
Thomas Badie's avatar
Thomas Badie committed
359
360
  bool reduction_dir_sim = false;
  spot::tgba* temp_dir_sim = 0;
361
  bool ta_opt = false;
362
  bool tgta_opt = false;
363
  bool opt_with_artificial_initial_state = true;
364
365
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
366

367

368
  for (;;)
369
    {
370
      if (argc < formula_index + 2)
371
	syntax(argv[0]);
372
373
374

      ++formula_index;

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

569
	  spot::tgba_parse_error_list pel;
570
571
572
	  spot::tgba_explicit_string* s;
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, env, debug_opt);
573
574
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
575
	    return 2;
576
	  s->merge_transitions();
577
	  tm.stop("reading -P's argument");
578
	  system = s;
579
	}
580
581
      else if (!strcmp(argv[formula_index], "-r"))
	{
582
583
	  output = 1;
	}
584
585
      else if (!strcmp(argv[formula_index], "-r1"))
	{
586
587
	  simpltl = true;
	  redopt.reduce_basics = true;
588
589
590
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
591
592
	  simpltl = true;
	  redopt.event_univ = true;
593
594
595
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
596
597
	  simpltl = true;
	  redopt.synt_impl = true;
598
599
600
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
601
602
603
604
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
605
	}
606
607
      else if (!strcmp(argv[formula_index], "-r5"))
	{
608
609
	  simpltl = true;
	  redopt.containment_checks = true;
610
611
612
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
613
614
615
	  simpltl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
616
617
618
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
619
620
621
622
623
624
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
625
	}
626
627
628
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
629
	}
630
631
632
633
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
634
	{
635
	  // For backward compatibility, make all these options
636
	  // equal to -RDS.
637
	  reduction_dir_sim = true;
638
639
640
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
641
	  scc_filter = true;
642
	}
643
644
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
645
	  scc_filter = true;
646
647
	  scc_filter_all = true;
	}
648
649
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
650
	  symbolic_scc_pruning = true;
651
	}
652
653
      else if (!strcmp(argv[formula_index], "-rd"))
	{
654
	  display_reduced_form = true;
655
	}
656
657
658
659
      else if (!strcmp(argv[formula_index], "-rD"))
	{
	  simpcache_stats = true;
	}
660
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
661
        {
662
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
663
        }
664
      else if (!strcmp(argv[formula_index], "-rL"))
665
666
667
668
669
        {
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.reduce_size_strictly = true;
        }
670
671
672
673
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
674
675
676
677
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
678
679
680
681
682
683
684
685
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
686
687
688
689
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
690
691
692
693
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
694
695
696
697
      else if (!strcmp(argv[formula_index], "-TA"))
        {
          ta_opt = true;
        }
698
      else if (!strcmp(argv[formula_index], "-TGTA"))
699
        {
700
          tgta_opt = true;
701
        }
702
703
704
705
      else if (!strcmp(argv[formula_index], "-lv"))
        {
          opt_with_artificial_livelock = true;
        }
706
707
708
709
      else if (!strcmp(argv[formula_index], "-sp"))
        {
          opt_single_pass_emptiness_check = true;
        }
710
711
712
713
      else if (!strcmp(argv[formula_index], "-in"))
        {
          opt_with_artificial_initial_state = false;
        }
714
715
716
717
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
718
719
720
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
721
	  translation = TransFM;
722
	  // Parse -U's argument.
723
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
724
725
726
	  while (tok)
	    {
	      unobservables->insert
727
		(static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
728
	      tok = strtok(0, ", \t;");
729
730
	    }
	}
731
732
733
734
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
735
736
      else if (!strcmp(argv[formula_index], "-x"))
	{
737
	  translation = TransFM;
738
739
	  fm_exprop_opt = true;
	}
740
741
742
743
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
744
745
746
747
748
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  read_neverclaim = true;
	}
749
750
      else if (!strcmp(argv[formula_index], "-y"))
	{
751
	  translation = TransFM;
752
753
	  fm_symb_merge_opt = false;
	}
754
755
756
757
      else
	{
	  break;
	}
758
759
    }

760
  if ((graph_run_opt || graph_run_tgba_opt)
761
      && (!echeck_inst || !expect_counter_example))
762
    {
763
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
764
765
766
      exit(1);
    }

767
768
769
770
  std::string input;

  if (file_opt)
    {
771
      tm.start("reading formula");
772
      if (strcmp(argv[formula_index], "-"))
773
	{
774
	  std::ifstream fin(argv[formula_index]);
775
	  if (!fin)
776
777
778
779
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
780

781
	  if (!std::getline(fin, input, '\0'))
782
783
784
785
786
787
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
788
	{
789
	  std::getline(std::cin, input, '\0');
790
	}
791
      tm.stop("reading formula");
792
793
794
795
796
797
    }
  else
    {
      input = argv[formula_index];
    }

798
  const spot::ltl::formula* f = 0;
799
  if (!from_file) // Reading a formula, not reading an automaton from a file.
800
    {
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
      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;
842
	}
843
    }
844

845
  if (f || from_file)
846
    {
847
      spot::tgba_bdd_concrete* concrete = 0;
848
      const spot::tgba* to_free = 0;
849
      spot::tgba* a = 0;
850

851
852
      if (from_file)
	{
853
	  spot::tgba_explicit_string* e;
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
	  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
869
	    {
870
	      spot::neverclaim_parse_error_list pel;
871
	      tm.start("parsing neverclaim");
872
873
	      to_free = a = e = spot::neverclaim_parse(input, pel, dict,
						       env, debug_opt);
874
	      tm.stop("parsing neverclaim");
875
876
877
878
879
	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
880
		}
881
	      assume_sba = true;
882
	    }
883
	  e->merge_transitions();
884
	}
885
      else
886
	{
887
888
	  spot::ltl::ltl_simplifier* simp = 0;
	  if (simpltl)
889
	    simp = new spot::ltl::ltl_simplifier(redopt, dict);
890
891

	  if (simp)
892
	    {
893
	      tm.start("reducing formula");
894
	      const spot::ltl::formula* t = simp->simplify(f);
895
	      f->destroy();
896
	      tm.stop("reducing formula");
897
	      f = t;
898
899
900
901
902
903
904
	      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;
		}
905
906
907
	      // This helps ltl_to_tgba_fm() to order BDD variables in
	      // a more natural way.
	      simp->clear_as_bdd_cache();
908
	    }
909

910
911
912
913
914
915
916
917
918
	  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;
	    }

919
	  tm.start("translating formula");
920
921
922
923
924
925
926
927
	  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,
928
				       fm_red ? simp : 0);
929
930
931
932
933
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
934
935
936
937
938
	      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);
939
940
	      break;
	    }
941
	  tm.stop("translating formula");
942
	  to_free = a;
943

944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
	  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);
	    }
961
	  delete simp;
962
	}
963

964
      if (opt_monitor && !scc_filter)
965
	{
966
	  if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
967
968
	    symbolic_scc_pruning = true;
	  else
969
	    scc_filter = true;
970
971
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
972
973
      if (symbolic_scc_pruning)
        {
974
975
	  const spot::tgba_bdd_concrete* bc =
	    dynamic_cast<const spot::tgba_bdd_concrete*>(a);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
976
977
978
979
980
981
982
983
984
985
986
987
988
	  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)
989
990
		const_cast<spot::tgba_bdd_concrete*>(bc)
		  ->delete_unaccepting_scc();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
991
992
993
994
	      tm.stop("reducing A_f w/ symbolic SCC pruning");
	    }
	}

995
996
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.