ltl2tgba.cc 45.1 KB
Newer Older
1
2
3
// -*- coding: utf-8 -*-
// Copyright (C) 2007, 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
4
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
5
6
// Paris 6 (LIP6), département Systèmes Répartis
// Coopératifs (SRC), Université Pierre et Marie Curie.
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
//
// 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
// the Free Software Foundation; either version 2 of the License, or
// (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
// along with Spot; see the file COPYING.  If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.

25
#include <iostream>
26
#include <iomanip>
27
#include <cassert>
28
29
#include <fstream>
#include <string>
30
#include <cstdlib>
31
#include "ltlvisit/tostring.hh"
32
#include "ltlvisit/apcollect.hh"
33
#include "ltlast/allnodes.hh"
34
#include "ltlparse/public.hh"
35
#include "tgbaalgos/ltl2tgba_lacim.hh"
36
#include "tgbaalgos/ltl2tgba_fm.hh"
37
#include "tgbaalgos/ltl2taa.hh"
38
#include "tgba/bddprint.hh"
39
#include "tgbaalgos/save.hh"
40
#include "tgbaalgos/dotty.hh"
41
#include "tgbaalgos/lbtt.hh"
42
#include "tgba/tgbatba.hh"
43
#include "tgba/tgbasgba.hh"
44
#include "tgbaalgos/degen.hh"
45
#include "tgba/tgbaproduct.hh"
46
#include "tgba/futurecondcol.hh"
47
#include "tgbaalgos/reducerun.hh"
48
#include "tgbaparse/public.hh"
49
#include "neverparse/public.hh"
50
#include "tgbaalgos/dupexp.hh"
Felix Abecassis's avatar
Felix Abecassis committed
51
#include "tgbaalgos/minimize.hh"
52
#include "taalgos/minimize.hh"
53
#include "tgbaalgos/neverclaim.hh"
54
#include "tgbaalgos/replayrun.hh"
55
#include "tgbaalgos/rundotdec.hh"
56
#include "tgbaalgos/sccfilter.hh"
57
#include "tgbaalgos/safety.hh"
58
#include "tgbaalgos/eltl2tgba_lacim.hh"
59
#include "tgbaalgos/gtec/gtec.hh"
60
#include "eltlparse/public.hh"
61
#include "misc/timer.hh"
62
#include "tgbaalgos/stats.hh"
63
#include "tgbaalgos/scc.hh"
64
#include "tgbaalgos/emptiness_stats.hh"
65
66
#include "tgbaalgos/scc.hh"
#include "kripkeparse/public.hh"
Thomas Badie's avatar
Thomas Badie committed
67
#include "tgbaalgos/simulation.hh"
68

69
#include "taalgos/tgba2ta.hh"
70
#include "taalgos/dotty.hh"
71
#include "taalgos/stats.hh"
72

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

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

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

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

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
116
	    << std::endl
117
	    << "  -X    do not compute an automaton, read it from a file"
118
	    << std::endl
119
120
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
121
122
123
124
	    << "  -Pfile  multiply the formula automaton with the TGBA read"
	    << " from `file'\n"
	    << "  -KPfile multiply the formula automaton with the Kripke"
	    << " structure from `file'\n"
125
126
127
	    << std::endl

	    << "Translation algorithm:" << std::endl
128
            << "  -f    use Couvreur's FM algorithm for LTL"
129
	    << " (default)" << std::endl
130
            << "  -l    use Couvreur's LaCIM algorithm for LTL "
131
	    << std::endl
132
133
134
	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
	    << std::endl
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
135
	    << std::endl
136
137
138
	    << std::endl

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
139
140
	    << "  -fr   reduce formula at each step of FM" << std::endl
	    << "          as specified with the -r{1..7} options" << std::endl
141
142
143
144
145
            << "  -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)"
146
	    << std::endl
147
148
149
150
            << "  -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
151
	    << std::endl
152

153
154
	    << "Options for Couvreur's LaCIM algorithm (-l or -le):"
	    << std::endl
155
156
	    << "  -a    display the acceptance_conditions BDD, not the "
	    << "reachability graph"
157
	    << std::endl
158
	    << "  -A    same as -a, but as a set" << std::endl
159
160
	    << "  -lo   pre-define standard LTL operators as automata "
	    << "(implies -le)" << std::endl
161
	    << "  -r    display the relation BDD, not the reachability graph"
162
	    << std::endl
163
	    << "  -R    same as -r, but as a set" << std::endl
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
164
165
	    << "  -R3b  symbolically prune unaccepting SCC from BDD relation"
	    << std::endl
166
	    << std::endl
