ltl2tgba.cc 38.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/contain.hh"
32
#include "ltlvisit/tostring.hh"
33
#include "ltlvisit/apcollect.hh"
34
#include "ltlast/allnodes.hh"
35
#include "ltlparse/public.hh"
36
#include "tgbaalgos/ltl2tgba_lacim.hh"
37
#include "tgbaalgos/ltl2tgba_fm.hh"
38
#include "tgbaalgos/ltl2taa.hh"
39
#include "tgba/bddprint.hh"
40
#include "tgbaalgos/save.hh"
41
#include "tgbaalgos/dotty.hh"
42
#include "tgbaalgos/lbtt.hh"
43
#include "tgba/tgbatba.hh"
44
#include "tgba/tgbasgba.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 "tgbaalgos/neverclaim.hh"
53
#include "tgbaalgos/replayrun.hh"
54
#include "tgbaalgos/rundotdec.hh"
55
#include "tgbaalgos/sccfilter.hh"
56
#include "tgbaalgos/safety.hh"
57
#include "tgbaalgos/eltl2tgba_lacim.hh"
58
#include "tgbaalgos/gtec/gtec.hh"
59
#include "eltlparse/public.hh"
60
#include "misc/timer.hh"
61
#include "tgbaalgos/stats.hh"
62
#include "tgbaalgos/scc.hh"
63
#include "tgbaalgos/emptiness_stats.hh"
64
65
#include "tgbaalgos/scc.hh"
#include "kripkeparse/public.hh"
Thomas Badie's avatar
Thomas Badie committed
66
#include "tgbaalgos/simulation.hh"
67

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

