ltl2tgba.cc 35.6 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
2
// Copyright (C) 2007, 2008, 2009, 2010 Laboratoire de Recherche et
// Dveloppement de l'Epita (LRDE).
Guillaume Sadegh's avatar
Guillaume Sadegh committed
3
4
// Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), dpartement Systmes Rpartis
5
// Coopratifs (SRC), Universit Pierre et Marie Curie.
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
//
// 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.

24
#include <iostream>
25
#include <iomanip>
26
#include <cassert>
27
28
#include <fstream>
#include <string>
29
#include <cstdlib>
30
#include "ltlvisit/contain.hh"
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 "tgba/tgbaproduct.hh"
45
#include "tgba/futurecondcol.hh"
46
#include "tgbaalgos/reducerun.hh"
47
#include "tgbaparse/public.hh"
48
#include "neverparse/public.hh"
49
#include "tgbaalgos/dupexp.hh"
50
#include "tgbaalgos/neverclaim.hh"
51
#include "tgbaalgos/reductgba_sim.hh"
52
#include "tgbaalgos/replayrun.hh"
53
#include "tgbaalgos/rundotdec.hh"
54
#include "tgbaalgos/sccfilter.hh"
55
56
#include "tgbaalgos/eltl2tgba_lacim.hh"
#include "eltlparse/public.hh"
57
#include "misc/timer.hh"
58

59
#include "tgbaalgos/stats.hh"
60
#include "tgbaalgos/scc.hh"
61
62
#include "tgbaalgos/emptiness_stats.hh"

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

