ltl2tgba.cc 52.4 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
3
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013 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
//
// 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
12
// the Free Software Foundation; either version 3 of the License, or
13
14
15
16
17
18
19
20
// (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
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22

23
#include <iostream>
24
#include <iomanip>
25
#include <cassert>
26
27
#include <fstream>
#include <string>
28
#include <cstdlib>
29
#include "ltlvisit/tostring.hh"
30
#include "ltlvisit/apcollect.hh"
31
#include "ltlast/allnodes.hh"
32
#include "ltlparse/public.hh"
33
#include "tgbaalgos/ltl2tgba_lacim.hh"
34
#include "tgbaalgos/ltl2tgba_fm.hh"
35
#include "tgbaalgos/ltl2taa.hh"
36
#include "tgba/bddprint.hh"
37
#include "tgbaalgos/save.hh"
38
#include "tgbaalgos/dotty.hh"
39
#include "tgbaalgos/lbtt.hh"
40
#include "tgba/tgbatba.hh"
41
#include "tgba/tgbasgba.hh"
42
#include "tgbaalgos/degen.hh"
43
#include "tgba/tgbaproduct.hh"
44
#include "tgba/futurecondcol.hh"
45
#include "tgbaalgos/reducerun.hh"
46
#include "tgbaparse/public.hh"
47
#include "neverparse/public.hh"
48
#include "dstarparse/public.hh"
49
#include "tgbaalgos/dupexp.hh"
Felix Abecassis's avatar
Felix Abecassis committed
50
#include "tgbaalgos/minimize.hh"
51
#include "taalgos/minimize.hh"
52
#include "tgbaalgos/neverclaim.hh"
53
#include "tgbaalgos/replayrun.hh"
54
#include "tgbaalgos/rundotdec.hh"
55
#include "tgbaalgos/sccfilter.hh"
56
#include "tgbaalgos/safety.hh"
57
#include "tgbaalgos/eltl2tgba_lacim.hh"
58
#include "tgbaalgos/gtec/gtec.hh"
59
#include "eltlparse/public.hh"
60
#include "misc/timer.hh"
Thomas Badie's avatar
Thomas Badie committed
61
#include "misc/unique_ptr.hh"
62
#include "tgbaalgos/stats.hh"
63
#include "tgbaalgos/scc.hh"
64
#include "tgbaalgos/emptiness_stats.hh"
65
#include "tgbaalgos/scc.hh"
66
#include "tgbaalgos/isdet.hh"
67
#include "tgbaalgos/cycles.hh"
68
#include "tgbaalgos/isweakscc.hh"
69
#include "kripkeparse/public.hh"
Thomas Badie's avatar
Thomas Badie committed
70
#include "tgbaalgos/simulation.hh"
71
#include "tgbaalgos/compsusp.hh"
72

73
#include "taalgos/tgba2ta.hh"
74
#include "taalgos/dotty.hh"
75
#include "taalgos/stats.hh"
76

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