86
87
88
void
syntax(char* prog)
{
89
90
91
92
93
  // 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;

94
  std::cerr << "Usage: "<< prog << " [-f|-l|-le|-taa] [OPTIONS...] formula"
95
	    << std::endl
96
            << "       "<< prog << " [-f|-l|-le|-taa] -F [OPTIONS...] file"
97
	    << std::endl
98
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
99
	    << std::endl
100

101
102
            << "Translate an LTL formula into an automaton, or read the "
	    << "automaton from a file." << std::endl
103
104
105
106
	    << "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
107
	    << std::endl
108
109
110

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

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

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
135
136
137
138
	    << "  -fr1  use -r1 (see below) at each step of FM" << std::endl
	    << "  -fr2  use -r2 (see below) at each step of FM" << std::endl
	    << "  -fr3  use -r3 (see below) at each step of FM" << std::endl
	    << "  -fr4  use -r4 (see below) at each step of FM" << std::endl
139
140
141
	    << "  -fr5  use -r5 (see below) at each step of FM" << std::endl
	    << "  -fr6  use -r6 (see below) at each step of FM" << std::endl
	    << "  -fr7  use -r7 (see below) at each step of FM" << std::endl
142
143
144
145
146
            << "  -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)"
147
	    << std::endl
148
149
150
151
            << "  -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
152
	    << std::endl
153

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

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

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

	    << "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
199
	    << "  -R3   use SCC to reduce the automata" << std::endl
200
	    << "  -R3f  clean more acceptance conditions than -R3" << std::endl
201
202
203
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
204
205
206
	    << "  -RDS  minimize the automaton with direct simulation"
	    << std::endl
            << "  -Rm   attempt to WDBA-minimize the automata" << std::endl
207
	    << std::endl
208

209
            << "Automaton conversion:" << std::endl
210
211
            << "  -M    convert into a deterministic minimal monitor "
	    << "(implies -R3 or R3b)" << std::endl
212
213
214
215
	    << "  -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
216
217
	    << std::endl

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

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

288
  bool debug_opt = false;
289
  bool paper_opt = false;
290
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
291
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
292
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
293
    translation = TransFM;
294
  int fm_red = spot::ltl::Reduce_None;
295
  bool fm_exprop_opt = false;
296
  bool fm_symb_merge_opt = true;
297
  bool file_opt = false;
298
  int output = 0;
299
  int formula_index = 0;
300
301
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
302
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
303
  bool expect_counter_example = false;
304
305
  bool accepting_run = false;
  bool accepting_run_replay = false;
306
  bool from_file = false;
307
  bool read_neverclaim = false;
308
  int redopt = spot::ltl::Reduce_None;
309
  bool scc_filter = false;
310
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
311
  bool symbolic_scc_pruning = false;
312
  bool display_reduce_form = false;
313
  bool post_branching = false;
314
  bool fair_loop_approx = false;
315
  bool graph_run_opt = false;
316
  bool graph_run_tgba_opt = false;
317
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
318
  bool opt_minimize = false;
319
  bool opt_monitor = false;
320
  bool containment = false;
321
  bool show_fc = false;
322
  bool spin_comments = false;
323
324
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
325
  spot::tgba* system = 0;
326
327
  const spot::tgba* product = 0;
  const spot::tgba* product_to_free = 0;
328
  spot::bdd_dict* dict = new spot::bdd_dict();
329
330
  spot::timer_map tm;
  bool use_timer = false;
331
  bool assume_sba = false;
Thomas Badie's avatar
Thomas Badie committed
332
333
334
  bool reduction_dir_sim = false;
  spot::tgba* temp_dir_sim = 0;

335

336
  for (;;)
337
    {
338
      if (argc < formula_index + 2)
339
	syntax(argv[0]);
340
341
342

      ++formula_index;

343
344
345
346
347
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
348
349
350
	{
	  output = 2;
	}
351
      else if (!strcmp(argv[formula_index], "-A"))
352
	{
353
	  output = 4;
354
	}
355
      else if (!strcmp(argv[formula_index], "-b"))
356
	{
357
	  output = 7;
358
	}
359
360
361
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
362
	  translation = TransTAA;
363
	}
364
365
366
367
368
369
370
371
372
      else if (!strcmp(argv[formula_index], "-C"))
	{
	  accepting_run = true;
	}
      else if (!strcmp(argv[formula_index], "-CR"))
	{
	  accepting_run = true;
	  accepting_run_replay = true;
	}
373
      else if (!strcmp(argv[formula_index], "-d"))
374
375
376
	{
	  debug_opt = true;
	}
377
378
      else if (!strcmp(argv[formula_index], "-D"))
	{
379
380
381
382
383
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
384
	}
385
      else if (!strncmp(argv[formula_index], "-e", 2))
386
        {
387
388
389
390
391
392
393
394
395
396
397
398
399
	  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);
	    }
400
401
402
          expect_counter_example = true;
          output = -1;
        }
403
      else if (!strncmp(argv[formula_index], "-E", 2))
404
        {
405
406
407
408
409
410
411
412
413
414
415
416
417
	  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);
	    }
418
419
420
          expect_counter_example = false;
          output = -1;
        }
421
422
      else if (!strcmp(argv[formula_index], "-f"))
	{
423
	  translation = TransFM;
424
	}
