ltl2tgba.cc 57.5 KB
Newer Older
1
// -*- coding: utf-8 -*-
2 3 4 5
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012, 2013, 2014
// 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_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"
61
#include "tgbaalgos/stats.hh"
62
#include "tgbaalgos/scc.hh"
63
#include "tgbaalgos/emptiness_stats.hh"
64
#include "tgbaalgos/scc.hh"
65
#include "tgbaalgos/sccinfo.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
#include "tgbaalgos/powerset.hh"
73
#include "tgbaalgos/dtgbacomp.hh"
74 75
#include "tgbaalgos/complete.hh"
#include "tgbaalgos/dtbasat.hh"
76
#include "tgbaalgos/dtgbasat.hh"
77

78
#include "taalgos/tgba2ta.hh"
79
#include "taalgos/dotty.hh"
80
#include "taalgos/stats.hh"
81

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

100 101 102
void
syntax(char* prog)
{
103 104 105 106 107
  // 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;

108
  std::cerr << "Usage: "<< prog << " [-f|-l|-le|-taa] [OPTIONS...] formula"
109
	    << std::endl
110
            << "       "<< prog << " [-f|-l|-le|-taa] -F [OPTIONS...] file"
111
	    << std::endl
112
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing  
Alexandre Duret-Lutz committed
113
	    << std::endl
114

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

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

	    << "Translation algorithm:" << std::endl
145
            << "  -f    use Couvreur's FM algorithm for LTL"
146
	    << " (default)" << std::endl
147
            << "  -l    use Couvreur's LaCIM algorithm for LTL "
148
	    << std::endl
149 150 151
	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
	    << std::endl
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
152
	    << std::endl
153 154
	    << "  -u    use Compositional translation"
	    << std::endl
155 156 157
	    << std::endl

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

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

	    << "Options for Tauriainen's TAA-based algorithm (-taa):"
188
	    << std::endl
189
	    << "  -c    enable language containment checks (implies -taa)"
190
	    << std::endl
191
	    << std::endl
192 193

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

	    << "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
217 218 219 220
	    << "          (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"
221 222 223 224
	    << std::endl

	    << "Automaton simplifications (after translation):"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
225
	    << "  -R3   use SCC to reduce the automaton" << std::endl
226
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
227 228 229
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
230
	    << "  -RDS  reduce the automaton with direct simulation"
231
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
232
	    << "  -RRS  reduce the automaton with reverse simulation"
Thomas Badie's avatar
Thomas Badie committed
233
	    << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
234
	    << "  -RIS  iterate both direct and reverse simulations"
235
	    << std::endl
Thomas Badie's avatar
Thomas Badie committed
236 237
            << "  -RDCS reduce the automaton with direct simulation"
            << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
238
            << "  -Rm   attempt to WDBA-minimize the automaton" << std::endl
239
	    << std::endl
240 241
            << "  -RM   attempt to WDBA-minimize the automaton unless the "
	    << "result is bigger" << std::endl
242
	    << "  -RQ   determinize a TGBA (assuming it's legal!)" << std::endl
243
	    << std::endl
244

245
            << "Automaton conversion:" << std::endl
246 247
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
248
	    << "  -s    convert to explicit automaton, and number states "
249
	    << "in DFS order" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
250
	    << "  -S    convert to explicit automaton, and number states "
251
	    << "in BFS order" << std::endl
252 253
	    << std::endl

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

334 335 336
  exit(2);
}

Thomas Badie's avatar
Thomas Badie committed
337 338 339 340 341 342
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
343 344 345 346
    {
      std::cerr << "Failed to parse `" << s << "' as an integer." << std::endl;
      exit(1);
    }
Thomas Badie's avatar
Thomas Badie committed
347 348 349
  return res;
}

350 351 352 353 354
int
main(int argc, char** argv)
{
  int exit_code = 0;

355
  bool debug_opt = false;
356
  bool paper_opt = false;
357
  bool utf8_opt = false;
358
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
359
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
360 361
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA,
	 TransCompo }
362
    translation = TransFM;
363
  bool fm_red = false;
364
  bool fm_exprop_opt = false;
365
  bool fm_symb_merge_opt = true;
366
  bool file_opt = false;
367
  bool degen_reset = true;
368
  bool degen_order = false;
369
  bool degen_cache = true;
370
  int output = 0;
371
  int formula_index = 0;
372 373
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
374
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
375
  bool expect_counter_example = false;
376 377
  bool accepting_run = false;
  bool accepting_run_replay = false;
378
  bool from_file = false;
379 380
  enum { ReadSpot, ReadLbtt, ReadNeverclaim, ReadDstar } readformat = ReadSpot;
  bool nra2nba = false;
381
  bool dra2dba = false;
382
  bool scc_filter = false;
383
  bool simpltl = false;
