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

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

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

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

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

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

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

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

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

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

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

	    << "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
195
196
197
198
	    << "          (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"
199
200
201
202
	    << std::endl

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

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

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

312
313
314
  exit(2);
}

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

328
329
330
331
332
int
main(int argc, char** argv)
{
  int exit_code = 0;

333
  bool debug_opt = false;
334
  bool paper_opt = false;
335
  bool utf8_opt = false;
336
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
337
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
338
  enum { TransFM, TransTAA, TransCompo } translation = TransFM;
339
  bool fm_red = false;
340
  bool fm_exprop_opt = false;
341
  bool fm_symb_merge_opt = true;
342
  bool file_opt = false;
343
  bool degen_reset = true;
344
  bool degen_order = false;
345
  bool degen_cache = true;
346
  int output = 0;
347
  int formula_index = 0;
348
349
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
350
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
351
  bool expect_counter_example = false;
352
353
  bool accepting_run = false;
  bool accepting_run_replay = false;
354
  bool from_file = false;
355
356
  enum { ReadSpot, ReadLbtt, ReadNeverclaim, ReadDstar } readformat = ReadSpot;
  bool nra2nba = false;
357
  bool dra2dba = false;
358
  bool scc_filter = false;
359
  bool simpltl = false;
360
361
  spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
					   false, false, false);
362
  bool simpcache_stats = false;
363
  bool scc_filter_all = false;
364
  bool display_reduced_form = false;
365
  bool post_branching = false;
366
  bool fair_loop_approx = false;
367
  bool graph_run_opt = false;
368
  bool graph_run_tgba_opt = false;
369
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
370
  bool opt_minimize = false;
371
  bool opt_determinize = false;
372
373
  unsigned opt_determinize_threshold = 0;
  unsigned opt_o_threshold = 0;
374
  bool opt_dtgbacomp = false;
375
  bool reject_bigger = false;
376
  bool opt_bisim_ta = false;
377
  bool opt_monitor = false;
378
  bool containment = false;
379
  bool show_fc = false;
380
  bool spin_comments = false;
381
382
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
383
  spot::tgba* system_aut = 0;
384
  const spot::tgba* product_to_free = 0;
385
  spot::bdd_dict* dict = new spot::bdd_dict();
386
387
  spot::timer_map tm;
  bool use_timer = false;
Thomas Badie's avatar
Thomas Badie committed
388
  bool reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
389
  bool reduction_rev_sim = false;
390
  bool reduction_iterated_sim = false;
Thomas Badie's avatar
Thomas Badie committed
391
392
393
  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
394
  spot::tgba* temp_dir_sim = 0;
395
  bool ta_opt = false;
396
  bool tgta_opt = false;
397
  bool opt_with_artificial_initial_state = true;
398
399
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
Thomas Badie's avatar
Thomas Badie committed
400
  spot::tgba* temp_rev_sim = 0;
401
  spot::tgba* temp_iterated_sim = 0;
Thomas Badie's avatar
Thomas Badie committed
402
403
  spot::tgba* temp_dont_care_sim = 0;
  spot::tgba* temp_dont_care_iterated_sim = 0;
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
	  degeneralize_opt = DegenTBA;
	}
456
457
      else if (!strcmp(argv[formula_index], "-DC"))
	{
458
	  opt_dtgbacomp = true;
459
	}
460
      else if (!strncmp(argv[formula_index], "-DS", 3))
461
462
	{
	  degeneralize_opt = DegenSBA;
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
	  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;
		}
	    }
488
	}
489
      else if (!strncmp(argv[formula_index], "-e", 2))
490
        {
491
492
493
494
495
496
497
498
499
500
	  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 `"
501
			<< err <<  '\'' << std::endl;
502
503
	      exit(2);
	    }
504
505
506
          expect_counter_example = true;
          output = -1;
        }
507
      else if (!strncmp(argv[formula_index], "-E", 2))
508
        {
509
510
511
512
513
514
515
516
517
518
	  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 `"
519
			<< err <<  '\'' << std::endl;
520
521
	      exit(2);
	    }
522
523
524
          expect_counter_example = false;
          output = -1;
        }
525
526
      else if (!strcmp(argv[formula_index], "-f"))
	{
527
	  translation = TransFM;
528
	}
529
      else if (!strcmp(argv[formula_index], "-fr"))
530
	{
531
	  fm_red = true;
532
	  translation = TransFM;
533
	}
534
535
536
537
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
538
539
540
541
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
542
543
      else if (!strcmp(argv[formula_index], "-g"))
	{
544
	  accepting_run = true;
545
546
	  graph_run_opt = true;
	}
547
548
      else if (!strcmp(argv[formula_index], "-G"))
	{
549
	  accepting_run = true;
550
551
	  graph_run_tgba_opt = true;
	}