95
96
97
void
syntax(char* prog)
{
98
99
100
101
102
  // 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;

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

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

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
120
	    << std::endl
121
	    << "  -X    do not compute an automaton, read it from a file"
122
	    << std::endl
123
124
125
126
	    << "  -XD   do not compute an automaton, read it from an"
	    << " ltl2dstar file" << std::endl
	    << "  -XDB  read the from an ltl2dstar file and convert it to "
	    << "TGBA" << std::endl
127
128
	    << "  -XL   do not compute an automaton, read it from an"
	    << " LBTT file" << std::endl
129
130
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
131
132
133
134
	    << "  -Pfile  multiply the formula automaton with the TGBA read"
	    << " from `file'\n"
	    << "  -KPfile multiply the formula automaton with the Kripke"
	    << " structure from `file'\n"
135
136
137
	    << std::endl

	    << "Translation algorithm:" << std::endl
138
            << "  -f    use Couvreur's FM algorithm for LTL"
139
	    << " (default)" << std::endl
140
            << "  -l    use Couvreur's LaCIM algorithm for LTL "
141
	    << std::endl
142
143
144
	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
	    << std::endl
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
145
	    << std::endl
146
147
	    << "  -u    use Compositional translation"
	    << std::endl
148
149
150
	    << std::endl

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
151
152
	    << "  -fr   reduce formula at each step of FM" << std::endl
	    << "          as specified with the -r{1..7} options" << std::endl
153
154
155
156
157
            << "  -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)"
158
	    << std::endl
159
160
161
162
            << "  -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
163
	    << std::endl
164

165
166
	    << "Options for Couvreur's LaCIM algorithm (-l or -le):"
	    << std::endl
167
168
	    << "  -a    display the acceptance_conditions BDD, not the "
	    << "reachability graph"
169
	    << std::endl
170
	    << "  -A    same as -a, but as a set" << std::endl
171
172
	    << "  -lo   pre-define standard LTL operators as automata "
	    << "(implies -le)" << std::endl
173
	    << "  -r    display the relation BDD, not the reachability graph"
174
	    << std::endl
175
	    << "  -R    same as -r, but as a set" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
176
177
	    << "  -R3b  symbolically prune unaccepting SCC from BDD relation"
	    << std::endl
178
	    << std::endl
179
180

	    << "Options for Tauriainen's TAA-based algorithm (-taa):"
181
	    << std::endl
182
	    << "  -c    enable language containment checks (implies -taa)"
183
	    << std::endl
184
	    << std::endl
185
186

	    << "Formula simplification (before translation):"
187
	    << std::endl
martinez's avatar
martinez committed
188
189
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
190
	    << "universality" << std::endl
martinez's avatar
martinez committed
191
	    << "  -r3   reduce formula using implication between "
192
	    << "sub-formulae" << std::endl
193
194
195
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
196
	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
197
	    << "  -rd   display the reduced formula" << std::endl
198
	    << "  -rD   dump statistics about the simplifier cache" << std::endl
199
	    << "  -rL   disable basic rewritings producing larger formulas"
200
201
	    << std::endl
	    << "  -ru   lift formulae that are eventual and universal"
202
	    << std::endl << std::endl
203
204
205
206
207
208
209

	    << "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
210
211
212
213
	    << "          (append z/Z, o/O, l/L: to turn on/off options "
            << "(default: zol)\n "
	    << "          z: level resetting, o: adaptive order, "
	    << "l: level cache)\n"
214
215
216
217
	    << std::endl

	    << "Automaton simplifications (after translation):"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
218
	    << "  -R3   use SCC to reduce the automaton" << std::endl
219
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
220
221
222
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
223
	    << "  -RDS  reduce the automaton with direct simulation"
224
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
225
	    << "  -RRS  reduce the automaton with reverse simulation"
Thomas Badie's avatar
Thomas Badie committed
226
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
227
	    << "  -RIS  iterate both direct and reverse simulations"
228
	    << std::endl
Thomas Badie's avatar
Thomas Badie committed
229
230
            << "  -RDCS reduce the automaton with direct simulation"
            << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
231
            << "  -Rm   attempt to WDBA-minimize the automaton" << std::endl
232
	    << std::endl
233
234
235
            << "  -RM   attempt to WDBA-minimize the automaton unless the "
	    << "result is bigger" << std::endl
	    << std::endl
236

237
            << "Automaton conversion:" << std::endl
238
239
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
240
	    << "  -s    convert to explicit automaton, and number states "
241
	    << "in DFS order" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
242
	    << "  -S    convert to explicit automaton, and number states "
243
	    << "in BFS order" << std::endl
244
245
	    << std::endl

246
247
248
249
250
251
252
253
254
255
256
257
258
259
	    << "Conversion to Testing Automaton:" << std::endl
 	    << "  -TA   output a Generalized Testing Automaton (GTA),\n"
	    << "          or a Testing Automaton (TA) with -DS\n"
 	    << "  -lv   add an artificial livelock state to obtain a "
	    << "Single-pass (G)TA\n"
            << "  -sp   convert into a single-pass (G)TA without artificial "
	    << "livelock state\n"
	    << "  -in   do not use an artificial initial state\n"
            << "  -TGTA output a Transition-based Generalized TA"
            << std::endl
	    << "  -RT   reduce the (G)TA/TGTA using bisimulation.\n"
            << std::endl

	    << "Options for performing emptiness checks (on TGBA):" << std::endl
260
261
262
	    << "  -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
263
	    << std::endl
264
265
266
267
	    << "  -C    compute an accepting run (Counterexample) if it exists"
	    << std::endl
	    << "  -CR   compute and replay an accepting run (implies -C)"
	    << std::endl
268
	    << "  -g    graph the accepting run on the automaton (requires -e)"
269
	    << std::endl
270
271
272
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
	    << "  -m    try to reduce accepting runs, in a second pass"
273
274
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
275
276
277
278
279
	    << "  Cou99(OPTIONS) (the default)" << std::endl
	    << "  CVWY90(OPTIONS)" << std::endl
	    << "  GV04(OPTIONS)" << std::endl
	    << "  SE05(OPTIONS)" << std::endl
	    << "  Tau03(OPTIONS)" << std::endl
280
281
282
283
284
285
286
287
288
289
290
291
292
	    << "  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
293
294
295
	    << "  -k    display statistics on the automaton (size and SCCs)"
	    << std::endl
	    << "  -ks   display statistics on the automaton (size only)"
296
	    << std::endl
297
298
299
	    << "  -kt   display statistics on the automaton (size + "
	    << "subtransitions)"
	    << std::endl
300
301
302
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
	    << std::endl
303
	    << "  -KC   list cycles in automaton" << std::endl
304
	    << "  -KW   list weak SCCs" << std::endl
305
	    << "  -N    output the never clain for Spin (implies -DS)"
306
307
	    << std::endl
	    << "  -NN   output the never clain for Spin, with commented states"
308
	    << " (implies -DS)" << std::endl
309
310
	    << "  -O    tell if a formula represents a safety, guarantee, "
	    << "or obligation property"
311
	    << std::endl
312
313
314
315
316
317
	    << "  -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
318
	    << "  -8    output UTF-8 formulae" << std::endl
319
320
321
322
	    << "  -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"
323
	    << std::endl
324
	    << std::endl;
325

326
327
328
  exit(2);
}

