ikwiad.cc 44.9 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 30 31
#include "tl/print.hh"
#include "tl/apcollect.hh"
#include "tl/formula.hh"
32
#include "tl/parse.hh"
33 34
#include "twaalgos/ltl2tgba_fm.hh"
#include "twaalgos/ltl2taa.hh"
35
#include "twa/bddprint.hh"
36
#include "twaalgos/dot.hh"
37 38 39
#include "twaalgos/lbtt.hh"
#include "twaalgos/hoa.hh"
#include "twaalgos/degen.hh"
40
#include "twa/twaproduct.hh"
41
#include "twaalgos/reducerun.hh"
42
#include "parseaut/public.hh"
43
#include "twaalgos/copy.hh"
44
#include "twaalgos/minimize.hh"
45
#include "taalgos/minimize.hh"
46 47 48 49 50
#include "twaalgos/neverclaim.hh"
#include "twaalgos/replayrun.hh"
#include "twaalgos/sccfilter.hh"
#include "twaalgos/safety.hh"
#include "twaalgos/gtec/gtec.hh"
51
#include "misc/timer.hh"
52 53 54 55 56 57 58
#include "twaalgos/stats.hh"
#include "twaalgos/sccinfo.hh"
#include "twaalgos/emptiness_stats.hh"
#include "twaalgos/sccinfo.hh"
#include "twaalgos/isdet.hh"
#include "twaalgos/cycles.hh"
#include "twaalgos/isweakscc.hh"
59
#include "kripkeparse/public.hh"
60 61 62
#include "twaalgos/simulation.hh"
#include "twaalgos/compsusp.hh"
#include "twaalgos/powerset.hh"
63 64
#include "twaalgos/complement.hh"
#include "twaalgos/remfin.hh"
65 66 67 68
#include "twaalgos/complete.hh"
#include "twaalgos/dtbasat.hh"
#include "twaalgos/dtgbasat.hh"
#include "twaalgos/stutter.hh"
69
#include "twaalgos/totgba.hh"
70

71
#include "taalgos/tgba2ta.hh"
72
#include "taalgos/dot.hh"
73
#include "taalgos/stats.hh"
74