81
82
83
void
syntax(char* prog)
{
84
85
86
87
88
  // 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;

89
  std::cerr << "Usage: "<< prog << " [-f|-l|-le|-taa] [OPTIONS...] formula"
90
	    << std::endl
91
            << "       "<< prog << " [-f|-l|-le|-taa] -F [OPTIONS...] file"
92
	    << std::endl
93
            << "       "<< prog << " -X [OPTIONS...] file" << std::endl
Alexandre Duret-Lutz's avatar
spacing    
Alexandre Duret-Lutz committed
94
	    << std::endl
95

96
97
            << "Translate an LTL formula into an automaton, or read the "
	    << "automaton from a file." << std::endl
98
99
100
101
	    << "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
102
	    << std::endl
103
104
105

            << "Input options:" << std::endl
            << "  -F    read the formula from a file, not from the command line"
106
	    << std::endl
107
	    << "  -X    do not compute an automaton, read it from a file"
108
	    << std::endl
109
110
	    << "  -XN   do not compute an automaton, read it from a"
	    << " neverclaim file" << std::endl
111
112
	    << "  -Pfile  multiply the formula automaton with the automaton"
	    << " from `file'"
113
	    << std::endl
114
115
116
	    << std::endl

	    << "Translation algorithm:" << std::endl
117
            << "  -f    use Couvreur's FM algorithm for LTL"
118
	    << "(default)"
119
	    << std::endl
120
            << "  -l    use Couvreur's LaCIM algorithm for LTL "
121
	    << std::endl
122
123
124
	    << "  -le   use Couvreur's LaCIM algorithm for ELTL"
	    << std::endl
            << "  -taa  use Tauriainen's TAA-based algorithm for LTL"
martinez's avatar
martinez committed
125
	    << std::endl
126
127
128
	    << std::endl

	    << "Options for Couvreur's FM algorithm (-f):" << std::endl
129
130
131
132
	    << "  -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
133
134
135
	    << "  -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
136
137
138
139
140
            << "  -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)"
141
	    << std::endl
142
143
144
145
            << "  -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
146
	    << std::endl
147

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

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

	    << "Formula simplification (before translation):"
170
	    << std::endl
martinez's avatar
martinez committed
171
172
	    << "  -r1   reduce formula using basic rewriting" << std::endl
	    << "  -r2   reduce formula using class of eventuality and "
173
	    << "universality" << std::endl
martinez's avatar
martinez committed
174
	    << "  -r3   reduce formula using implication between "
175
	    << "sub-formulae" << std::endl
176
177
178
	    << "  -r4   reduce formula using all above rules" << std::endl
	    << "  -r5   reduce formula using tau03" << std::endl
	    << "  -r6   reduce formula using tau03+" << std::endl
179
	    << "  -r7   reduce formula using tau03+ and -r4" << std::endl
180
181
182
183
184
185
186
187
188
189
190
191
192
193
	    << "  -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
194
	    << "  -R1q  merge states using direct simulation "
martinez's avatar
martinez committed
195
	    << "(use -L for more reduction)"
196
	    << std::endl
197
	    << "  -R1t  remove transitions using direct simulation "
martinez's avatar
martinez committed
198
	    << "(use -L for more reduction)"
199
	    << std::endl
200
201
	    << "  -R2q  merge states using delayed simulation" << std::endl
	    << "  -R2t  remove transitions using delayed simulation"
202
	    << std::endl
203
	    << "  -R3   use SCC to reduce the automata" << std::endl
204
205
206
207
	    << "  -R3f  clean more acceptance conditions that -R3" << std::endl
	    << "          "
	    << "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)"
	    << std::endl
208
209
	    << "  -Rd   display the simulation relation" << std::endl
	    << "  -RD   display the parity game (dot format)" << std::endl
210
	    << std::endl
211
212
213
214
215

	    << "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
216
	    << std::endl
217
	    << "  -g    graph the accepting run on the automaton (requires -e)"
218
	    << std::endl
219
220
221
	    << "  -G    graph the accepting run seen as an automaton "
	    << " (requires -e)" << std::endl
	    << "  -m    try to reduce accepting runs, in a second pass"
222
223
	    << std::endl
	    << "Where ALGO should be one of:" << std::endl
224
225
226
227
228
	    << "  Cou99(OPTIONS) (the default)" << std::endl
	    << "  CVWY90(OPTIONS)" << std::endl
	    << "  GV04(OPTIONS)" << std::endl
	    << "  SE05(OPTIONS)" << std::endl
	    << "  Tau03(OPTIONS)" << std::endl
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
	    << "  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
	    << "  -k    display statistics on the automaton of dumping it"
	    << std::endl
	    << "  -K    dump the graph of SCCs in dot format" << std::endl
	    << "  -KV   verbosely dump the graph of SCCs in dot format"
	    << std::endl
	    << "  -N    output the never clain for Spin (implies -D)"
	    << std::endl
	    << "  -NN   output the never clain for Spin, with commented states"
	    << " (implies -D)" << std::endl
	    << "  -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
	    << "  -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
            << "  -T    time the different phases of the translation"
	    << std::endl
	    << "  -v    display the BDD variables used by the automaton"
	    << std::endl;
266
267
268
269
270
271
272
273
  exit(2);
}

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

274
  bool debug_opt = false;
275
  bool paper_opt = false;
276
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
277
  enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
278
  enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
279
    translation = TransFM;
280
  int fm_red = spot::ltl::Reduce_None;
281
  bool fm_exprop_opt = false;
282
  bool fm_symb_merge_opt = true;
283
  bool file_opt = false;
284
  int output = 0;
285
  int formula_index = 0;
286
287
  const char* echeck_algo = 0;
  spot::emptiness_check_instantiator* echeck_inst = 0;
288
  enum { NoneDup, BFS, DFS } dupexp = NoneDup;
289
  bool expect_counter_example = false;
290
  bool from_file = false;
291
  bool read_neverclaim = false;
292
  int reduc_aut = spot::Reduce_None;
293
  int redopt = spot::ltl::Reduce_None;
294
  bool scc_filter_all = false;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
295
  bool symbolic_scc_pruning = false;
296
297
  bool display_reduce_form = false;
  bool display_rel_sim = false;
298
  bool display_parity_game = false;
299
  bool post_branching = false;
300
  bool fair_loop_approx = false;
301
  bool graph_run_opt = false;
302
  bool graph_run_tgba_opt = false;
303
  bool opt_reduce = false;
304
  bool containment = false;
305
  bool show_fc = false;