552
553
554
555
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
556
557
558
559
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
560
561
562
563
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
564
565
566
567
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
568
569
570
571
572
      else if (!strncmp(argv[formula_index], "-KP", 3))
	{
	  tm.start("reading -KP's argument");

	  spot::kripke_parse_error_list pel;
573
574
	  system_aut = spot::kripke_parse(argv[formula_index] + 3,
					  pel, dict, env, debug_opt);
575
576
577
578
579
	  if (spot::format_kripke_parse_errors(std::cerr,
					       argv[formula_index] + 2, pel))
	    return 2;
	  tm.stop("reading -KP's argument");
	}
580
581
582
583
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
584
585
586
587
      else if (!strcmp(argv[formula_index], "-KC"))
	{
	  output = 15;
	}
588
589
590
591
      else if (!strcmp(argv[formula_index], "-KW"))
	{
	  output = 16;
	}
592
593
594
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
595
	  translation = TransFM;
596
	}
597
598
599
600
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
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* s;
634
635
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, 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
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
802
803
804
805
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
806
807
808
809
      else if (!strcmp(argv[formula_index], "-TA"))
        {
          ta_opt = true;
        }
810
      else if (!strcmp(argv[formula_index], "-TGTA"))
811
        {
812
          tgta_opt = true;
813
        }
814
815
816
817
      else if (!strcmp(argv[formula_index], "-lv"))
        {
          opt_with_artificial_livelock = true;
        }
818
819
820
821
      else if (!strcmp(argv[formula_index], "-sp"))
        {
          opt_single_pass_emptiness_check = true;
        }
822
823
824
825
      else if (!strcmp(argv[formula_index], "-in"))
        {
          opt_with_artificial_initial_state = false;
        }
826
827
828
829
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
830
831
832
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
833
	  translation = TransFM;
834
	  // Parse -U's argument.
835
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
836
837
838
	  while (tok)
	    {
	      unobservables->insert
839
		(static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
840
	      tok = strtok(0, ", \t;");
841
842
	    }
	}
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
      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;
	    }
	}
887
888
889
890
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
891
892
      else if (!strcmp(argv[formula_index], "-x"))
	{
893
	  translation = TransFM;
894
895
	  fm_exprop_opt = true;
	}
896
897
898
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
899
	  readformat = ReadSpot;
900
	}
901
      else if (!strcmp(argv[formula_index], "-XD"))
902
903
	{
	  from_file = true;
904
905
906
907
908
909
910
	  readformat = ReadDstar;
	}
      else if (!strcmp(argv[formula_index], "-XDB"))
	{
	  from_file = true;
	  readformat = ReadDstar;
	  nra2nba = true;
911
	}
912
913
914
915
916
917
918
      else if (!strcmp(argv[formula_index], "-XDD"))
	{
	  from_file = true;
	  readformat = ReadDstar;
	  nra2nba = true;
	  dra2dba = true;
	}
919
920
921
      else if (!strcmp(argv[formula_index], "-XL"))
	{
	  from_file = true;
922
923
924
925
926
927
	  readformat = ReadLbtt;
	}
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  readformat = ReadNeverclaim;
928
	}
929
930
      else if (!strcmp(argv[formula_index], "-y"))
	{
931
	  translation = TransFM;
932
933
	  fm_symb_merge_opt = false;
	}
934
935
936
937
      else
	{
	  break;
	}
938
939
    }

940
  if ((graph_run_opt || graph_run_tgba_opt)
941
      && (!echeck_inst || !expect_counter_example))
942
    {
943
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
944
945
946
      exit(1);
    }

947
948
949
950
  std::string input;

  if (file_opt)
    {
951
      tm.start("reading formula");
952
      if (strcmp(argv[formula_index], "-"))
953
	{
954
	  std::ifstream fin(argv[formula_index]);
955
	  if (!fin)
956
957
958
959
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
960

961
	  if (!std::getline(fin, input, '\0'))
962
963
964
965
966
967
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
968
	{
969
	  std::getline(std::cin, input, '\0');
970
	}
971
      tm.stop("reading formula");
972
973
974
975
976
977
    }
  else
    {
      input = argv[formula_index];
    }

978
  const spot::ltl::formula* f = 0;
979
  if (!from_file) // Reading a formula, not reading an automaton from a file.
980
    {
981
982
983
984
      switch (translation)
	{
	case TransFM:
	case TransTAA:
985
	case TransCompo:
986
987
988
989
990
991
992
993
	  {
	    spot::ltl::parse_error_list pel;
	    tm.start("parsing formula");
	    f = spot::ltl::parse(input, pel, env, debug_opt);
	    tm.stop("parsing formula");
	    exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
	  }
	  break;
994
	}
995
    }
996