ltl2tgba.cc 47.4 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/dotty.hh"
37
#include "tgbaalgos/lbtt.hh"
38
#include "tgbaalgos/hoa.hh"
39
#include "tgbaalgos/degen.hh"
40
#include "tgba/tgbaproduct.hh"
41
#include "tgbaalgos/reducerun.hh"
42
#include "dstarparse/public.hh"
43
#include "hoaparse/public.hh"
44
#include "tgbaalgos/dupexp.hh"
Felix Abecassis's avatar
Felix Abecassis committed
45
#include "tgbaalgos/minimize.hh"
46
#include "taalgos/minimize.hh"
47
#include "tgbaalgos/neverclaim.hh"
48
#include "tgbaalgos/replayrun.hh"
49
#include "tgbaalgos/sccfilter.hh"
50
#include "tgbaalgos/safety.hh"
51
#include "tgbaalgos/gtec/gtec.hh"
52
#include "misc/timer.hh"
53
#include "tgbaalgos/stats.hh"
54
#include "tgbaalgos/sccinfo.hh"
55
#include "tgbaalgos/emptiness_stats.hh"
56
#include "tgbaalgos/scc.hh"
57
#include "tgbaalgos/sccinfo.hh"
58
#include "tgbaalgos/isdet.hh"
59
#include "tgbaalgos/cycles.hh"
60
#include "tgbaalgos/isweakscc.hh"
61
#include "kripkeparse/public.hh"
Thomas Badie's avatar
Thomas Badie committed
62
#include "tgbaalgos/simulation.hh"
63
#include "tgbaalgos/compsusp.hh"
64
#include "tgbaalgos/powerset.hh"
65
#include "tgbaalgos/dtgbacomp.hh"
66 67
#include "tgbaalgos/complete.hh"
#include "tgbaalgos/dtbasat.hh"
68
#include "tgbaalgos/dtgbasat.hh"
69
#include "tgbaalgos/stutter.hh"
70

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

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

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

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

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

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
118
	    << std::endl
119 120 121 122
	    << "  -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
123 124
	    << "  -XDD  read the from an ltl2dstar file and convert it to "
	    << "TGBA,\n       keeping it deterministic when possible\n"
125 126
	    << "  -XH   do not compute an automaton, read it from a"
	    << " HOA file\n"
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
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
141
	    << std::endl
142 143
	    << "  -u    use Compositional translation"
	    << std::endl
144 145 146
	    << std::endl

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

	    << "Options for Tauriainen's TAA-based algorithm (-taa):"
162
	    << std::endl
163
	    << "  -c    enable language containment checks (implies -taa)"
164
	    << std::endl
165
	    << std::endl
166 167

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

	    << "Automaton degeneralization (after translation):"
	    << std::endl
187
	    << "  -DT   degeneralize the automaton as a TBA" << std::endl
188
	    << "  -DS   degeneralize the automaton as an SBA" << std::endl
189 190 191 192
	    << "          (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"
193 194 195 196
	    << std::endl

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

215
            << "Automaton conversion:" << std::endl
216 217
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
218
	    << "  -s    convert to explicit automaton, and number states "
219
	    << "in DFS order" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
220
	    << "  -S    convert to explicit automaton, and number states "
221
	    << "in BFS order" << std::endl
222 223
	    << std::endl

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

296 297 298
  exit(2);
}

Thomas Badie's avatar
Thomas Badie committed
299 300 301 302 303 304
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
305 306 307 308
    {
      std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
      exit(1);
    }
Thomas Badie's avatar
Thomas Badie committed
309 310 311
  return res;
}

312 313 314 315 316
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;
317
  return spot::make_tgba_digraph(a, spot::twa::prop_set::all());
318 319
}