306
  bool spin_comments = false;
307
308
  spot::ltl::environment& env(spot::ltl::default_environment::instance());
  spot::ltl::atomic_prop_set* unobservables = 0;
309
  spot::tgba_explicit_string* system = 0;
310
  spot::tgba* product = 0;
311
  spot::tgba* product_to_free = 0;
312
  spot::bdd_dict* dict = new spot::bdd_dict();
313
314
  spot::timer_map tm;
  bool use_timer = false;
315

316
  for (;;)
317
    {
318
      if (argc < formula_index + 2)
319
	syntax(argv[0]);
320
321
322

      ++formula_index;

323
324
325
326
327
      if (!strcmp(argv[formula_index], "-0"))
	{
	  paper_opt = true;
	}
      else if (!strcmp(argv[formula_index], "-a"))
328
329
330
	{
	  output = 2;
	}
331
      else if (!strcmp(argv[formula_index], "-A"))
332
	{
333
	  output = 4;
334
	}
335
      else if (!strcmp(argv[formula_index], "-b"))
336
	{
337
	  output = 7;
338
	}
339
340
341
      else if (!strcmp(argv[formula_index], "-c"))
	{
	  containment = true;
342
	  translation = TransTAA;
343
	}
344
      else if (!strcmp(argv[formula_index], "-d"))
345
346
347
	{
	  debug_opt = true;
	}
348
349
      else if (!strcmp(argv[formula_index], "-D"))
	{
350
351
352
353
354
	  degeneralize_opt = DegenTBA;
	}
      else if (!strcmp(argv[formula_index], "-DS"))
	{
	  degeneralize_opt = DegenSBA;
355
	}
356
      else if (!strncmp(argv[formula_index], "-e", 2))
357
        {
358
359
360
361
362
363
364
365
366
367
368
369
370
	  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);
	    }
371
372
373
          expect_counter_example = true;
          output = -1;
        }
374
      else if (!strncmp(argv[formula_index], "-E", 2))
375
        {
376
377
378
379
380
381
382
383
384
385
386
387
388
	  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);
	    }
389
390
391
          expect_counter_example = false;
          output = -1;
        }
392
393
      else if (!strcmp(argv[formula_index], "-f"))
	{
394
	  translation = TransFM;
395
	}