Thomas Badie's avatar
Thomas Badie committed
329
330
331
332
333
334
335
336
337
338
339
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
    return -1;
  return res;
}


340
341
342
343
344
int
main(int argc, char** argv)
{
  int exit_code = 0;

345
  bool debug_opt = false;
346
  bool paper_opt = false;
347
  bool utf8_opt = false;
348
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
349
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
350
351
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA,
	 TransCompo }
352
    translation = TransFM;
353
  bool fm_red = false;
354
  bool fm_exprop_opt = false;
355
  bool fm_symb_merge_opt = true;
356
  bool file_opt = false;
357
  bool degen_reset = true;
358
  bool degen_order = false;
359
  bool degen_cache = true;
360
  int output = 0;
361
  int formula_index = 0;
362
363
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
364
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
365
  bool expect_counter_example = false;
366
367
  bool accepting_run = false;
  bool accepting_run_replay = false;
368
  bool from_file = false;
369
370
  enum { ReadSpot, ReadLbtt, ReadNeverclaim, ReadDstar } readformat = ReadSpot;
  bool nra2nba = false;
371
  bool scc_filter = false;
372
  bool simpltl = false;
373
374
  spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
					   false, false, false);
375
  bool simpcache_stats = false;
376
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
377
  bool symbolic_scc_pruning = false;
378
  bool display_reduced_form = false;
379
  bool post_branching = false;
380
  bool fair_loop_approx = false;
381
  bool graph_run_opt = false;
382
  bool graph_run_tgba_opt = false;
383
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
384
  bool opt_minimize = false;
385
  bool reject_bigger = false;
386
  bool opt_bisim_ta = false;
387
  bool opt_monitor = false;
388
  bool containment = false;
389
  bool show_fc = false;
390
  bool spin_comments = false;
391
392
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
393
  spot::tgba* system = 0;
394
  const spot::tgba* product_to_free = 0;
395
  spot::bdd_dict* dict = new spot::bdd_dict();
396
397
  spot::timer_map tm;
  bool use_timer = false;
Thomas Badie's avatar
Thomas Badie committed
398
  bool reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
399
  bool reduction_rev_sim = false;
400
  bool reduction_iterated_sim = false;
Thomas Badie's avatar
Thomas Badie committed
401
402
403
  bool reduction_dont_care_sim = false;
  int limit_dont_care_sim = 0;
  bool reduction_iterated_dont_care_sim = false;