167
168

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

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

	    << "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
	    << std::endl

	    << "Automaton simplifications (after translation):"
	    << std::endl
200
	    << "  -R3   use SCC to reduce the automata" << std::endl
201
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
202
203
204
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
205
206
	    << "  -RDS  minimize the automaton with direct simulation"
	    << std::endl
Thomas Badie's avatar
Thomas Badie committed
207
208
	    << "  -RRS  minimize the automaton with reverse simulation"
	    << std::endl
209
210
211
	    << "  -RPS  minimize the automaton with an alternance"
            << " reverse simulation and simulation"
	    << std::endl
212
            << "  -Rm   attempt to WDBA-minimize the automata" << std::endl
213
	    << std::endl
214

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

224
225
226
227
228
229
230
231
232
233
234
235
236
237
	    << "Conversion to Testing Automaton:" << std::endl
 	    << "  -TA   output a Generalized Testing Automaton (GTA),\n"
	    << "          or a Testing Automaton (TA) with -DS\n"
 	    << "  -lv   add an artificial livelock state to obtain a "
	    << "Single-pass (G)TA\n"
            << "  -sp   convert into a single-pass (G)TA without artificial "
	    << "livelock state\n"
	    << "  -in   do not use an artificial initial state\n"
            << "  -TGTA output a Transition-based Generalized TA"
            << std::endl
	    << "  -RT   reduce the (G)TA/TGTA using bisimulation.\n"
            << std::endl

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

302
303
304
305
306
307
308
309
  exit(2);
}

int
main(int argc, char** argv)
{
  int exit_code = 0;

310
  bool debug_opt = false;
311
  bool paper_opt = false;
312
  bool utf8_opt = false;
313
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
314
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
315
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
316
    translation = TransFM;
317
  bool fm_red = false;
318
  bool fm_exprop_opt = false;
319
  bool fm_symb_merge_opt = true;
320
  bool file_opt = false;
321
  int output = 0;
322
  int formula_index = 0;
323
324
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
325
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
326
  bool expect_counter_example = false;
327
328
  bool accepting_run = false;
  bool accepting_run_replay = false;
329
  bool from_file = false;
330
  bool read_neverclaim = false;
331
  bool scc_filter = false;
332
  bool simpltl = false;
333
334
  spot::ltl::ltl_simplifier_options redopt(false, false, false, false,
					   false, false, false);
335
  bool simpcache_stats = false;
336
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
337
  bool symbolic_scc_pruning = false;
338
  bool display_reduced_form = false;
339
  bool post_branching = false;
340
  bool fair_loop_approx = false;
341
  bool graph_run_opt = false;
342
  bool graph_run_tgba_opt = false;
343
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
344
  bool opt_minimize = false;
345
  bool opt_bisim_ta = false;
346
  bool opt_monitor = false;
347
  bool containment = false;
348
  bool show_fc = false;
349
  bool spin_comments = false;
350
351
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
352
  spot::tgba* system = 0;
353
354
  const spot::tgba* product = 0;
  const spot::tgba* product_to_free = 0;
355
  spot::bdd_dict* dict = new spot::bdd_dict();
356
357
  spot::timer_map tm;
  bool use_timer = false;
358
  bool assume_sba = false;
Thomas Badie's avatar
Thomas Badie committed
359
  bool reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
360
  bool reduction_rev_sim = false;
361
  bool reduction_iterated_sim = false;
Thomas Badie's avatar
Thomas Badie committed
362
  spot::tgba* temp_dir_sim = 0;
363
  bool ta_opt = false;
364
  bool tgta_opt = false;
365
  bool opt_with_artificial_initial_state = true;
366
367
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
Thomas Badie's avatar
Thomas Badie committed
368
  spot::tgba* temp_rev_sim = 0;
369
370
  spot::tgba* temp_iterated_sim = 0;

371

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

      ++formula_index;

379
380
381
382
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
383
384
385
386
387
      else if (!strcmp(argv[formula_index], "-8"))
	{
	  utf8_opt = true;
	  spot::enable_utf8();
	}
388
      else if (!strcmp(argv[formula_index], "-a"))
389
390
391
	{
	  output = 2;
	}
392
      else if (!strcmp(argv[formula_index], "-A"))
393
	{
394
	  output = 4;
395
	}
396
      else if (!strcmp(argv[formula_index], "-b"))
397
	{
398
	  output = 7;
399
	}
400
401
402
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
403
	  translation = TransTAA;
404
	}
405
406
407
408
409
410
411
412
413
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
414
      else if (!strcmp(argv[formula_index], "-d"))
415
416
417
	{
	  debug_opt = true;
	}