396
397
      else if (!strcmp(argv[formula_index], "-fr1"))
	{
398
	  translation = TransFM;
399
400
401
402
	  fm_red |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-fr2"))
	{
403
	  translation = TransFM;
404
405
406
407
	  fm_red |= spot::ltl::Reduce_Eventuality_And_Universality;
	}
      else if (!strcmp(argv[formula_index], "-fr3"))
	{
408
	  translation = TransFM;
409
410
411
	  fm_red |= spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr4"))
412
	{
413
	  translation = TransFM;
414
415
416
417
418
419
 	  fm_red |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
	}
      else if (!strcmp(argv[formula_index], "-fr5"))
	{
420
	  translation = TransFM;
421
422
423
424
	  fm_red |= spot::ltl::Reduce_Containment_Checks;
	}
      else if (!strcmp(argv[formula_index], "-fr6"))
	{
425
	  translation = TransFM;
426
427
428
	  fm_red |= spot::ltl::Reduce_Containment_Checks_Stronger;
	}
      else if (!strcmp(argv[formula_index], "-fr7"))
429
	{
430
	  translation = TransFM;
431
432
	  fm_red |= spot::ltl::Reduce_All;
	}
433
434
435
436
      else if (!strcmp(argv[formula_index], "-F"))
	{
	  file_opt = true;
	}
437
438
439
440
      else if (!strcmp(argv[formula_index], "-FC"))
	{
	  show_fc = true;
	}
441
442
443
444
      else if (!strcmp(argv[formula_index], "-g"))
	{
	  graph_run_opt = true;
	}
445
446
447
448
      else if (!strcmp(argv[formula_index], "-G"))
	{
	  graph_run_tgba_opt = true;
	}
449
450
451
452
      else if (!strcmp(argv[formula_index], "-k"))
	{
	  output = 9;
	}
453
454
455
456
      else if (!strcmp(argv[formula_index], "-K"))
	{
	  output = 10;
	}
457
458
459
460
      else if (!strcmp(argv[formula_index], "-KV"))
	{
	  output = 11;
	}
461
462
463
464
      else if (!strcmp(argv[formula_index], "-l"))
	{
	  translation = TransLaCIM;
	}
465
466
467
468
469
470
471
472
473
474
      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;
	}
475
476
477
      else if (!strcmp(argv[formula_index], "-L"))
	{
	  fair_loop_approx = true;
478
	  translation = TransFM;
479
	}
480
481
482
483
      else if (!strcmp(argv[formula_index], "-lS"))
	{
	  labeling_opt = StateLabeled;
	}
484
485
      else if (!strcmp(argv[formula_index], "-m"))
	{
486
	  opt_reduce = true;
487
	}
martinez's avatar
martinez committed
488
489
      else if (!strcmp(argv[formula_index], "-N"))
	{
490
	  degeneralize_opt = DegenSBA;
martinez's avatar
martinez committed
491
492
	  output = 8;
	}
493
494
495
496
497
498
      else if (!strcmp(argv[formula_index], "-NN"))
	{
	  degeneralize_opt = DegenSBA;
	  output = 8;
	  spin_comments = true;
	}
499
500
501
      else if (!strcmp(argv[formula_index], "-p"))
	{
	  post_branching = true;
502
	  translation = TransFM;
503
	}
504
505
506
507
      else if (!strncmp(argv[formula_index], "-P", 2))
	{
	  spot::tgba_parse_error_list pel;
	  system = spot::tgba_parse(argv[formula_index] + 2,
508
				    pel, dict, env, env, debug_opt);
509
510
	  if (spot::format_tgba_parse_errors(std::cerr,
					     argv[formula_index] + 2, pel))
511
512
	    return 2;
	  system->merge_transitions();
513
514
515

	  if (!paper_opt)
	    std::clog << argv[formula_index] + 2 << " read" << std::endl;
516
	}
517
518
      else if (!strcmp(argv[formula_index], "-r"))
	{
519
520
	  output = 1;
	}
521
522
523
524
525
526
      else if (!strcmp(argv[formula_index], "-r1"))
	{
	  redopt |= spot::ltl::Reduce_Basics;
	}
      else if (!strcmp(argv[formula_index], "-r2"))
	{
527
	  redopt |= spot::ltl::Reduce_Eventuality_And_Universality;
528
529
530
	}
      else if (!strcmp(argv[formula_index], "-r3"))
	{
531
	  redopt |= spot::ltl::Reduce_Syntactic_Implications;
532
533
534
	}
      else if (!strcmp(argv[formula_index], "-r4"))
	{
535
536
537
 	  redopt |= spot::ltl::Reduce_Basics
	    | spot::ltl::Reduce_Eventuality_And_Universality
	    | spot::ltl::Reduce_Syntactic_Implications;
538
	}
539
540
      else if (!strcmp(argv[formula_index], "-r5"))
	{
541
	  redopt |= spot::ltl::Reduce_Containment_Checks;
542
543
544
	}
      else if (!strcmp(argv[formula_index], "-r6"))
	{
545
	  redopt |= spot::ltl::Reduce_Containment_Checks_Stronger;
546
547
548
549
550
	}
      else if (!strcmp(argv[formula_index], "-r7"))
	{
	  redopt |= spot::ltl::Reduce_All;
	}
551
552
553
      else if (!strcmp(argv[formula_index], "-R"))
	{
	  output = 3;
554
	}
martinez's avatar
martinez committed
555
556
557
558
559
560
561
562
563
      else if (!strcmp(argv[formula_index], "-R1q"))
	{
	  reduc_aut |= spot::Reduce_quotient_Dir_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R1t"))
	{
	  reduc_aut |= spot::Reduce_transition_Dir_Sim;
	}
      else if (!strcmp(argv[formula_index], "-R2q"))
564
	{
martinez's avatar
martinez committed
565
	  reduc_aut |= spot::Reduce_quotient_Del_Sim;
566
	}
martinez's avatar
martinez committed
567
      else if (!strcmp(argv[formula_index], "-R2t"))
568
	{
martinez's avatar
martinez committed
569
	  reduc_aut |= spot::Reduce_transition_Del_Sim;
570
571
572
573
574
	}
      else if (!strcmp(argv[formula_index], "-R3"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	}
575
576
577
578
579
      else if (!strcmp(argv[formula_index], "-R3f"))
	{
	  reduc_aut |= spot::Reduce_Scc;
	  scc_filter_all = true;
	}
580
581
      else if (!strcmp(argv[formula_index], "-R3b"))
	{
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
582
	  symbolic_scc_pruning = true;
583
	}
584
585
586
587
588
589
590
591
592
593
594
595
      else if (!strcmp(argv[formula_index], "-rd"))
	{
	  display_reduce_form = true;
	}
      else if (!strcmp(argv[formula_index], "-Rd"))
	{
	  display_rel_sim = true;
	}
      else if (!strcmp(argv[formula_index], "-RD"))
	{
	  display_parity_game = true;
	}
596
597
598
599
600
601
602
603
      else if (!strcmp(argv[formula_index], "-s"))
	{
	  dupexp = DFS;
	}
      else if (!strcmp(argv[formula_index], "-S"))
	{
	  dupexp = BFS;
	}
604
605
606
607
      else if (!strcmp(argv[formula_index], "-t"))
	{
	  output = 6;
	}
608
609
610
611
      else if (!strcmp(argv[formula_index], "-T"))
	{
	  use_timer = true;
	}
612
613
614
615
      else if (!strcmp(argv[formula_index], "-taa"))
	{
	  translation = TransTAA;
	}
616
617
618
      else if (!strncmp(argv[formula_index], "-U", 2))
	{
	  unobservables = new spot::ltl::atomic_prop_set;
619
	  translation = TransFM;
620
	  // Parse -U's argument.
621
	  const char* tok = strtok(argv[formula_index] + 2, ", \t;");
622
623
624
625
	  while (tok)
	    {
	      unobservables->insert
		(static_cast<spot::ltl::atomic_prop*>(env.require(tok)));
626
	      tok = strtok(0, ", \t;");
627
628
	    }
	}
629
630
631
632
      else if (!strcmp(argv[formula_index], "-v"))
	{
	  output = 5;
	}
633
634
      else if (!strcmp(argv[formula_index], "-x"))
	{
635
	  translation = TransFM;
636
637
	  fm_exprop_opt = true;
	}
638
639
640
641
      else if (!strcmp(argv[formula_index], "-X"))
	{
	  from_file = true;
	}
642
643
644
645
646
      else if (!strcmp(argv[formula_index], "-XN"))
	{
	  from_file = true;
	  read_neverclaim = true;
	}
647
648
      else if (!strcmp(argv[formula_index], "-y"))
	{
649
	  translation = TransFM;
650
651
	  fm_symb_merge_opt = false;
	}
652
653
654
655
      else
	{
	  break;
	}
656
657
    }

658
  if ((graph_run_opt || graph_run_tgba_opt)
659
      && (!echeck_inst || !expect_counter_example))
660
    {
661
      std::cerr << argv[0] << ": error: -g and -G require -e." << std::endl;
662
663
664
      exit(1);
    }

665
666
667
668
  std::string input;

  if (file_opt)
    {
669
      tm.start("reading formula");
670
      if (strcmp(argv[formula_index], "-"))
671
	{
672
	  std::ifstream fin(argv[formula_index]);
673
	  if (!fin)
674
675
676
677
	    {
	      std::cerr << "Cannot open " << argv[formula_index] << std::endl;
	      exit(2);
	    }
678

679
	  if (!std::getline(fin, input, '\0'))
680
681
682
683
684
685
	    {
	      std::cerr << "Cannot read " << argv[formula_index] << std::endl;
	      exit(2);
	    }
	}
      else
686
	{
687
	  std::getline(std::cin, input, '\0');
688
	}
689
      tm.stop("reading formula");
690
691
692
693
694
695
    }
  else
    {
      input = argv[formula_index];
    }

696
  spot::ltl::formula* f = 0;
697
  if (!from_file) // Reading a formula, not reading an automaton from a file.
698
    {
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
      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;
740
	}
741
742
    }
  if (f || from_file)
743
    {
744
745
746
747
      spot::tgba_bdd_concrete* concrete = 0;
      spot::tgba* to_free = 0;
      spot::tgba* a = 0;

748
749
      if (from_file)
	{
750
	  spot::tgba_explicit_string* e;
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
	  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
766
	    {
767
768
769
770
771
772
773
774
775
776
777
	      spot::neverclaim_parse_error_list pel;
	      tm.start("parsing never claim");
	      to_free = a = e = spot::neverclaim_parse(input, pel, dict, 
						       env, debug_opt);	      
	      tm.stop("parsing never claim");
	      if (spot::format_neverclaim_parse_errors(std::cerr, input, pel))
		{
		  delete to_free;
		  delete dict;
		  return 2;
		}	      
778
	    }
779
	  e->merge_transitions();
780
	}
781
      else
782
	{
783
	  if (redopt != spot::ltl::Reduce_None)
784
	    {
785
	      tm.start("reducing formula");
786
	      spot::ltl::formula* t = spot::ltl::reduce(f, redopt);
787
	      f->destroy();
788
	      tm.stop("reducing formula");
789
	      f = t;
790
791
	      if (display_reduce_form)
		std::cout << spot::ltl::to_string(f) << std::endl;
792
	    }
793

794
	  tm.start("translating formula");
795
796
797
798
799
800
801
802
	  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,
803
				       fm_red);
804
805
806
807
808
	      break;
	    case TransTAA:
	      a = spot::ltl_to_taa(f, dict, containment);
	      break;
	    case TransLaCIM:
809
810
811
812
813
	      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);
814
815
	      break;
	    }