Thomas Badie's avatar
Thomas Badie committed
404
  spot::tgba* temp_dir_sim = 0;
405
  bool ta_opt = false;
406
  bool tgta_opt = false;
407
  bool opt_with_artificial_initial_state = true;
408
409
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
Thomas Badie's avatar
Thomas Badie committed
410
  spot::tgba* temp_rev_sim = 0;
411
  spot::tgba* temp_iterated_sim = 0;
Thomas Badie's avatar
Thomas Badie committed
412
413
  spot::tgba* temp_dont_care_sim = 0;
  spot::tgba* temp_dont_care_iterated_sim = 0;
414
415
416
417
418
  bool cs_nowdba = true;
  bool cs_wdba_smaller = false;
  bool cs_nosimul = true;
  bool cs_early_start = false;
  bool cs_oblig = false;
419

420
  for (;;)
421
    {
422
      if (argc < formula_index + 2)
423
	syntax(argv[0]);
424
425
426

      ++formula_index;

427
428
429
430
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
431
432
433
434
435
      else if (!strcmp(argv[formula_index], "-8"))
	{
	  utf8_opt = true;
	  spot::enable_utf8();
	}
436
      else if (!strcmp(argv[formula_index], "-a"))
437
438
439
	{
	  output = 2;
	}
440
      else if (!strcmp(argv[formula_index], "-A"))
441
	{
442
	  output = 4;
443
	}
444
      else if (!strcmp(argv[formula_index], "-b"))
445
	{
446
	  output = 7;
447
	}
448
449
450
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
451
	  translation = TransTAA;
452
	}
453
454
455
456
457
458
459
460
461
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
462
      else if (!strcmp(argv[formula_index], "-d"))
463
464
465
	{
	  debug_opt = true;
	}
466
467
      else if (!strcmp(argv[formula_index], "-D"))
	{
468
469
	  degeneralize_opt = DegenTBA;
	}
470
      else if (!strncmp(argv[formula_index], "-DS", 3))
471
472
	{
	  degeneralize_opt = DegenSBA;
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
	  const char* p = argv[formula_index] + 3;
	  while (*p)
	    {
	      switch (*p++)
		{
		case 'o':
		  degen_order = true;
		  break;
		case 'O':
		  degen_order = false;
		  break;
		case 'z':
		  degen_reset = true;
		  break;
		case 'Z':
		  degen_reset = false;
		  break;
		case 'l':
		  degen_cache = true;
		  break;
		case 'L':
		  degen_cache = false;
		  break;
		}
	    }
498
	}
499
      else if (!strncmp(argv[formula_index], "-e", 2))
500
        {
501
502
503
504
505
506
507
508
509
510
511
512
513
	  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);
	    }
514
515
516
          expect_counter_example = true;
          output = -1;
        }
517
      else if (!strncmp(argv[formula_index], "-E", 2))
518
        {
519
520
521
522
523
524
525
526
527
528
529
530
531
	  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);
	    }
532
533
534
          expect_counter_example = false;
          output = -1;
        }
535
536
      else if (!strcmp(argv[formula_index], "-f"))
	{
537
	  translation = TransFM;
538
	}
539
      else if (!strcmp(argv[formula_index], "-fr"))
540
	{
541
	  fm_red = true;
542
	  translation = TransFM;
543
	}
544
545
546
547
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
548
549
550
551
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
552
553
      else if (!strcmp(argv[formula_index], "-g"))
	{
554
	  accepting_run = true;
555
556
	  graph_run_opt = true;
	}
557
558
      else if (!strcmp(argv[formula_index], "-G"))
	{
559
	  accepting_run = true;
560
561
	  graph_run_tgba_opt = true;
	}
562
563
564
565
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
566
567
568
569
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
570
571
572
573
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
574
575
576
577
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
578
579
580
581
582
583
584
585
586
587
588
589
      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");
	}
590
591
592
593
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
594
595
596
597
      else if (!strcmp(argv[formula_index], "-KC"))
	{
	  output = 15;
	}
598
599
600
601
      else if (!strcmp(argv[formula_index], "-KW"))
	{
	  output = 16;
	}
602
603
604
605
      else if (!strcmp(argv[formula_index], "-l"))
	{
	  translation = TransLaCIM;
	}
606
607
608
609
610
611
612
613
614
615
      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;
	}
