ltl2tgba.cc 50.6 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
3
4
5
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
6
// 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_fm.hh"
34
#include "tgbaalgos/ltl2taa.hh"
35
#include "tgba/bddprint.hh"
36
#include "tgbaalgos/save.hh"
37
#include "tgbaalgos/dotty.hh"
38
#include "tgbaalgos/lbtt.hh"
39
#include "tgbaalgos/hoa.hh"
40
#include "tgbaalgos/degen.hh"
41
#include "tgba/tgbaproduct.hh"
42
#include "tgbaalgos/reducerun.hh"
43
#include "tgbaparse/public.hh"
44
#include "dstarparse/public.hh"
45
#include "hoaparse/public.hh"
46
#include "tgbaalgos/dupexp.hh"
Felix Abecassis's avatar
Felix Abecassis committed
47
#include "tgbaalgos/minimize.hh"
48
#include "taalgos/minimize.hh"
49
#include "tgbaalgos/neverclaim.hh"
50
#include "tgbaalgos/replayrun.hh"
51
#include "tgbaalgos/rundotdec.hh"
52
#include "tgbaalgos/sccfilter.hh"
53
#include "tgbaalgos/safety.hh"
54
#include "tgbaalgos/gtec/gtec.hh"
55
#include "misc/timer.hh"
56
#include "tgbaalgos/stats.hh"
57
#include "tgbaalgos/sccinfo.hh"
58
#include "tgbaalgos/emptiness_stats.hh"
59
#include "tgbaalgos/scc.hh"
60
#include "tgbaalgos/sccinfo.hh"
61
#include "tgbaalgos/isdet.hh"
62
#include "tgbaalgos/cycles.hh"
63
#include "tgbaalgos/isweakscc.hh"
64
#include "kripkeparse/public.hh"
Thomas Badie's avatar
Thomas Badie committed
65
#include "tgbaalgos/simulation.hh"
66
#include "tgbaalgos/compsusp.hh"
67
#include "tgbaalgos/powerset.hh"
68
#include "tgbaalgos/dtgbacomp.hh"
69
70
#include "tgbaalgos/complete.hh"
#include "tgbaalgos/dtbasat.hh"
71
#include "tgbaalgos/dtgbasat.hh"
72
#include "tgbaalgos/stutter.hh"
73

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

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

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

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

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

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
121
	    << std::endl
122
	    << "  -X    do not compute an automaton, read it from a file"
123
	    << std::endl
124
125
126
127
	    << "  -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
128
129
	    << "  -XDD  read the from an ltl2dstar file and convert it to "
	    << "TGBA,\n       keeping it deterministic when possible\n"
130
131
	    << "  -XH   do not compute an automaton, read it from a"
	    << " HOA file\n"
132
133
	    << "  -XL   do not compute an automaton, read it from an"
	    << " LBTT file" << std::endl
134
135
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
136
137
138
139
	    << "  -Pfile  multiply the formula automaton with the TGBA read"
	    << " from `file'\n"
	    << "  -KPfile multiply the formula automaton with the Kripke"
	    << " structure from `file'\n"
140
141
142
	    << std::endl

	    << "Translation algorithm:" << std::endl
143
            << "  -f    use Couvreur's FM algorithm for LTL"
144
	    << " (default)" << std::endl
145
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
146
	    << std::endl
147
148
	    << "  -u    use Compositional translation"
	    << std::endl
149
150
151
	    << std::endl

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

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

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

	    << "Automaton degeneralization (after translation):"
	    << std::endl
192
	    << "  -DT   degeneralize the automaton as a TBA" << std::endl
193
	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
194
195
196
197
	    << "          (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"
198
199
200
201
	    << std::endl

	    << "Automaton simplifications (after translation):"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
202
	    << "  -R3   use SCC to reduce the automaton" << std::endl
203
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
204
205
206
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
207
	    << "  -RDS  reduce the automaton with direct simulation"
208
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
209
	    << "  -RRS  reduce the automaton with reverse simulation"
Thomas Badie's avatar
Thomas Badie committed
210
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
211
	    << "  -RIS  iterate both direct and reverse simulations"