816
	  tm.stop("translating formula");
817
	  to_free = a;
818
	}
819

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
      if (symbolic_scc_pruning)
        {
	  spot::tgba_bdd_concrete* bc =
	    dynamic_cast<spot::tgba_bdd_concrete*>(a);
	  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)
		bc->delete_unaccepting_scc();
	      tm.stop("reducing A_f w/ symbolic SCC pruning");
	    }
	}

842
843
844
845
846
847
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.
      spot::tgba* aut_scc = 0;
      if (reduc_aut & spot::Reduce_Scc)
	{
	  tm.start("reducing A_f w/ SCC");
848
	  a = aut_scc = spot::scc_filter(a, scc_filter_all);
849
850
851
	  tm.stop("reducing A_f w/ SCC");
	}

852
      spot::tgba_tba_proxy* degeneralized = 0;
853
      spot::tgba_sgba_proxy* state_labeled = 0;
854

855
856
      unsigned int n_acc = a->number_of_acceptance_conditions();
      if (echeck_inst
857
	  && degeneralize_opt == NoDegen
858
859
	  && n_acc > 1
	  && echeck_inst->max_acceptance_conditions() < n_acc)
860
861
	degeneralize_opt = DegenTBA;
      if (degeneralize_opt == DegenTBA)
862
	a = degeneralized = new spot::tgba_tba_proxy(a);