75
static void
76 77
syntax(char* prog)
{
78 79 80 81 82
  // 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;

83
  std::cerr << "Usage: "<< prog << " [-f|-l|-taa] [OPTIONS...] formula"
84
	    << std::endl
85
            << "       "<< prog << " [-f|-l|-taa] -F [OPTIONS...] file"
86
	    << std::endl
87
            << "       "<< prog << " -XH [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing  
Alexandre Duret-Lutz committed
88
	    << std::endl
89

90 91
            << "Translate an LTL formula into an automaton, or read the "
	    << "automaton from a file." << std::endl
92 93 94 95
	    << "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
96
	    << std::endl
97 98 99

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
100
	    << std::endl
101 102
	    << "  -XD   do not compute an automaton, read it from an"
	    << " ltl2dstar file" << std::endl
103
	    << "  -XDB  like -XD, and convert it to TGBA\n"
104 105
	    << "  -XH   do not compute an automaton, read it from a"
	    << " HOA file\n"
106 107
	    << "  -XL   do not compute an automaton, read it from an"
	    << " LBTT file" << std::endl
108 109
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
110 111 112 113
	    << "  -Pfile  multiply the formula automaton with the TGBA read"
	    << " from `file'\n"
	    << "  -KPfile multiply the formula automaton with the Kripke"
	    << " structure from `file'\n"
114 115 116
	    << std::endl

	    << "Translation algorithm:" << std::endl
117
            << "  -f    use Couvreur's FM algorithm for LTL"
118
	    << " (default)" << std::endl
119
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
120
	    << std::endl
121 122
	    << "  -u    use Compositional translation"
	    << std::endl
123 124 125
	    << std::endl

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
126 127
	    << "  -fr   reduce formula at each step of FM" << std::endl
	    << "          as specified with the -r{1..7} options" << std::endl
128
	    << "  -fu   build unambiguous automata" << std::endl
129 130 131 132 133
            << "  -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)"
134
	    << std::endl
135 136 137 138
            << "  -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
139
	    << std::endl
140 141

	    << "Options for Tauriainen's TAA-based algorithm (-taa):"
142
	    << std::endl
143
	    << "  -c    enable language containment checks (implies -taa)"
144
	    << std::endl
145
	    << std::endl
146 147

	    << "Formula simplification (before translation):"
148
	    << std::endl
martinez's avatar
martinez committed
149 150
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
151
	    << "universality" << std::endl
martinez's avatar
martinez committed
152
	    << "  -r3   reduce formula using implication between "
153
	    << "sub-formulae" << std::endl
154 155 156
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
157
	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
158
	    << "  -rd   display the reduced formula" << std::endl
159
	    << "  -rD   dump statistics about the simplifier cache" << std::endl
160
	    << "  -rL   disable basic rewritings producing larger formulas"
161 162
	    << std::endl
	    << "  -ru   lift formulae that are eventual and universal"
163
	    << std::endl << std::endl
164 165 166

	    << "Automaton degeneralization (after translation):"
	    << std::endl
167
	    << "  -DT   degeneralize the automaton as a TBA" << std::endl
168
	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
169 170 171 172
	    << "          (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"
173 174 175 176
	    << std::endl

	    << "Automaton simplifications (after translation):"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
177
	    << "  -R3   use SCC to reduce the automaton" << std::endl
178
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
179 180 181
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
182
	    << "  -RDS  reduce the automaton with direct simulation"
183
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
184
	    << "  -RRS  reduce the automaton with reverse simulation"
Thomas Badie's avatar
Thomas Badie committed
185
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
186
	    << "  -RIS  iterate both direct and reverse simulations"
187
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
188
            << "  -Rm   attempt to WDBA-minimize the automaton" << std::endl
189
	    << std::endl
190 191
            << "  -RM   attempt to WDBA-minimize the automaton unless the "
	    << "result is bigger" << std::endl
192
	    << "  -RQ   determinize a TGBA (assuming it's legal!)" << std::endl
193
	    << std::endl
194

195
            << "Automaton conversion:" << std::endl
196 197
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
198
	    << "  -s    convert to explicit automaton, and number states "
199
	    << "in DFS order" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
200
	    << "  -S    convert to explicit automaton, and number states "
201
	    << "in BFS order" << std::endl
202 203
	    << std::endl

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

274 275 276
  exit(2);
}

Thomas Badie's avatar
Thomas Badie committed
277 278 279 280 281 282
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
283 284 285 286
    {
      std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
      exit(1);
    }
Thomas Badie's avatar
Thomas Badie committed
287 288 289
  return res;
}

290 291
static spot::twa_graph_ptr
ensure_digraph(const spot::twa_ptr& a)
292
{
293
  auto aa = std::dynamic_pointer_cast<spot::twa_graph>(a);
294 295
  if (aa)
    return aa;
296
  return spot::make_twa_graph(a, spot::twa::prop_set::all());
297 298
}