212
	    << std::endl
Thomas Badie's avatar
Thomas Badie committed
213
214
            << "  -RDCS reduce the automaton with direct simulation"
            << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
215
            << "  -Rm   attempt to WDBA-minimize the automaton" << std::endl
216
	    << std::endl
217
218
            << "  -RM   attempt to WDBA-minimize the automaton unless the "
	    << "result is bigger" << std::endl
219
	    << "  -RQ   determinize a TGBA (assuming it's legal!)" << std::endl
220
	    << std::endl
221

222
            << "Automaton conversion:" << std::endl
223
224
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
225
	    << "  -s    convert to explicit automaton, and number states "
226
	    << "in DFS order" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
227
	    << "  -S    convert to explicit automaton, and number states "
228
	    << "in BFS order" << std::endl
229
230
	    << std::endl

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

307
308
309
  exit(2);
}

Thomas Badie's avatar
Thomas Badie committed
310
311
312
313
314
315
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
316
317
318
319
    {
      std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
      exit(1);
    }
Thomas Badie's avatar
Thomas Badie committed
320
321
322
  return res;
}

323
324
325
326
327
spot::tgba_digraph_ptr ensure_digraph(const spot::tgba_ptr& a)
{
  auto aa = std::dynamic_pointer_cast<spot::tgba_digraph>(a);
  if (aa)
    return aa;
328
  return spot::make_tgba_digraph(a, spot::tgba::prop_set::all());
329
330
}

331
int
332
checked_main(int argc, char** argv)
333
334
335
{
  int exit_code = 0;

336
  bool debug_opt = false;
337
  bool paper_opt = false;
338
  bool utf8_opt = false;
339
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
340
  enum { TransFM, TransTAA, TransCompo } translation = TransFM;
341
  bool fm_red = false;
342
  bool fm_exprop_opt = false;
343
  bool fm_symb_merge_opt = true;
344
  bool file_opt = false;
345
  bool degen_reset = true;
346
  bool degen_order = false;
347
  bool degen_cache = true;
348
  int output = 0;
349
  int formula_index = 0;
350
  const char* echeck_algo = 0;
351
  spot::emptiness_check_instantiator_ptr echeck_inst = 0;
352
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
353
  bool expect_counter_example = false;
354
355
  bool accepting_run = false;
  bool accepting_run_replay = false;
356
  bool from_file = false;
357
  enum { ReadSpot, ReadLbtt, ReadDstar, ReadHoa } readformat = ReadSpot;
358
  bool nra2nba = false;
359
  bool dra2dba = false;
360
  bool scc_filter = false;
361
  bool simpltl = false;
362
363
  spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
					   false, false, false);
364
  bool simpcache_stats = false;
365
  bool scc_filter_all = false;
366
  bool display_reduced_form = false;
367
  bool post_branching = false;
368
  bool fair_loop_approx = false;
369
  bool graph_run_opt = false;
370
  bool graph_run_tgba_opt = false;
371
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
372
  bool opt_minimize = false;
373
  bool opt_determinize = false;
374
375
  unsigned opt_determinize_threshold = 0;
  unsigned opt_o_threshold = 0;
376
  bool opt_dtgbacomp = false;
377
  bool reject_bigger = false;
378
  bool opt_monitor = false;
379
  bool containment = false;
380
381
  bool opt_closure = false;
  bool opt_stutterize = false;
382
383
  const char* opt_never = nullptr;
  const char* hoa_opt = nullptr;
384
  auto& env = spot::ltl::default_environment::instance();
385
  spot::ltl::atomic_prop_set* unobservables = 0;
386
  spot::tgba_ptr system_aut = 0;
387
  auto dict = spot::make_bdd_dict();
388
389
  spot::timer_map tm;
  bool use_timer = false;
Thomas Badie's avatar
Thomas Badie committed
390
  bool reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
391
  bool reduction_rev_sim = false;
392
  bool reduction_iterated_sim = false;
Thomas Badie's avatar
Thomas Badie committed
393
394
395
  bool reduction_dont_care_sim = false;
  int limit_dont_care_sim = 0;
  bool reduction_iterated_dont_care_sim = false;