863
864
      else if (degeneralize_opt == DegenSBA)
	a = degeneralized = new spot::tgba_sba_proxy(a);
865
866
867
868
      else if (labeling_opt == StateLabeled)
      {
        a = state_labeled = new spot::tgba_sgba_proxy(a);
      }
869

870
871
872
      spot::tgba_reduc* aut_red = 0;
      if (reduc_aut != spot::Reduce_None)
	{
873
	  if (reduc_aut & ~spot::Reduce_Scc)
874
	    {
875
	      tm.start("reducing A_f w/ sim.");
876
	      a = aut_red = new spot::tgba_reduc(a);
martinez's avatar
martinez committed
877
878

	      if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
879
880
881
			       spot::Reduce_transition_Dir_Sim |
			       spot::Reduce_quotient_Del_Sim |
			       spot::Reduce_transition_Del_Sim))
882
		{
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
		  spot::direct_simulation_relation* rel_dir = 0;
		  spot::delayed_simulation_relation* rel_del = 0;

		  if (reduc_aut & (spot::Reduce_quotient_Dir_Sim |
				   spot::Reduce_transition_Dir_Sim))
		    {
		      rel_dir =
			spot::get_direct_relation_simulation
			  (a, std::cout, display_parity_game);
		      assert(rel_dir);
		    }
		  if (reduc_aut & (spot::Reduce_quotient_Del_Sim |
					spot::Reduce_transition_Del_Sim))
		    {
		      rel_del =
			spot::get_delayed_relation_simulation
			  (a, std::cout, display_parity_game);
		      assert(rel_del);
		    }

		  if (display_rel_sim)
		    {
		      if (rel_dir)
			aut_red->display_rel_sim(rel_dir, std::cout);
		      if (rel_del)
			aut_red->display_rel_sim(rel_del, std::cout);
		    }

		  if (reduc_aut & spot::Reduce_quotient_Dir_Sim)
		    aut_red->quotient_state(rel_dir);
		  if (reduc_aut & spot::Reduce_transition_Dir_Sim)
		    aut_red->delete_transitions(rel_dir);
		  if (reduc_aut & spot::Reduce_quotient_Del_Sim)
		    aut_red->quotient_state(rel_del);
		  if (reduc_aut & spot::Reduce_transition_Del_Sim)
		    aut_red->delete_transitions(rel_del);
919

martinez's avatar
martinez committed
920
		  if (rel_dir)
921
		    spot::free_relation_simulation(rel_dir);
martinez's avatar
martinez committed
922
		  if (rel_del)
923
		    spot::free_relation_simulation(rel_del);
martinez's avatar
martinez committed
924
		}
