ltl2tgba.cc 50.8 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
277
278
	    << "  -k    display statistics on the automaton (size and SCCs)"
	    << std::endl
	    << "  -ks   display statistics on the automaton (size only)"
279
	    << std::endl
280
281
282
	    << "  -kt   display statistics on the automaton (size + "
	    << "subtransitions)"
	    << std::endl
283
284
285
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
	    << std::endl
286
	    << "  -KC   list cycles in automaton" << std::endl
287
	    << "  -KW   list weak SCCs" << std::endl
288
	    << "  -N    output the never clain for Spin (implies -DS)"
289
290
	    << std::endl
	    << "  -NN   output the never clain for Spin, with commented states"
291
	    << " (implies -DS)" << std::endl
292
293
	    << "  -O    tell if a formula represents a safety, guarantee, "
	    << "or obligation property"
294
	    << std::endl
295
296
297
298
299
300
	    << "  -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
301
	    << "  -8    output UTF-8 formulae" << std::endl
302
303
304
305
	    << "  -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"
306
	    << std::endl
307
	    << std::endl;
308

309
310
311
  exit(2);
}

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

325
326
327
328
329
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;
330
  return spot::make_tgba_digraph(a, spot::tgba::prop_set::all());
331
332
}

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

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

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

      ++formula_index;

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

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

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

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

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

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

952
  if ((graph_run_opt || graph_run_tgba_opt)