396
  bool opt_bisim_ta = false;
397
  bool ta_opt = false;
398
  bool tgta_opt = false;
399
  bool opt_with_artificial_initial_state = true;
400
401
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
402
403
404
405
406
  bool cs_nowdba = true;
  bool cs_wdba_smaller = false;
  bool cs_nosimul = true;
  bool cs_early_start = false;
  bool cs_oblig = false;
407
408
  bool opt_complete = false;
  int opt_dtbasat = -1;
409
  int opt_dtgbasat = -1;
410

411
  for (;;)
412
    {
413
      if (argc < formula_index + 2)
414
	syntax(argv[0]);
415
416
417

      ++formula_index;

418
419
420
421
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
422
423
424
425
426
      else if (!strcmp(argv[formula_index], "-8"))
	{
	  utf8_opt = true;
	  spot::enable_utf8();
	}
427

428
      else if (!strcmp(argv[formula_index], "-b"))
429
	{
430
	  output = 7;
431
	}
432
433
434
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
435
	  translation = TransTAA;
436
	}
437
438
439
440
441
442
443
444
445
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
446
      else if (!strcmp(argv[formula_index], "-d"))
447
448
449
	{
	  debug_opt = true;
	}
450
451
      else if (!strcmp(argv[formula_index], "-D"))
	{
452
453
	  std::cerr << "-D was renamed to -DT\n";
	  abort();
454
	}
455
456
      else if (!strcmp(argv[formula_index], "-DC"))
	{
457
	  opt_dtgbacomp = true;
458
	}
459
460
      else if (!strncmp(argv[formula_index], "-DS", 3)
	       || !strncmp(argv[formula_index], "-DT", 3))
461
	{
462
463
	  degeneralize_opt =
	    argv[formula_index][2] == 'S' ? DegenSBA : DegenTBA;
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
	  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;
		}
	    }
489
	}
490
      else if (!strncmp(argv[formula_index], "-e", 2))
491
        {
492
493
494
495
496
497
	  echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
498
	    spot::make_emptiness_check_instantiator(echeck_algo, &err);
499
500
501
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
502
			<< err <<  '\'' << std::endl;
503
504
	      exit(2);
	    }
505
506
507
          expect_counter_example = true;
          output = -1;
        }
508
      else if (!strncmp(argv[formula_index], "-E", 2))
509
        {
510
511
512
513
514
515
	  const char* echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
516
	    spot::make_emptiness_check_instantiator(echeck_algo, &err);
517
518
519
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
520
			<< err <<  '\'' << std::endl;
521
522
	      exit(2);
	    }
523
524
525
          expect_counter_example = false;
          output = -1;
        }
526
527
      else if (!strcmp(argv[formula_index], "-f"))
	{
528
	  translation = TransFM;
529
	}
530
      else if (!strcmp(argv[formula_index], "-fr"))
531
	{
532
	  fm_red = true;
533
	  translation = TransFM;
534
	}
535
536
537
538
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
539
540
      else if (!strcmp(argv[formula_index], "-g"))
	{
541
	  accepting_run = true;
542
543
	  graph_run_opt = true;
	}
544
545
      else if (!strcmp(argv[formula_index], "-G"))
	{
546
	  accepting_run = true;
547
548
	  graph_run_tgba_opt = true;
	}
549
550
551
      else if (!strncmp(argv[formula_index], "-H", 2))
	{
	  output = 17;
552
	  hoa_opt = argv[formula_index] + 2;
553
	}
554
555
556
557
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
558
559
560
561
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
562
563
564
565
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
566
567
568
569
570
      else if (!strncmp(argv[formula_index], "-KP", 3))
	{
	  tm.start("reading -KP's argument");

	  spot::kripke_parse_error_list pel;
571
572
	  system_aut = spot::kripke_parse(argv[formula_index] + 3,
					  pel, dict, env, debug_opt);
573
574
575
576
577
	  if (spot::format_kripke_parse_errors(std::cerr,
					       argv[formula_index] + 2, pel))
	    return 2;
	  tm.stop("reading -KP's argument");
	}