925
	      tm.stop("reducing A_f w/ sim.");
926
927
928
	    }
	}

929
930
931
932
933
934
935
936
937
938
939
940
941
      spot::tgba_explicit* expl = 0;
      switch (dupexp)
	{
	case NoneDup:
	  break;
	case BFS:
	  a = expl = tgba_dupexp_bfs(a);
	  break;
	case DFS:
	  a = expl = tgba_dupexp_dfs(a);
	  break;
	}

942
943
      spot::tgba* product_degeneralized = 0;

944
      if (system)
945
946
        {
          a = product = product_to_free = new spot::tgba_product(system, a);
947
948
949
950
951
952

	  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)
953
954
955
956
957
958
959
960
            degeneralize_opt = DegenTBA;
          if (degeneralize_opt == DegenTBA)
            a = product = product_degeneralized =
                                            new spot::tgba_tba_proxy(product);
          else if (degeneralize_opt == DegenSBA)
            a = product = product_degeneralized =
                                            new spot::tgba_sba_proxy(product);
        }
961

962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
      if (echeck_inst
	  && (a->number_of_acceptance_conditions()
	      < echeck_inst->min_acceptance_conditions()))
	{
	  if (!paper_opt)
	    {
	      std::cerr << echeck_algo << " requires at least "
			<< echeck_inst->min_acceptance_conditions()
			<< " acceptance conditions." << std::endl;
	      exit(1);
	    }
	  else
	    {
	      std::cout << std::endl;
	      exit(0);
	    }
	}

980
981
982
983
984
      if (show_fc)
	{
	  a = new spot::future_conditions_collector(a, true);
	}

985
      if (output != -1)