418
419
      else if (!strcmp(argv[formula_index], "-D"))
	{
420
421
422
423
424
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
425
	}
426
      else if (!strncmp(argv[formula_index], "-e", 2))
427
        {
428
429
430
431
432
433
434
435
436
437
438
439
440
	  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 `"
			<< err <<  "'" << std::endl;
	      exit(2);
	    }
441
442
443
          expect_counter_example = true;
          output = -1;
        }
444
      else if (!strncmp(argv[formula_index], "-E", 2))
445
        {
446
447
448
449
450
451
452
453
454
455
456
457
458
	  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 `"
			<< err <<  "'" << std::endl;
	      exit(2);
	    }
459
460
461
          expect_counter_example = false;
          output = -1;
        }
462
463
      else if (!strcmp(argv[formula_index], "-f"))
	{
464
	  translation = TransFM;
465
	}
466
      else if (!strcmp(argv[formula_index], "-fr"))
467
	{
468
	  fm_red = true;
469
	  translation = TransFM;
470
	}
471
472
473
474
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
475
476
477
478
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
479
480
      else if (!strcmp(argv[formula_index], "-g"))
	{
481
	  accepting_run = true;
482
483
	  graph_run_opt = true;
	}
484
485
      else if (!strcmp(argv[formula_index], "-G"))
	{
486
	  accepting_run = true;
487
488
	  graph_run_tgba_opt = true;
	}
489
490
491
492
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
493
494
495
496
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
497
498
499
500
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
501
502
503
504
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
505
506
507
508
509
510
511
512
513
514
515
516
      else if (!strncmp(argv[formula_index], "-KP", 3))
	{
	  tm.start("reading -KP's argument");

	  spot::kripke_parse_error_list pel;
	  system = spot::kripke_parse(argv[formula_index] + 3,
				      pel, dict, env, debug_opt);
	  if (spot::format_kripke_parse_errors(std::cerr,
					       argv[formula_index] + 2, pel))
	    return 2;
	  tm.stop("reading -KP's argument");
	}
517
518
519
520
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
521
522
523
524
      else if (!strcmp(argv[formula_index], "-l"))
	{
	  translation = TransLaCIM;
	}
525
526
527
528
529
530
531
532
533
534
      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;
	}
535
536
537
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
538
	  translation = TransFM;
539
	}
540
541
542
543
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
544
545
      else if (!strcmp(argv[formula_index], "-m"))
	{
546
	  opt_reduce = true;
547
	}
martinez's avatar
martinez committed
548
549
      else if (!strcmp(argv[formula_index], "-N"))
	{
550
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
551
552
	  output = 8;
	}
553
554
555
556
557
558
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
	  spin_comments = true;
	}
559
560
      else if (!strcmp(argv[formula_index], "-O"))
	{
561
	  output = 14;
562
          opt_minimize = true;
563
	}
564
565
566
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
567
	  translation = TransFM;
568
	}
569
570
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
571
572
	  tm.start("reading -P's argument");

573
	  spot::tgba_parse_error_list pel;
574
575
576
	  spot::tgba_explicit_string* s;
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, env, debug_opt);
577
578
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
579
	    return 2;
580
	  s->merge_transitions();
581
	  tm.stop("reading -P's argument");
582
	  system = s;
583
	}
584
585
      else if (!strcmp(argv[formula_index], "-r"))
	{
586
587
	  output = 1;
	}
588
589
      else if (!strcmp(argv[formula_index], "-r1"))
	{
590
591
	  simpltl = true;
	  redopt.reduce_basics = true;
592
593
594
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
595
596
	  simpltl = true;
	  redopt.event_univ = true;
597
598
599
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
600
601
	  simpltl = true;
	  redopt.synt_impl = true;
602
603
604
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
605
606
607
608
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
609
	}
610
611
      else if (!strcmp(argv[formula_index], "-r5"))
	{
612
613
	  simpltl = true;
	  redopt.containment_checks = true;
614
615
616
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
617
618
619
	  simpltl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
620
621
622
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
623
624
625
626
627
628
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.event_univ = true;
	  redopt.synt_impl = true;
	  redopt.containment_checks = true;
	  redopt.containment_checks_stronger = true;
629
	}
630
631
632
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
633
	}
634
635
636
637
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
638
	{
639
	  // For backward compatibility, make all these options
640
	  // equal to -RDS.
641
	  reduction_dir_sim = true;
642
	}
Thomas Badie's avatar
Thomas Badie committed
643
644
645
646
      else if (!strcmp(argv[formula_index], "-RRS"))
        {
          reduction_rev_sim = true;
        }