578
579
580
581
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
582
583
584
585
      else if (!strcmp(argv[formula_index], "-KC"))
	{
	  output = 15;
	}
586
587
588
589
      else if (!strcmp(argv[formula_index], "-KW"))
	{
	  output = 16;
	}
590
591
592
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
593
	  translation = TransFM;
594
	}
595
596
      else if (!strcmp(argv[formula_index], "-m"))
	{
597
	  opt_reduce = true;
598
	}
martinez's avatar
martinez committed
599
600
      else if (!strcmp(argv[formula_index], "-N"))
	{
601
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
602
	  output = 8;
603
	  opt_never = nullptr;
martinez's avatar
martinez committed
604
	}
605
606
607
608
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
609
	  opt_never = "c";
610
	}
611
      else if (!strncmp(argv[formula_index], "-O", 2))
612
	{
613
	  output = 14;
614
          opt_minimize = true;
615
616
	  if (argv[formula_index][2] != 0)
	    opt_o_threshold = to_int(argv[formula_index] + 2);
617
	}
618
619
620
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
621
	  translation = TransFM;
622
	}
623
624
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
625
626
	  tm.start("reading -P's argument");

627
	  spot::tgba_parse_error_list pel;
628
	  spot::tgba_digraph_ptr s;
629
	  s = spot::tgba_parse(argv[formula_index] + 2,
630
			       pel, dict, env, debug_opt);
631
632
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
633
	    return 2;
634
	  s->merge_transitions();
635
	  tm.stop("reading -P's argument");
636
	  system_aut = s;
637
	}
638
639
      else if (!strcmp(argv[formula_index], "-r1"))
	{
640
641
	  simpltl = true;
	  redopt.reduce_basics = true;
642
643
644
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
645
646
	  simpltl = true;
	  redopt.event_univ = true;
647
648
649
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
650
651
	  simpltl = true;
	  redopt.synt_impl = true;
652
653
654
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
655
656
657
658
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
659
	}
660
661
      else if (!strcmp(argv[formula_index], "-r5"))
	{
662
663
	  simpltl = true;
	  redopt.containment_checks = true;
664
665
666
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
667
668
669
	  simpltl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
670
671
672
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
673
674
675
676
677
678
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
679
	}
680
681
682
683
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
684
	{
685
	  // For backward compatibility, make all these options
686
	  // equal to -RDS.
687
	  reduction_dir_sim = true;
688
	}
Thomas Badie's avatar
Thomas Badie committed
689
690
691
692
      else if (!strcmp(argv[formula_index], "-RRS"))
        {
          reduction_rev_sim = true;
        }
693
694
      else if (!strcmp(argv[formula_index], "-R3"))
	{
695
	  scc_filter = true;
696
	}
697
698
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
699
	  scc_filter = true;
700
701
	  scc_filter_all = true;
	}
702
703
      else if (!strcmp(argv[formula_index], "-rd"))
	{
704
	  display_reduced_form = true;
705
	}
706
707
708
709
      else if (!strcmp(argv[formula_index], "-rD"))
	{
	  simpcache_stats = true;
	}
710
711
712
713
      else if (!strcmp(argv[formula_index], "-RC"))
	{
	  opt_complete = true;
	}
714
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
715
        {
716
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
717
        }
718
719
720
721
      else if (!strcmp(argv[formula_index], "-RIS"))
        {
          reduction_iterated_sim = true;
        }
Thomas Badie's avatar
Thomas Badie committed
722
723
724
725
726
727
728
729
730
731
732
733
      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);
        }
734
      else if (!strcmp(argv[formula_index], "-rL"))
735
736
737
738
739
        {
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.reduce_size_strictly = true;
        }
740
741
742
743
744
745
746
747
      else if (!strncmp(argv[formula_index], "-RG", 3))
        {
	  if (argv[formula_index][3] != 0)
	    opt_dtgbasat = to_int(argv[formula_index] + 3);
	  else
	    opt_dtgbasat = 0;
          //output = -1;
        }