299
static int
300
checked_main(int argc, char** argv)
301 302 303
{
  int exit_code = 0;

304
  bool debug_opt = false;
305
  bool paper_opt = false;
306
  bool utf8_opt = false;
307
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
308
  enum { TransFM, TransTAA, TransCompo } translation = TransFM;
309
  bool fm_red = false;
310
  bool fm_exprop_opt = false;
311
  bool fm_symb_merge_opt = true;
312
  bool fm_unambiguous = false;
313
  bool file_opt = false;
314
  bool degen_reset = true;
315
  bool degen_order = false;
316
  bool degen_cache = true;
317
  int output = 0;
318
  int formula_index = 0;
319 320
  const char* echeck_algo = nullptr;
  spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
321
  bool dupexp = false;
322
  bool expect_counter_example = false;
323 324
  bool accepting_run = false;
  bool accepting_run_replay = false;
325
  bool from_file = false;
326
  bool nra2nba = false;
327
  bool scc_filter = false;
328
  bool simpltl = false;
329
  spot::tl_simplifier_options redopt(false, false, false, false,
330
					   false, false, false);
331
  bool simpcache_stats = false;
332
  bool scc_filter_all = false;
333
  bool display_reduced_form = false;
334
  bool post_branching = false;
335
  bool fair_loop_approx = false;
336
  bool graph_run_tgba_opt = false;
337
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
338
  bool opt_minimize = false;
339
  bool opt_determinize = false;
340 341
  unsigned opt_determinize_threshold = 0;
  unsigned opt_o_threshold = 0;
342
  bool opt_dtwacomp = false;
343
  bool reject_bigger = false;
344
  bool opt_monitor = false;
345
  bool containment = false;
346 347
  bool opt_closure = false;
  bool opt_stutterize = false;
348 349
  const char* opt_never = nullptr;
  const char* hoa_opt = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
350 351
  auto& env = spot::default_environment::instance();
  spot::atomic_prop_set* unobservables = nullptr;
352
  spot::twa_ptr system_aut = nullptr;
353
  auto dict = spot::make_bdd_dict();
354 355
  spot::timer_map tm;
  bool use_timer = false;
Thomas Badie's avatar
Thomas Badie committed
356
  bool reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
357
  bool reduction_rev_sim = false;
358
  bool reduction_iterated_sim = false;
359
  bool opt_bisim_ta = false;
360
  bool ta_opt = false;
361
  bool tgta_opt = false;
362
  bool opt_with_artificial_initial_state = true;
363 364
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
365 366 367 368 369
  bool cs_nowdba = true;
  bool cs_wdba_smaller = false;
  bool cs_nosimul = true;
  bool cs_early_start = false;
  bool cs_oblig = false;
370 371
  bool opt_complete = false;
  int opt_dtbasat = -1;
372
  int opt_dtgbasat = -1;
373

374
  for (;;)
375
    {
376
      if (argc < formula_index + 2)
377
	syntax(argv[0]);
378 379 380

      ++formula_index;

381 382 383 384
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
385 386 387 388 389
      else if (!strcmp(argv[formula_index], "-8"))
	{
	  utf8_opt = true;
	  spot::enable_utf8();
	}
390 391 392
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
393
	  translation = TransTAA;
394
	}
395 396 397 398 399 400 401 402 403
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
404
      else if (!strcmp(argv[formula_index], "-d"))
405 406 407
	{
	  debug_opt = true;
	}
408 409
      else if (!strcmp(argv[formula_index], "-D"))
	{
410 411
	  std::cerr << "-D was renamed to -DT\n";
	  abort();
412
	}
413 414
      else if (!strcmp(argv[formula_index], "-DC"))
	{
415
	  opt_dtwacomp = true;
416
	}
417 418
      else if (!strncmp(argv[formula_index], "-DS", 3)
	       || !strncmp(argv[formula_index], "-DT", 3))
419
	{
420 421
	  degeneralize_opt =
	    argv[formula_index][2] == 'S' ? DegenSBA : DegenTBA;
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446
	  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;
		}
	    }
447
	}
448
      else if (!strncmp(argv[formula_index], "-e", 2))
449
        {
450 451 452 453 454 455
	  echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
456
	    spot::make_emptiness_check_instantiator(echeck_algo, &err);
457 458 459
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
460
			<< err <<  '\'' << std::endl;
461 462
	      exit(2);
	    }
463 464 465
          expect_counter_example = true;
          output = -1;
        }
466
      else if (!strncmp(argv[formula_index], "-E", 2))
467
        {
468 469 470 471 472 473
	  const char* echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
474
	    spot::make_emptiness_check_instantiator(echeck_algo, &err);
475 476 477
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
478
			<< err <<  '\'' << std::endl;
479 480
	      exit(2);
	    }
481 482 483
          expect_counter_example = false;
          output = -1;
        }
484 485
      else if (!strcmp(argv[formula_index], "-f"))
	{
486
	  translation = TransFM;
487
	}
488
      else if (!strcmp(argv[formula_index], "-fr"))
489
	{
490
	  fm_red = true;
491
	  translation = TransFM;
492
	}