986
	{
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
	  tm.start("producing output");
	  switch (output)
	    {
	    case 0:
	      spot::dotty_reachable(std::cout, a);
	      break;
	    case 1:
	      if (concrete)
		spot::bdd_print_dot(std::cout, concrete->get_dict(),
				    concrete->get_core_data().relation);
	      break;
	    case 2:
	      if (concrete)
		spot::bdd_print_dot(std::cout, concrete->get_dict(),
				    concrete->
				    get_core_data().acceptance_conditions);
	      break;
	    case 3:
	      if (concrete)
		spot::bdd_print_set(std::cout, concrete->get_dict(),
				    concrete->get_core_data().relation);
	      break;
	    case 4:
	      if (concrete)
		spot::bdd_print_set(std::cout, concrete->get_dict(),
				    concrete->
				    get_core_data().acceptance_conditions);
	      break;
	    case 5:
	      a->get_dict()->dump(std::cout);
	      break;
	    case 6:
	      spot::lbtt_reachable(std::cout, a);
	      break;
	    case 7:
	      spot::tgba_save_reachable(std::cout, a);
	      break;
	    case 8:
	      {
		assert(degeneralize_opt == DegenSBA);
		const spot::tgba_sba_proxy* s =
		  static_cast<const spot::tgba_sba_proxy*>(degeneralized);
1029
		spot::never_claim_reachable(std::cout, s, f, spin_comments);
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
		break;
	      }
	    case 9:
	      stats_reachable(a).dump(std::cout);
	      build_scc_stats(a).dump(std::cout);
	      break;
	    case 10:
	      dump_scc_dot(a, std::cout, false);
	      break;
	    case 11:
	      dump_scc_dot(a, std::cout, true);
	      break;
	    default:
	      assert(!"unknown output option");
	    }
	  tm.stop("producing output");
1046
	}
1047

1048
      if (echeck_inst)
1049
	{
1050
1051
1052
	  spot::emptiness_check* ec = echeck_inst->instantiate(a);
	  bool search_many = echeck_inst->options().get("repeated");
	  assert(ec);
1053
1054
	  do
	    {
1055
	      tm.start("running emptiness check");
1056
	      spot::emptiness_check_result* res = ec->check();
1057
1058
	      tm.stop("running emptiness check");

1059
1060
1061
              if (paper_opt)
                {
                  std::ios::fmtflags old = std::cout.flags();
1062
                  std::cout << std::left << std::setw(25)
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
                            << echeck_algo << ", ";
                  spot::tgba_statistics a_size =
                                        spot::stats_reachable(ec->automaton());
                  std::cout << std::right << std::setw(10)
                            << a_size.states << ", "
                            << std::right << std::setw(10)
                            << a_size.transitions << ", ";
                  std::cout <<
                            ec->automaton()->number_of_acceptance_conditions()
                            << ", ";
                  const spot::ec_statistics* ecs =
                        dynamic_cast<const spot::ec_statistics*>(ec);
                  if (ecs)
                    std::cout << std::right << std::setw(10)
                              << ecs->states() << ", "
                              << std::right << std::setw(10)
                              << ecs->transitions() << ", "
                              << std::right << std::setw(10)
                              << ecs->max_depth();
                  else
1083
                    std::cout << "no stats, , ";
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
                  if (res)
                    std::cout << ", accepting run found";
                  else
                    std::cout << ", no accepting run found";
                  std::cout << std::endl;
                  std::cout << std::setiosflags(old);
                }
              else
                {
                  if (!graph_run_opt && !graph_run_tgba_opt)
                    ec->print_stats(std::cout);
                  if (expect_counter_example != !!res &&
1096
		      (!expect_counter_example || ec->safe()))
1097
1098
1099
                    exit_code = 1;

                  if (!res)
1100
                    {
1101
                      std::cout << "no accepting run found";
1102
                      if (!ec->safe() && expect_counter_example)
1103
1104
                        {
                          std::cout << " even if expected" << std::endl;
1105
1106
                          std::cout << "this may be due to the use of the bit"
                                    << " state hashing technique" << std::endl;
1107
1108
1109
1110
1111
1112
                          std::cout << "you can try to increase the heap size "
                                    << "or use an explicit storage"
                                    << std::endl;
                        }
                      std::cout << std::endl;
                      break;
1113
                    }
1114
1115
                  else
                    {
1116

1117
		      tm.start("computing accepting run");
1118
                      spot::tgba_run* run = res->accepting_run();
1119
1120
		      tm.stop("computing accepting run");