647
648
      else if (!strcmp(argv[formula_index], "-R3"))
	{
649
	  scc_filter = true;
650
	}
651
652
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
653
	  scc_filter = true;
654
655
	  scc_filter_all = true;
	}
656
657
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
658
	  symbolic_scc_pruning = true;
659
	}
660
661
      else if (!strcmp(argv[formula_index], "-rd"))
	{
662
	  display_reduced_form = true;
663
	}
664
665
666
667
      else if (!strcmp(argv[formula_index], "-rD"))
	{
	  simpcache_stats = true;
	}
668
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
669
        {
670
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
671
        }
672
673
674
675
      else if (!strcmp(argv[formula_index], "-RIS"))
        {
          reduction_iterated_sim = true;
        }
676
      else if (!strcmp(argv[formula_index], "-rL"))
677
678
679
680
681
        {
	  simpltl = true;
	  redopt.reduce_basics = true;
	  redopt.reduce_size_strictly = true;
        }
682
683
684
685
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
686
687
688
689
      else if (!strcmp(argv[formula_index], "-RT"))
        {
          opt_bisim_ta = true;
        }
690
691
692
693
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
694
695
696
697
698
699
700
701
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
702
703
704
705
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
706
707
708
709
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
710
711
712
713
      else if (!strcmp(argv[formula_index], "-TA"))
        {
          ta_opt = true;
        }
714
      else if (!strcmp(argv[formula_index], "-TGTA"))
715
        {
716
          tgta_opt = true;
717
        }
718
719
720
721
      else if (!strcmp(argv[formula_index], "-lv"))
        {
          opt_with_artificial_livelock = true;
        }
722
723
724
725
      else if (!strcmp(argv[formula_index], "-sp"))
        {
          opt_single_pass_emptiness_check = true;
        }
726
727
728
729
      else if (!strcmp(argv[formula_index], "-in"))
        {
          opt_with_artificial_initial_state = false;
        }
730
731
732
733
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
734
735
736
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
737
	  translation = TransFM;
738
	  // Parse -U's argument.
739
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
740
741
742
	  while (tok)
	    {
	      unobservables->insert
743
		(static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
744
	      tok = strtok(0, ", \t;");
745
746
	    }
	}
747
748
749
750
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
751
752
      else if (!strcmp(argv[formula_index], "-x"))
	{
753
	  translation = TransFM;
754
755
	  fm_exprop_opt = true;
	}
756
757
758
759
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
760
761
762
763
764
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  read_neverclaim = true;
	}
765
766
      else if (!strcmp(argv[formula_index], "-y"))
	{
767
	  translation = TransFM;
768
769
	  fm_symb_merge_opt = false;
	}
770
771
772
773
      else
	{
	  break;
	}
774
775
    }

776
  if ((graph_run_opt || graph_run_tgba_opt)
777
      && (!echeck_inst || !expect_counter_example))
778
    {
779
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
780
781
782
      exit(1);
    }