493 494 495 496 497 498
      else if (!strcmp(argv[formula_index], "-fu"))
	{
	  fm_unambiguous = true;
	  fm_exprop_opt = true;
	  translation = TransFM;
	}
499 500 501 502
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
503 504
      else if (!strcmp(argv[formula_index], "-G"))
	{
505
	  accepting_run = true;
506 507
	  graph_run_tgba_opt = true;
	}
508 509 510
      else if (!strncmp(argv[formula_index], "-H", 2))
	{
	  output = 17;
511
	  hoa_opt = argv[formula_index] + 2;
512
	}
513 514 515 516
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
517 518 519 520
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
521 522 523 524
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
525 526 527 528 529
      else if (!strncmp(argv[formula_index], "-KP", 3))
	{
	  tm.start("reading -KP's argument");

	  spot::kripke_parse_error_list pel;
530 531
	  system_aut = spot::kripke_parse(argv[formula_index] + 3,
					  pel, dict, env, debug_opt);
532 533 534 535 536
	  if (spot::format_kripke_parse_errors(std::cerr,
					       argv[formula_index] + 2, pel))
	    return 2;
	  tm.stop("reading -KP's argument");
	}
537 538 539 540
      else if (!strcmp(argv[formula_index], "-KC"))
	{
	  output = 15;
	}
541 542 543 544
      else if (!strcmp(argv[formula_index], "-KW"))
	{
	  output = 16;
	}
545 546 547
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
548
	  translation = TransFM;
549
	}
550 551
      else if (!strcmp(argv[formula_index], "-m"))
	{
552
	  opt_reduce = true;
553
	}
martinez's avatar
martinez committed
554 555
      else if (!strcmp(argv[formula_index], "-N"))
	{
556
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
557
	  output = 8;
558
	  opt_never = nullptr;
martinez's avatar
martinez committed
559
	}
560 561 562 563
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
564
	  opt_never = "c";
565
	}
566
      else if (!strncmp(argv[formula_index], "-O", 2))
567
	{
568
	  output = 14;
569
          opt_minimize = true;
570 571
	  if (argv[formula_index][2] != 0)
	    opt_o_threshold = to_int(argv[formula_index] + 2);
572
	}
573 574 575
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
576
	  translation = TransFM;
577
	}
578 579
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
580 581
	  tm.start("reading -P's argument");

582
	  spot::parse_aut_error_list pel;
583 584
	  spot::automaton_parser_options opts;
	  opts.debug = debug_opt;
585
	  auto daut = spot::parse_aut(argv[formula_index] + 2, pel,
586
				      dict, env, opts);
587
	  if (spot::format_parse_aut_errors(std::cerr,
588
					    argv[formula_index] + 2, pel))
589
	    return 2;
590
	  daut->aut->merge_edges();
591
	  system_aut = daut->aut;
592
	  tm.stop("reading -P's argument");
593
	}
594 595
      else if (!strcmp(argv[formula_index], "-r1"))
	{
596 597
	  simpltl = true;
	  redopt.reduce_basics = true;
598 599 600
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
601 602
	  simpltl = true;
	  redopt.event_univ = true;
603 604 605
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
606 607
	  simpltl = true;
	  redopt.synt_impl = true;
608 609 610
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
611 612 613 614
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
615
	}
616 617
      else if (!strcmp(argv[formula_index], "-r5"))
	{
618 619
	  simpltl = true;
	  redopt.containment_checks = true;
620 621 622
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
623 624 625
	  simpltl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
626 627 628
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
629 630 631 632 633 634
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
635
	}
636 637 638 639
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
640
	{
641
	  // For backward compatibility, make all these options
642
	  // equal to -RDS.
643
	  reduction_dir_sim = true;
644
	}
Thomas Badie's avatar
Thomas Badie committed
645 646 647 648
      else if (!strcmp(argv[formula_index], "-RRS"))
        {
          reduction_rev_sim = true;
        }
649 650
      else if (!strcmp(argv[formula_index], "-R3"))
	{
651
	  scc_filter = true;
652
	}