425
426
      else if (!strcmp(argv[formula_index], "-fr1"))
	{
427
	  translation = TransFM;
428
429
430
431
	  fm_red |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-fr2"))
	{
432
	  translation = TransFM;
433
434
435
436
	  fm_red |= spot::ltl::Reduce_Eventuality_And_Universality;
	}
      else if (!strcmp(argv[formula_index], "-fr3"))
	{
437
	  translation = TransFM;
438
439
440
	  fm_red |= spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr4"))
441
	{
442
	  translation = TransFM;
443
444
445
446
447
448
 	  fm_red |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr5"))
	{
449
	  translation = TransFM;
450
451
452
453
	  fm_red |= spot::ltl::Reduce_Containment_Checks;
	}
      else if (!strcmp(argv[formula_index], "-fr6"))
	{
454
	  translation = TransFM;
455
456
457
	  fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger;
	}
      else if (!strcmp(argv[formula_index], "-fr7"))
458
	{
459
	  translation = TransFM;
460
461
	  fm_red |= spot::ltl::Reduce_All;
	}
462
463
464
465
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
466
467
468
469
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
470
471
      else if (!strcmp(argv[formula_index], "-g"))
	{
472
	  accepting_run = true;
473
474
	  graph_run_opt = true;
	}
475
476
      else if (!strcmp(argv[formula_index], "-G"))
	{
477
	  accepting_run = true;
478
479
	  graph_run_tgba_opt = true;
	}
480
481
482
483
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
484
485
486
487
      else if (!strcmp(argv[formula_index], "-ks"))
	{
	  output = 12;
	}
488
489
490
491
      else if (!strcmp(argv[formula_index], "-kt"))
	{
	  output = 13;
	}
492
493
494
495
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
496
497
498
499
500
501
502
503
504
505
506
507
      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");
	}
508
509
510
511
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
512
513
514
515
      else if (!strcmp(argv[formula_index], "-l"))
	{
	  translation = TransLaCIM;
	}
516
517
518
519
520
521
522
523
524
525
      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;
	}
526
527
528
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
529
	  translation = TransFM;
530
	}
531
532
533
534
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
535
536
      else if (!strcmp(argv[formula_index], "-m"))
	{
537
	  opt_reduce = true;
538
	}
martinez's avatar
martinez committed
539
540
      else if (!strcmp(argv[formula_index], "-N"))
	{
541
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
542
543
	  output = 8;
	}
544
545
546
547
548
549
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
	  spin_comments = true;
	}
550
551
      else if (!strcmp(argv[formula_index], "-O"))
	{
552
	  output = 14;
553
          opt_minimize = true;
554
	}
555
556
557
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
558
	  translation = TransFM;
559
	}
560
561
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
562
563
	  tm.start("reading -P's argument");

564
	  spot::tgba_parse_error_list pel;
565
566
567
	  spot::tgba_explicit_string* s;
	  s = spot::tgba_parse(argv[formula_index] + 2,
			       pel, dict, env, env, debug_opt);
568
569
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
570
	    return 2;
571
	  s->merge_transitions();
572
	  tm.stop("reading -P's argument");
573
	  system = s;
574
	}
575
576
      else if (!strcmp(argv[formula_index], "-r"))
	{
577
578
	  output = 1;
	}
579
580
581
582
583
584
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
585
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
586
587
588
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
589
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
590
591
592
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
593
594
595
 	  redopt |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
596
	}
597
598
      else if (!strcmp(argv[formula_index], "-r5"))
	{
599
	  redopt |= spot::ltl::Reduce_Containment_Checks;
600
601
602
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
603
	  redopt |= spot::ltl::Reduce_Containment_Checks_Stronger;
604
605
606
607
608
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
609
610
611
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
612
	}
613
614
615
616
      else if (!strcmp(argv[formula_index], "-R1q")
	       || !strcmp(argv[formula_index], "-R1t")
	       || !strcmp(argv[formula_index], "-R2q")
	       || !strcmp(argv[formula_index], "-R2t"))
617
	{
618
	  // For backward compatibility, make all these options
619
	  // equal to -RDS.
620
	  reduction_dir_sim = true;
621
622
623
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
624
	  scc_filter = true;
625
	}
626
627
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
628
	  scc_filter = true;
629
630
	  scc_filter_all = true;
	}
631
632
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
633
	  symbolic_scc_pruning = true;
634
	}
635
636
637
638
      else if (!strcmp(argv[formula_index], "-rd"))
	{
	  display_reduce_form = true;
	}
639
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
640
        {
641
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
642
        }
643
      else if (!strcmp(argv[formula_index], "-Rm"))
644
        {
645
          opt_minimize = true;
646
        }
647
648
649
650
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
651
652
653
654
655
656
657
658
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
659
660
661
662
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
663
664
665
666
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
667
668
669
670
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
671
672
673
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
674
	  translation = TransFM;
675
	  // Parse -U's argument.
676
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
677
678
679
680
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
681
	      tok = strtok(0, ", \t;");