320
int
321
checked_main(int argc, char** argv)
322 323 324
{
  int exit_code = 0;

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

396
  for (;;)
397
    {
398
      if (argc < formula_index + 2)
399
	syntax(argv[0]);
400 401 402

      ++formula_index;

403 404 405 406
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
407 408 409 410 411
      else if (!strcmp(argv[formula_index], "-8"))
	{
	  utf8_opt = true;
	  spot::enable_utf8();
	}
412 413 414
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
415
	  translation = TransTAA;
416
	}
417 418 419 420 421 422 423 424 425
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
426
      else if (!strcmp(argv[formula_index], "-d"))
427 428 429
	{
	  debug_opt = true;
	}
430 431
      else if (!strcmp(argv[formula_index], "-D"))
	{
432 433
	  std::cerr << "-D was renamed to -DT\n";
	  abort();
434
	}
435 436
      else if (!strcmp(argv[formula_index], "-DC"))
	{
437
	  opt_dtgbacomp = true;
438
	}
439 440
      else if (!strncmp(argv[formula_index], "-DS", 3)
	       || !strncmp(argv[formula_index], "-DT", 3))
441
	{
442 443
	  degeneralize_opt =
	    argv[formula_index][2] == 'S' ? DegenSBA : DegenTBA;
444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468
	  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;
		}
	    }
469
	}
470
      else if (!strncmp(argv[formula_index], "-e", 2))
471
        {
472 473 474 475 476 477
	  echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
478
	    spot::make_emptiness_check_instantiator(echeck_algo, &err);
479 480 481
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
482
			<< err <<  '\'' << std::endl;
483 484
	      exit(2);
	    }
485 486 487
          expect_counter_example = true;
          output = -1;
        }
488
      else if (!strncmp(argv[formula_index], "-E", 2))
489
        {
490 491 492 493 494 495
	  const char* echeck_algo = 2 + argv[formula_index];
	  if (!*echeck_algo)
	    echeck_algo = "Cou99";

	  const char* err;
	  echeck_inst =
496
	    spot::make_emptiness_check_instantiator(echeck_algo, &err);
497 498 499
	  if (!echeck_inst)
	    {
	      std::cerr << "Failed to parse argument of -e near `"
500
			<< err <<  '\'' << std::endl;
501 502
	      exit(2);
	    }
503 504 505
          expect_counter_example = false;
          output = -1;
        }
506 507
      else if (!strcmp(argv[formula_index], "-f"))
	{
508
	  translation = TransFM;
509
	}
510
      else if (!strcmp(argv[formula_index], "-fr"))
511
	{
512
	  fm_red = true;
513
	  translation = TransFM;
514
	}
515 516 517 518
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
519 520
      else if (!strcmp(argv[formula_index], "-G"))
	{
521
	  accepting_run = true;
522 523
	  graph_run_tgba_opt = true;
	}
524 525 526
      else if (!strncmp(argv[formula_index], "-H", 2))
	{
	  output = 17;
527
	  hoa_opt = argv[formula_index] + 2;
528
	}
529 530 531 532
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
533 534 535 536
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
537 538 539 540
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
541 542 543 544 545
      else if (!strncmp(argv[formula_index], "-KP", 3))
	{
	  tm.start("reading -KP's argument");

	  spot::kripke_parse_error_list pel;
546 547
	  system_aut = spot::kripke_parse(argv[formula_index] + 3,
					  pel, dict, env, debug_opt);
548 549 550 551 552
	  if (spot::format_kripke_parse_errors(std::cerr,
					       argv[formula_index] + 2, pel))
	    return 2;
	  tm.stop("reading -KP's argument");
	}
553 554 555 556
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
557 558 559 560
      else if (!strcmp(argv[formula_index], "-KC"))
	{
	  output = 15;
	}
561 562 563 564
      else if (!strcmp(argv[formula_index], "-KW"))
	{
	  output = 16;
	}
565 566 567
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
568
	  translation = TransFM;
569
	}
570 571
      else if (!strcmp(argv[formula_index], "-m"))
	{
572
	  opt_reduce = true;
573
	}
martinez's avatar
martinez committed
574 575
      else if (!strcmp(argv[formula_index], "-N"))
	{
576
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
577
	  output = 8;
578
	  opt_never = nullptr;
martinez's avatar
martinez committed
579
	}
580 581 582 583
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
584
	  opt_never = "c";
585
	}
586
      else if (!strncmp(argv[formula_index], "-O", 2))
587
	{
588
	  output = 14;
589
          opt_minimize = true;
590 591
	  if (argv[formula_index][2] != 0)
	    opt_o_threshold = to_int(argv[formula_index] + 2);
592
	}
593 594 595
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
596
	  translation = TransFM;
597
	}
598 599
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
600 601
	  tm.start("reading -P's argument");

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