783
784
785
786
  std::string input;

  if (file_opt)
    {
787
      tm.start("reading formula");
788
      if (strcmp(argv[formula_index], "-"))
789
	{
790
	  std::ifstream fin(argv[formula_index]);
791
	  if (!fin)
792
793
794
795
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
796

797
	  if (!std::getline(fin, input, '\0'))
798
799
800
801
802
803
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
804
	{
805
	  std::getline(std::cin, input, '\0');
806
	}
807
      tm.stop("reading formula");
808
809
810
811
812
813
    }
  else
    {
      input = argv[formula_index];
    }

814
  const spot::ltl::formula* f = 0;
815
  if (!from_file) // Reading a formula, not reading an automaton from a file.
816
    {
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
      switch (translation)
	{
	case TransFM:
	case TransLaCIM:
	case TransTAA:
	  {
	    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;
	case TransLaCIM_ELTL:
	  {
	    spot::eltl::parse_error_list p;
	    tm.start("parsing formula");
	    f = spot::eltl::parse_string(input, p, env, false);
	    tm.stop("parsing formula");
	    exit_code = spot::eltl::format_parse_errors(std::cerr, p);
	  }
	  break;
	case TransLaCIM_ELTL_ops:
	  {
	    // Call the LTL parser first to handle operators such as
	    // [] or <> and rewrite the output as a string with G or F.
	    // Then prepend definitions of usual LTL operators, and parse
	    // the result again as an ELTL formula.
	    spot::ltl::parse_error_list pel;
	    tm.start("parsing formula");
	    f = spot::ltl::parse(input, pel, env, debug_opt);
	    input = ltl_defs();
	    input += "%";
	    input += spot::ltl::to_string(f, true);
	    f->destroy();
	    spot::eltl::parse_error_list p;
	    f = spot::eltl::parse_string(input, p, env, debug_opt);
	    tm.stop("parsing formula");
	    exit_code = spot::eltl::format_parse_errors(std::cerr, p);
	  }
	  break;
858
	}
859
    }
860

861
  if (f || from_file)
862
    {
863
      spot::tgba_bdd_concrete* concrete = 0;
864
      const spot::tgba* to_free = 0;
865
      const spot::tgba* to_free2 = 0;
866
      spot::tgba* a = 0;
867

868
869
      if (from_file)
	{
870
	  spot::tgba_explicit_string* e;
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
	  if (!read_neverclaim)
	    {
	      spot::tgba_parse_error_list pel;
	      tm.start("parsing automaton");
	      to_free = a = e = spot::tgba_parse(input, pel, dict,
						 env, env, debug_opt);
	      tm.stop("parsing automaton");
	      if (spot::format_tgba_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
		}
	    }
	  else
886
	    {
887
	      spot::neverclaim_parse_error_list pel;
888
	      tm.start("parsing neverclaim");
889
890
	      to_free = a = e = spot::neverclaim_parse(input, pel, dict,
						       env, debug_opt);
891
	      tm.stop("parsing neverclaim");
892
893
894
895
896
	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
897
		}
898
	      assume_sba = true;
899
	    }
900
	  e->merge_transitions();
901
	}
902
      else
903
	{
904
905
	  spot::ltl::ltl_simplifier* simp = 0;
	  if (simpltl)
906
	    simp = new spot::ltl::ltl_simplifier(redopt, dict);
907
908

	  if (simp)
909
	    {
910
	      tm.start("reducing formula");
911
	      const spot::ltl::formula* t = simp->simplify(f);
912
	      f->destroy();
913
	      tm.stop("reducing formula");
914
	      f = t;
915
916
917
918
919
920
921
	      if (display_reduced_form)
		{
		  if (utf8_opt)
		    std::cout << spot::ltl::to_utf8_string(f) << std::endl;
		  else
		    std::cout << spot::ltl::to_string(f) << std::endl;
		}
922
923
924
	      // This helps ltl_to_tgba_fm() to order BDD variables in
	      // a more natural way.
	      simp->clear_as_bdd_cache();
925
	    }
926

927
928
929
930
931
932
933
934
935
	  if (f->is_psl_formula()
	      && !f->is_ltl_formula()
	      && translation != TransFM)
	    {
	      std::cerr << "Only the FM algorithm can translate PSL formulae;"
			<< " I'm using it for this formula." << std::endl;
	      translation = TransFM;
	    }

936
	  tm.start("translating formula");
937
938
939
940
941
942
943
944
	  switch (translation)
	    {
	    case TransFM:
	      a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
				       fm_symb_merge_opt,
				       post_branching,
				       fair_loop_approx,
				       unobservables,
945
				       fm_red ? simp : 0);
946
947
948
949
950
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
951
952
953
954
955
	      a = concrete = spot::ltl_to_tgba_lacim(f, dict);
	      break;
	    case TransLaCIM_ELTL:
	    case TransLaCIM_ELTL_ops:
	      a = concrete = spot::eltl_to_tgba_lacim(f, dict);
956
957
	      break;
	    }
958
	  tm.stop("translating formula");
959
	  to_free = a;
960

961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
	  if (simp && simpcache_stats)
	    {
	      simp->print_stats(std::cerr);
	      bddStat s;
	      bdd_stats(&s);
	      std::cerr << "BDD produced: " << s.produced
			<< "\n    nodenum: " << s.nodenum
			<< "\n    maxnodenum: " << s.maxnodenum
			<< "\n    freenodes: " <<  s.freenodes
			<< "\n    minfreenodes: " << s.minfreenodes
			<< "\n    varnum: " <<  s.varnum
			<< "\n    cachesize: " << s.cachesize
			<< "\n    gbcnum: " << s.gbcnum
			<< std::endl;
	      bdd_fprintstat(stderr);
	      dict->dump(std::cerr);
	    }
978
	  delete simp;
979
	}
980

981
      if (opt_monitor && !scc_filter)
982
	{
983
	  if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
984
985
	    symbolic_scc_pruning = true;
	  else
986
	    scc_filter = true;
987
988
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
989
990
      if (symbolic_scc_pruning)
        {
991
992
	  const spot::tgba_bdd_concrete* bc =
	    dynamic_cast<const spot::tgba_bdd_concrete*>(a);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
993
994
995
996
997
998
999
1000
1001
1002
1003