682
683
	    }
	}
684
685
686
687
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
688
689
      else if (!strcmp(argv[formula_index], "-x"))
	{
690
	  translation = TransFM;
691
692
	  fm_exprop_opt = true;
	}
693
694
695
696
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
697
698
699
700
701
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  read_neverclaim = true;
	}
702
703
      else if (!strcmp(argv[formula_index], "-y"))
	{
704
	  translation = TransFM;
705
706
	  fm_symb_merge_opt = false;
	}
707
708
709
710
      else
	{
	  break;
	}
711
712
    }

713
  if ((graph_run_opt || graph_run_tgba_opt)
714
      && (!echeck_inst || !expect_counter_example))
715
    {
716
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
717
718
719
      exit(1);
    }

720
721
722
723
  std::string input;

  if (file_opt)
    {
724
      tm.start("reading formula");
725
      if (strcmp(argv[formula_index], "-"))
726
	{
727
	  std::ifstream fin(argv[formula_index]);
728
	  if (!fin)
729
730
731
732
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
733

734
	  if (!std::getline(fin, input, '\0'))
735
736
737
738
739
740
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
741
	{
742
	  std::getline(std::cin, input, '\0');
743
	}
744
      tm.stop("reading formula");
745
746
747
748
749
750
    }
  else
    {
      input = argv[formula_index];
    }

751
  spot::ltl::formula* f = 0;
752
  if (!from_file) // Reading a formula, not reading an automaton from a file.
753
    {
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
      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;
795
	}
796
797
    }
  if (f || from_file)
798
    {
799
800
801
      const spot::tgba_bdd_concrete* concrete = 0;
      const spot::tgba* to_free = 0;
      const spot::tgba* a = 0;
802

803
804
      if (from_file)
	{
805
	  spot::tgba_explicit_string* e;
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
	  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
821
	    {
822
	      spot::neverclaim_parse_error_list pel;
823
	      tm.start("parsing neverclaim");
824
825
	      to_free = a = e = spot::neverclaim_parse(input, pel, dict,
						       env, debug_opt);
826
	      tm.stop("parsing neverclaim");
827
828
829
830
831
	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
832
		}
833
	    }
834
	  e->merge_transitions();
835
	}
836
      else
837
	{
838
	  if (redopt != spot::ltl::Reduce_None)
839
	    {
840
	      tm.start("reducing formula");
841
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
842
	      f->destroy();
843
	      tm.stop("reducing formula");
844
	      f = t;
845
846
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
847
	    }
848

849
	  tm.start("translating formula");
850
851
852
853
854
855
856
857
	  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,
858
				       fm_red);
859
860
861
862
863
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
864
865
866
867
868
	      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);
869
870
	      break;
	    }
871
	  tm.stop("translating formula");
872
	  to_free = a;
873
	}
874

875
      if (opt_monitor && !scc_filter)
876
	{
877
	  if (dynamic_cast<const spot::tgba_bdd_concrete*>(a))
878
879
	    symbolic_scc_pruning = true;
	  else
880
	    scc_filter = true;
881
882
	}

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
883
884
      if (symbolic_scc_pruning)
        {
885
886
	  const spot::tgba_bdd_concrete* bc =
	    dynamic_cast<const spot::tgba_bdd_concrete*>(a);
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
887
888
889
890
891
892
893
894
895
896
897
898
899
	  if (!bc)
	    {
	      std::cerr << ("Error: Automaton is not symbolic: cannot "
			    "prune SCCs symbolically.\n"
			    "       Try -R3 instead of -R3b, or use "
			    "another translation.")
			<< std::endl;
	      exit(2);
	    }
	  else
	    {
	      tm.start("reducing A_f w/ symbolic SCC pruning");
	      if (bc)
900
901
		const_cast<spot::tgba_bdd_concrete*>(bc)
		  ->delete_unaccepting_scc();
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
902
903
904
905
	      tm.stop("reducing A_f w/ symbolic SCC pruning");
	    }
	}