384 385
  spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
					   false, false, false);
386
  bool simpcache_stats = false;
387
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
388
  bool symbolic_scc_pruning = false;
389
  bool display_reduced_form = false;
390
  bool post_branching = false;
391
  bool fair_loop_approx = false;
392
  bool graph_run_opt = false;
393
  bool graph_run_tgba_opt = false;
394
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
395
  bool opt_minimize = false;
396
  bool opt_determinize = false;
397 398
  unsigned opt_determinize_threshold = 0;
  unsigned opt_o_threshold = 0;
399
  bool opt_dtgbacomp = false;
400
  bool reject_bigger = false;
401
  bool opt_bisim_ta = false;
402
  bool opt_monitor = false;
403
  bool containment = false;
404
  bool show_fc = false;
405
  bool spin_comments = false;
406 407
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
408
  spot::tgba* system_aut = 0;
409
  const spot::tgba* product_to_free = 0;
410
  spot::bdd_dict* dict = new spot::bdd_dict();
411 412
  spot::timer_map tm;
  bool use_timer = false;
Thomas Badie's avatar
Thomas Badie committed
413
  bool reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
414
  bool reduction_rev_sim = false;
415
  bool reduction_iterated_sim = false;
Thomas Badie's avatar
Thomas Badie committed
416 417 418
  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
419
  spot::tgba* temp_dir_sim = 0;
420
  bool ta_opt = false;
421
  bool tgta_opt = false;
422
  bool opt_with_artificial_initial_state = true;
423 424
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
Thomas Badie's avatar
Thomas Badie committed
425
  spot::tgba* temp_rev_sim = 0;
426
  spot::tgba* temp_iterated_sim = 0;
Thomas Badie's avatar
Thomas Badie committed
427 428
  spot::tgba* temp_dont_care_sim = 0;
  spot::tgba* temp_dont_care_iterated_sim = 0;
429 430 431 432 433
  bool cs_nowdba = true;
  bool cs_wdba_smaller = false;
  bool cs_nosimul = true;
  bool cs_early_start = false;
  bool cs_oblig = false;
434 435
  bool opt_complete = false;
  int opt_dtbasat = -1;
436
  int opt_dtgbasat = -1;
437

438
  for (;;)
439
    {
440
      if (argc < formula_index + 2)
441
	syntax(argv[0]);
442 443 444

      ++formula_index;

445 446 447 448
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
449 450 451 452 453
      else if (!strcmp(argv[formula_index], "-8"))
	{
	  utf8_opt = true;
	  spot::enable_utf8();
	}
454
      else if (!strcmp(argv[formula_index], "-a"))
455 456 457
	{
	  output = 2;
	}
458
      else if (!strcmp(argv[formula_index], "-A"))
459
	{
460
	  output = 4;
461
	}
462
      else if (!strcmp(argv[formula_index], "-b"))
463
	{
464
	  output = 7;
465
	}
466 467 468
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
469
	  translation = TransTAA;
470
	}
471 472 473 474 475 476 477 478 479
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
480
      else if (!strcmp(argv[formula_index], "-d"))
481 482 483
	{
	  debug_opt = true;
	}
484 485
      else if (!strcmp(argv[formula_index], "-D"))
	{
486 487
	  degeneralize_opt = DegenTBA;
	}
488 489
      else if (!strcmp(argv[formula_index], "-DC"))
	{
490
	  opt_dtgbacomp = true;
491
	}
492
      else if (!strncmp(argv[formula_index], "-DS", 3))
493 494
	{
	  degeneralize_opt = DegenSBA;
495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519
	  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;
		}
	    }
520
	}
521
      else if (!strncmp(argv[formula_index], "-e", 2))
522
        {
523 524 525 526 527 528 529 530 531 532
	  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 `"
533
			<< err <<  '\'' << std::endl;
534 535
	      exit(2);
	    }
536 537 538
          expect_counter_example = true;
          output = -1;
        }
539
      else if (!strncmp(argv[formula_index], "-E", 2))
540
        {
541 542 543 544 545 546 547 548 549 550
	  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 `"
551
			<< err <<  '\'' << std::endl;
552 553
	      exit(2);
	    }
554 555 556
          expect_counter_example = false;
          output = -1;
        }
557 558
      else if (!strcmp(argv[formula_index], "-f"))
	{
559
	  translation = TransFM;
560
	}
561
      else if (!strcmp(argv[formula_index], "-fr"))
562
	{
563
	  fm_red = true;
564
	  translation = TransFM;
565
	}
566 567 568 569
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
570 571 572 573
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
574 575
      else if (!strcmp(argv[formula_index], "-g"))
	{
576
	  accepting_run = true;
577 578
	  graph_run_opt = true;
	}