616
617
618
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
619
	  translation = TransFM;
620
	}
621
622
623
624
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
625
626
      else if (!strcmp(argv[formula_index], "-m"))
	{
627
	  opt_reduce = true;
628
	}
martinez's avatar
martinez committed
629
630
      else if (!strcmp(argv[formula_index], "-N"))
	{
631
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
632
633
	  output = 8;
	}
634
635
636
637
638
639
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
	  spin_comments = true;
	}
640
641
      else if (!strcmp(argv[formula_index], "-O"))
	{
642
	  output = 14;
643
          opt_minimize = true;
644
	}
645
646
647
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
648
	  translation = TransFM;
649
	}
650
651
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
652
653
	  tm.start("reading -P's argument");

654
	  spot::tgba_parse_error_list pel;
655
656
657
	  spot::tgba_explicit_string* s;
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, env, debug_opt);
658
659
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
660
	    return 2;
661
	  s->merge_transitions();
662
	  tm.stop("reading -P's argument");
663
	  system = s;
664
	}
665
666
      else if (!strcmp(argv[formula_index], "-r"))
	{
667
668
	  output = 1;
	}
669
670
      else if (!strcmp(argv[formula_index], "-r1"))
	{
671
672
	  simpltl = true;
	  redopt.reduce_basics = true;
673
674
675
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
676
677
	  simpltl = true;
	  redopt.event_univ = true;
678
679
680
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
681
682
	  simpltl = true;
	  redopt.synt_impl = true;
683
684
685
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
686
687
688
689
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
690
	}
691
692
      else if (!strcmp(argv[formula_index], "-r5"))
	{
693
694
	  simpltl = true;
	  redopt.containment_checks = true;
695
696
697
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
698
699
700
	  simpltl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
701
702
703
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
704
705
706
707
708
709
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
710
	}
711
712
713
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
714
	}
715
716
717
718
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
719
	{
720
	  // For backward compatibility, make all these options
721
	  // equal to -RDS.
722
	  reduction_dir_sim = true;
723
	}
Thomas Badie's avatar
Thomas Badie committed
724
725
726
727
      else if (!strcmp(argv[formula_index], "-RRS"))
        {
          reduction_rev_sim = true;
        }
728
729
      else if (!strcmp(argv[formula_index], "-R3"))
	{
730
	  scc_filter = true;
731
	}
732
733
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
734
	  scc_filter = true;
735
736
	  scc_filter_all = true;
	}
737
738
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
739
	  symbolic_scc_pruning = true;
740
	}
741
742
      else if (!strcmp(argv[formula_index], "-rd"))
	{
743
	  display_reduced_form = true;
744
	}
745
746
747
748
      else if (!strcmp(argv[formula_index], "-rD"))
	{
	  simpcache_stats = true;
	}
749
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
750
        {
751
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
752
        }
753
754
755
756
      else if (!strcmp(argv[formula_index], "-RIS"))
        {
          reduction_iterated_sim = true;
        }
Thomas Badie's avatar
Thomas Badie committed
757
758
759
760
761
762
763
764
765
766
767
768
      else if (!strncmp(argv[formula_index], "-RDCS", 5))
        {
          reduction_dont_care_sim = true;
          if (argv[formula_index][5] == '=')
            limit_dont_care_sim = to_int(argv[formula_index] + 6);
        }
      else if (!strncmp(argv[formula_index], "-RDCIS", 6))
        {
          reduction_iterated_dont_care_sim = true;
          if (argv[formula_index][6] == '=')
            limit_dont_care_sim = to_int(argv[formula_index] + 7);
        }
769
      else if (!strcmp(argv[formula_index], "-rL"))
770
771
772
773
774
        {
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.reduce_size_strictly = true;
        }
775
776
777
778
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
779
780
781
782
783
      else if (!strcmp(argv[formula_index], "-RM"))
        {
          opt_minimize = true;
	  reject_bigger = true;
        }
784
785
786
      else if (!strcmp(argv[formula_index], "-RT"))
        {
          opt_bisim_ta = true;
787
788
789
790
791
792
	}
      else if (!strcmp(argv[formula_index], "-ru"))
        {
	  simpltl = true;
	  redopt.event_univ = true;
	  redopt.favor_event_univ = true;
793
        }