906
907
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.
908
      const spot::tgba* aut_scc = 0;
909
      if (scc_filter)
910
911
	{
	  tm.start("reducing A_f w/ SCC");
912
	  a = aut_scc = spot::scc_filter(a, scc_filter_all);
913
914
915
	  tm.stop("reducing A_f w/ SCC");
	}

916
917
      const spot::tgba_tba_proxy* degeneralized = 0;
      const spot::tgba_sgba_proxy* state_labeled = 0;
918

919
      const spot::tgba* minimized = 0;
Felix Abecassis's avatar
Felix Abecassis committed
920
      if (opt_minimize)
921
	{
922
923
924
925
926
	  tm.start("obligation minimization");
	  minimized = minimize_obligation(a, f);
	  tm.stop("obligation minimization");

	  if (minimized == 0)
927
	    {
928
	      // if (!f)
929
930
931
932
933
934
		{
		  std::cerr << "Error: Without a formula I cannot make "
			    << "sure that the automaton built with -Rm\n"
			    << "       is correct." << std::endl;
		  exit(2);
		}
935
	    }
936
937
938
939
940
941
942
	  else if (minimized == a)
	    {
	      minimized = 0;
	    }
	  else
	    {
	      a = minimized;
Thomas Badie's avatar
Thomas Badie committed
943
944
              // When the minimization succeed, simulation is useless.
              reduction_dir_sim = false;
945
	      assume_sba = true;
946
	    }
947
	}
Felix Abecassis's avatar
Felix Abecassis committed
948

Thomas Badie's avatar
Thomas Badie committed
949
950
951
952
953
954
955
956
957
958

      if (reduction_dir_sim)
        {
          tm.start("Reduction w/ direct simulation");
          temp_dir_sim = spot::simulation(a);
          a = temp_dir_sim;
          tm.stop("Reduction w/ direct simulation");
        }


959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
	  && degeneralize_opt == NoDegen
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
	{
	  degeneralize_opt = DegenTBA;
	  assume_sba = false;
	}

      if (!assume_sba && !opt_monitor)
	{
	  if (degeneralize_opt == DegenTBA)
	    {
	      a = degeneralized = new spot::tgba_tba_proxy(a);
	    }
	  else if (degeneralize_opt == DegenSBA)
	    {
	      a = degeneralized = new spot::tgba_sba_proxy(a);
	      assume_sba = true;
	    }
	  else if (labeling_opt == StateLabeled)
	    {
	      a = state_labeled = new spot::tgba_sgba_proxy(a);
	    }
	}

986
987
988
      if (opt_monitor)
	{
	  tm.start("Monitor minimization");
989
	  a = minimized = minimize_monitor(a);
990
	  tm.stop("Monitor minimization");
991
992
993
	  assume_sba = false; 	// All states are accepting, so double
				// circles in the dot output are
				// pointless.
994
995
	}

Pierre PARUTTO's avatar
Pierre PARUTTO committed
996
      const spot::tgba_explicit_string* expl = 0;
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
      switch (dupexp)
	{
	case NoneDup:
	  break;
	case BFS:
	  a = expl = tgba_dupexp_bfs(a);
	  break;
	case DFS:
	  a = expl = tgba_dupexp_dfs(a);
	  break;
	}

1009
      const spot::tgba* product_degeneralized = 0;
1010

1011
      if (system)
1012
1013
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
1014

1015
1016
	  assume_sba = false;

1017
1018
1019
1020
1021
	  unsigned int n_acc = a->number_of_acceptance_conditions();
	  if (echeck_inst
	      && degeneralize_opt == NoDegen
	      && n_acc > 1
	      && echeck_inst->max_acceptance_conditions() < n_acc)
1022
1023
            degeneralize_opt = DegenTBA;
          if (degeneralize_opt == DegenTBA)
1024
1025
1026
1027
	    {
	      a = product = product_degeneralized =
		new spot::tgba_tba_proxy(product);
	    }
1028
          else if (degeneralize_opt == DegenSBA)