579 580
      else if (!strcmp(argv[formula_index], "-G"))
	{
581
	  accepting_run = true;
582 583
	  graph_run_tgba_opt = true;
	}
584 585 586 587
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
588 589 590 591
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
592 593 594 595
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
596 597 598 599
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
600 601 602 603 604
      else if (!strncmp(argv[formula_index], "-KP", 3))
	{
	  tm.start("reading -KP's argument");

	  spot::kripke_parse_error_list pel;
605 606
	  system_aut = spot::kripke_parse(argv[formula_index] + 3,
					  pel, dict, env, debug_opt);
607 608 609 610 611
	  if (spot::format_kripke_parse_errors(std::cerr,
					       argv[formula_index] + 2, pel))
	    return 2;
	  tm.stop("reading -KP's argument");
	}
612 613 614 615
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
616 617 618 619
      else if (!strcmp(argv[formula_index], "-KC"))
	{
	  output = 15;
	}
620 621 622 623
      else if (!strcmp(argv[formula_index], "-KW"))
	{
	  output = 16;
	}
624 625 626 627
      else if (!strcmp(argv[formula_index], "-l"))
	{
	  translation = TransLaCIM;
	}
628 629 630 631 632 633 634 635 636 637
      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;
	}
638 639 640
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
641
	  translation = TransFM;
642
	}
643 644 645 646
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
647 648
      else if (!strcmp(argv[formula_index], "-m"))
	{
649
	  opt_reduce = true;
650
	}
martinez's avatar
martinez committed
651 652
      else if (!strcmp(argv[formula_index], "-N"))
	{
653
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
654 655
	  output = 8;
	}
656 657 658 659 660 661
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
	  spin_comments = true;
	}
662
      else if (!strncmp(argv[formula_index], "-O", 2))
663
	{
664
	  output = 14;
665
          opt_minimize = true;
666 667
	  if (argv[formula_index][2] != 0)
	    opt_o_threshold = to_int(argv[formula_index] + 2);
668
	}
669 670 671
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
672
	  translation = TransFM;
673
	}
674 675
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
676 677
	  tm.start("reading -P's argument");

678
	  spot::tgba_parse_error_list pel;
679
	  spot::tgba_digraph* s;
680 681
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, env, debug_opt);
682 683
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
684
	    return 2;
685
	  s->merge_transitions();
686
	  tm.stop("reading -P's argument");
687
	  system_aut = s;
688
	}
689 690
      else if (!strcmp(argv[formula_index], "-r"))
	{
691 692
	  output = 1;
	}
693 694
      else if (!strcmp(argv[formula_index], "-r1"))
	{
695 696
	  simpltl = true;
	  redopt.reduce_basics = true;
697 698 699
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
700 701
	  simpltl = true;
	  redopt.event_univ = true;
702 703 704
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
705 706
	  simpltl = true;
	  redopt.synt_impl = true;
707 708 709
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
710 711 712 713
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
714
	}
715 716
      else if (!strcmp(argv[formula_index], "-r5"))
	{
717 718
	  simpltl = true;
	  redopt.containment_checks = true;
719 720 721
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
722 723 724
	  simpltl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
725 726 727
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
728 729 730 731 732 733
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
734
	}
735 736 737
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
738
	}
739 740 741 742
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
743
	{
744
	  // For backward compatibility, make all these options
745
	  // equal to -RDS.
746
	  reduction_dir_sim = true;
747
	}
Thomas Badie's avatar
Thomas Badie committed
748 749 750 751
      else if (!strcmp(argv[formula_index], "-RRS"))
        {
          reduction_rev_sim = true;
        }
752 753
      else if (!strcmp(argv[formula_index], "-R3"))
	{
754
	  scc_filter = true;
755
	}
756 757
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
758
	  scc_filter = true;
759 760
	  scc_filter_all = true;
	}
761 762
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
763
	  symbolic_scc_pruning = true;
764
	}
765 766
      else if (!strcmp(argv[formula_index], "-rd"))
	{
767
	  display_reduced_form = true;
768
	}
769 770 771 772
      else if (!strcmp(argv[formula_index], "-rD"))
	{
	  simpcache_stats = true;
	}
773 774 775 776
      else if (!strcmp(argv[formula_index], "-RC"))
	{
	  opt_complete = true;
	}
777
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
778
        {
779
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
780
        }
781 782 783 784
      else if (!strcmp(argv[formula_index], "-RIS"))
        {
          reduction_iterated_sim = true;
        }
Thomas Badie's avatar
Thomas Badie committed
785 786 787 788 789 790 791 792 793 794 795 796
      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);
        }
797
      else if (!strcmp(argv[formula_index], "-rL"))
798 799 800 801 802
        {
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.reduce_size_strictly = true;
        }
803 804 805 806 807 808 809 810
      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;
        }
811 812 813 814
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
815 816 817