794
795
796
797
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
798
799
800
801
802
803
804
805
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
806
807
808
809
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
810
811
812
813
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
814
815
816
817
      else if (!strcmp(argv[formula_index], "-TA"))
        {
          ta_opt = true;
        }
818
      else if (!strcmp(argv[formula_index], "-TGTA"))
819
        {
820
          tgta_opt = true;
821
        }
822
823
824
825
      else if (!strcmp(argv[formula_index], "-lv"))
        {
          opt_with_artificial_livelock = true;
        }
826
827
828
829
      else if (!strcmp(argv[formula_index], "-sp"))
        {
          opt_single_pass_emptiness_check = true;
        }
830
831
832
833
      else if (!strcmp(argv[formula_index], "-in"))
        {
          opt_with_artificial_initial_state = false;
        }
834
835
836
837
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
838
839
840
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
841
	  translation = TransFM;
842
	  // Parse -U's argument.
843
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
844
845
846
	  while (tok)
	    {
	      unobservables->insert
847
		(static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
848
	      tok = strtok(0, ", \t;");
849
850
	    }
	}
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
      else if (!strncmp(argv[formula_index], "-u", 2))
	{
	  translation = TransCompo;
	  const char* c = argv[formula_index] + 2;
	  while (*c != 0)
	    {
	      switch (*c)
		{
		case '2':
		  cs_nowdba = false;
		  cs_wdba_smaller = true;
		  break;
		case 'w':
		  cs_nowdba = false;
		  cs_wdba_smaller = false;
		  break;
		case 's':
		  cs_nosimul = false;
		  break;
		case 'e':
		  cs_early_start = true;
		  break;
		case 'W':
		  cs_nowdba = true;
		  break;
		case 'S':
		  cs_nosimul = true;
		  break;
		case 'E':
		  cs_early_start = false;
		  break;
		case 'o':
		  cs_oblig = true;
		  break;
		case 'O':
		  cs_oblig = false;
		  break;
		default:
		  std::cerr << "Unknown suboption `" << *c
			    << "' for option -u" << std::endl;
		}
	      ++c;
	    }
	}
895
896
897
898
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
899
900
      else if (!strcmp(argv[formula_index], "-x"))
	{
901
	  translation = TransFM;
902
903
	  fm_exprop_opt = true;
	}
904
905
906
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
907
	  readformat = ReadSpot;
908
	}
909
      else if (!strcmp(argv[formula_index], "-XD"))
910
911
	{
	  from_file = true;
912
913
914
915
916
917
918
	  readformat = ReadDstar;
	}
      else if (!strcmp(argv[formula_index], "-XDB"))
	{
	  from_file = true;
	  readformat = ReadDstar;
	  nra2nba = true;
919
	}
920
921
922
      else if (!strcmp(argv[formula_index], "-XL"))
	{
	  from_file = true;
923
924
925
926
927
928
	  readformat = ReadLbtt;
	}
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  readformat = ReadNeverclaim;
929
	}
930
931
      else if (!strcmp(argv[formula_index], "-y"))
	{
932
	  translation = TransFM;
933
934
	  fm_symb_merge_opt = false;
	}
935
936
937
938
      else
	{
	  break;
	}
939
940
    }

941
  if ((graph_run_opt || graph_run_tgba_opt)
942
      && (!echeck_inst || !expect_counter_example))
943
    {
944
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
945
946
947
      exit(1);
    }

948
949
950
951
  std::string input;

  if (file_opt)
    {
952
      tm.start("reading formula");
953
      if (strcmp(argv[formula_index], "-"))
954
	{
955
	  std::ifstream fin(argv[formula_index]);
956
	  if (!fin)
957
958
959
960
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
961

962
	  if (!std::getline(fin, input, '\0'))
963
964
965
966
967
968
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
969
	{
970
	  std::getline(std::cin, input, '\0');
971
	}
972
      tm.stop("reading formula");
973
974
975
976
977
978
    }
  else
    {
      input = argv[formula_index];
    }

979
  const spot::ltl::formula* f = 0;
980
  if (!from_file) // Reading a formula, not reading an automaton from a file.
981
    {
982
983
984
985
986
      switch (translation)
	{
	case TransFM:
	case TransLaCIM:
	case TransTAA:
987
	case TransCompo:
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
	  {
	    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;