653 654
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
655
	  scc_filter = true;
656 657
	  scc_filter_all = true;
	}
658 659
      else if (!strcmp(argv[formula_index], "-rd"))
	{
660
	  display_reduced_form = true;
661
	}
662 663 664 665
      else if (!strcmp(argv[formula_index], "-rD"))
	{
	  simpcache_stats = true;
	}
666 667 668 669
      else if (!strcmp(argv[formula_index], "-RC"))
	{
	  opt_complete = true;
	}
670
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
671
        {
672
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
673
        }
674 675 676 677
      else if (!strcmp(argv[formula_index], "-RIS"))
        {
          reduction_iterated_sim = true;
        }
678
      else if (!strcmp(argv[formula_index], "-rL"))
679 680 681 682 683
        {
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.reduce_size_strictly = true;
        }
684 685 686 687 688 689 690 691
      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;
        }
692 693 694 695
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
696 697 698 699 700
      else if (!strcmp(argv[formula_index], "-RM"))
        {
          opt_minimize = true;
	  reject_bigger = true;
        }
701
      else if (!strncmp(argv[formula_index], "-RQ", 3))
702 703
        {
          opt_determinize = true;
704 705
	  if (argv[formula_index][3] != 0)
	    opt_determinize_threshold = to_int(argv[formula_index] + 3);
706
        }
707 708 709 710 711
      else if (!strncmp(argv[formula_index], "-RS", 3))
        {
	  if (argv[formula_index][3] != 0)
	    opt_dtbasat = to_int(argv[formula_index] + 3);
	  else
712
	    opt_dtbasat = 0;
713 714
          //output = -1;
        }
715 716 717
      else if (!strcmp(argv[formula_index], "-RT"))
        {
          opt_bisim_ta = true;
718 719 720 721 722 723
	}
      else if (!strcmp(argv[formula_index], "-ru"))
        {
	  simpltl = true;
	  redopt.event_univ = true;
	  redopt.favor_event_univ = true;
724
        }
725 726 727 728
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
729 730
      else if (!strcmp(argv[formula_index], "-S"))
	{
731
	  dupexp = true;
732
	}
733 734 735 736 737 738 739 740
      else if (!strcmp(argv[formula_index], "-CL"))
	{
	  opt_closure = true;
	}
      else if (!strcmp(argv[formula_index], "-ST"))
	{
	  opt_stutterize = true;
	}
741 742 743 744
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
745 746 747 748
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
749 750 751 752
      else if (!strcmp(argv[formula_index], "-TA"))
        {
          ta_opt = true;
        }
753
      else if (!strcmp(argv[formula_index], "-TGTA"))
754
        {
755
          tgta_opt = true;
756
        }
757 758 759 760
      else if (!strcmp(argv[formula_index], "-lv"))
        {
          opt_with_artificial_livelock = true;
        }
761 762 763 764
      else if (!strcmp(argv[formula_index], "-sp"))
        {
          opt_single_pass_emptiness_check = true;
        }
765 766 767 768
      else if (!strcmp(argv[formula_index], "-in"))
        {
          opt_with_artificial_initial_state = false;
        }
769 770 771 772
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
773 774
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
775
	  unobservables = new spot::atomic_prop_set;
776
	  translation = TransFM;
777
	  // Parse -U's argument.
778
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
779 780
	  while (tok)
	    {
781
	      unobservables->insert(env.require(tok));
782
	      tok = strtok(nullptr, ", \t;");
783 784
	    }
	}
785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 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
      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;
	    }
	}
829 830 831 832
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
833 834
      else if (!strcmp(argv[formula_index], "-x"))
	{
835
	  translation = TransFM;
836 837
	  fm_exprop_opt = true;
	}
838
      else if (!strcmp(argv[formula_index], "-XD"))
839 840
	{
	  from_file = true;
841 842 843 844 845
	}
      else if (!strcmp(argv[formula_index], "-XDB"))
	{
	  from_file = true;
	  nra2nba = true;
846
	}
847 848 849 850
      else if (!strcmp(argv[formula_index], "-XH"))