748
749
750
751
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
752
753
754
755
756
      else if (!strcmp(argv[formula_index], "-RM"))
        {
          opt_minimize = true;
	  reject_bigger = true;
        }
757
      else if (!strncmp(argv[formula_index], "-RQ", 3))
758
759
        {
          opt_determinize = true;
760
761
	  if (argv[formula_index][3] != 0)
	    opt_determinize_threshold = to_int(argv[formula_index] + 3);
762
        }
763
764
765
766
767
      else if (!strncmp(argv[formula_index], "-RS", 3))
        {
	  if (argv[formula_index][3] != 0)
	    opt_dtbasat = to_int(argv[formula_index] + 3);
	  else
768
	    opt_dtbasat = 0;
769
770
          //output = -1;
        }
771
772
773
      else if (!strcmp(argv[formula_index], "-RT"))
        {
          opt_bisim_ta = true;
774
775
776
777
778
779
	}
      else if (!strcmp(argv[formula_index], "-ru"))
        {
	  simpltl = true;
	  redopt.event_univ = true;
	  redopt.favor_event_univ = true;
780
        }
781
782
783
784
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
785
786
787
788
789
790
791
792
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
793
794
795
796
797
798
799
800
      else if (!strcmp(argv[formula_index], "-CL"))
	{
	  opt_closure = true;
	}
      else if (!strcmp(argv[formula_index], "-ST"))
	{
	  opt_stutterize = true;
	}
801
802
803
804
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
805
806
807
808
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
809
810
811
812
      else if (!strcmp(argv[formula_index], "-TA"))
        {
          ta_opt = true;
        }
813
      else if (!strcmp(argv[formula_index], "-TGTA"))
814
        {
815
          tgta_opt = true;
816
        }
817
818
819
820
      else if (!strcmp(argv[formula_index], "-lv"))
        {
          opt_with_artificial_livelock = true;
        }
821
822
823
824
      else if (!strcmp(argv[formula_index], "-sp"))
        {
          opt_single_pass_emptiness_check = true;
        }
825
826
827
828
      else if (!strcmp(argv[formula_index], "-in"))
        {
          opt_with_artificial_initial_state = false;
        }
829
830
831
832
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
833
834
835
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
836
	  translation = TransFM;
837
	  // Parse -U's argument.
838
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
839
840
	  while (tok)
	    {
841
	      unobservables->insert(env.require(tok));
842
	      tok = strtok(0, ", \t;");
843
844
	    }
	}
845
846
847
848
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
      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;
	    }
	}
889
890
891
892
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
893
894
      else if (!strcmp(argv[formula_index], "-x"))
	{
895
	  translation = TransFM;
896
897
	  fm_exprop_opt = true;
	}
898
899
900
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
901
	  readformat = ReadSpot;
902
	}
903
      else if (!strcmp(argv[formula_index], "-XD"))
904
905
	{
	  from_file = true;
906
907
908
909
910
911
912
	  readformat = ReadDstar;
	}
      else if (!strcmp(argv[formula_index], "-XDB"))
	{
	  from_file = true;
	  readformat = ReadDstar;
	  nra2nba = true;
913
	}
914
915
916
917
918
919
920
      else if (!strcmp(argv[formula_index], "-XDD"))
	{
	  from_file = true;
	  readformat = ReadDstar;
	  nra2nba = true;
	  dra2dba = true;
	}
921
922
923
924
925
      else if (!strcmp(argv[formula_index], "-XH"))
	{
	  from_file = true;
	  readformat = ReadHoa;
	}
926
927
928
      else if (!strcmp(argv[formula_index], "-XL"))
	{
	  from_file = true;
929
930
	  readformat = ReadLbtt;
	}
931
      else if (!strcmp(argv[formula_index], "-XN")) // now synonym for -XH
932
933
	{
	  from_file = true;
934
	  readformat = ReadHoa;
935
	}
936
937
      else if (!strcmp(argv[formula_index], "-y"))
	{
938
	  translation = TransFM;
939
940
	  fm_symb_merge_opt = false;
	}
941
942
943
944
      else
	{
	  break;
	}
945
946
    }