ikwiad.cc 50.5 KB
Newer Older
1
// -*- coding: utf-8 -*-
2
// Copyright (C) 2007-2017 Laboratoire de Recherche et Développement
3
4
5
6
// de l'Epita (LRDE).
// Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie.
7
8
9
10
11
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
12
// the Free Software Foundation; either version 3 of the License, or
13
14
15
16
17
18
19
20
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
21
// along with this program.  If not, see <http://www.gnu.org/licenses/>.
22

23
#include <iostream>
24
#include <iomanip>
25
#include <cassert>
26
27
#include <fstream>
#include <string>
28
#include <cstdlib>
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
#include <spot/tl/print.hh>
#include <spot/tl/apcollect.hh>
#include <spot/tl/formula.hh>
#include <spot/tl/parse.hh>
#include <spot/twaalgos/ltl2tgba_fm.hh>
#include <spot/twaalgos/ltl2taa.hh>
#include <spot/twa/bddprint.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/lbtt.hh>
#include <spot/twaalgos/hoa.hh>
#include <spot/twaalgos/degen.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/parseaut/public.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/minimize.hh>
#include <spot/taalgos/minimize.hh>
#include <spot/twaalgos/neverclaim.hh>
#include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/strength.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/misc/timer.hh>
#include <spot/twaalgos/stats.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/emptiness_stats.hh>
#include <spot/twaalgos/sccinfo.hh>
#include <spot/twaalgos/isdet.hh>
#include <spot/twaalgos/cycles.hh>
#include <spot/twaalgos/isweakscc.hh>
#include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/compsusp.hh>
#include <spot/twaalgos/powerset.hh>
60
#include <spot/twaalgos/dualize.hh>
61
62
63
64
65
66
#include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/dtbasat.hh>
#include <spot/twaalgos/dtwasat.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twaalgos/totgba.hh>
67

68
69
70
#include <spot/taalgos/tgba2ta.hh>
#include <spot/taalgos/dot.hh>
#include <spot/taalgos/stats.hh>
71

72
static void
73
74
syntax(char* prog)
{
75
76
77
78
79
  // 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;

80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
  std::cerr <<
    "Usage: " << prog << " [-f|-l|-taa] [OPTIONS...] formula\n"
    "       " << prog << " [-f|-l|-taa] -F [OPTIONS...] file\n"
    "       " << prog << " -XH [OPTIONS...] file\n"
    "\n"
    "Translate an LTL formula into an automaton, or read the automaton from "
    "a file.\n"
    "Optionally multiply this automaton by another automaton read "
    "from a file.\n"
    "Output the result in various formats, or perform an emptiness check."
    "\n\n"
    "Input options:\n"
    "  -F    read the formula from a file, not from the command line\n"
    "  -XD   do not compute an automaton, read it from an ltl2dstar file\n"
    "  -XDB  like -XD, and convert it to TGBA\n"
    "  -XH   do not compute an automaton, read it from a HOA file\n"
    "  -XL   do not compute an automaton, read it from an LBTT file\n"
    "  -XN   do not compute an automaton, read it from a neverclaim file\n"
    "  -Pfile  multiply the formula automaton with the TGBA read"
    " from `file'\n"
    "  -KPfile multiply the formula automaton with the Kripke"
    " structure from `file'\n"
    "\n"
    "Translation algorithm:\n"
    "  -f    use Couvreur's FM algorithm for LTL (default)\n"
    "  -taa  use Tauriainen's TAA-based algorithm for LTL\n"
    "  -u    use Compositional translation\n"
    "\n"
    "Options for Couvreur's FM algorithm (-f):\n"
    "  -fr   reduce formula at each step of FM\n"
    "          as specified with the -r{1..7} options\n"
    "  -fu   build unambiguous automata\n"
    "  -L    fair-loop approximation (implies -f)\n"
    "  -p    branching postponement (implies -f)\n"
    "  -U[PROPS]  consider atomic properties of the formula as "
    "exclusive events, and\n"
    "        PROPS as unobservables events (implies -f)\n"
    "  -x    try to produce a more deterministic automaton "
    "(implies -f)\n"
    "  -y    do not merge states with same symbolic representation "
    "(implies -f)\n"
    "\n"
    "Options for Tauriainen's TAA-based algorithm (-taa):\n"
    "  -c    enable language containment checks (implies -taa)\n"
    "\n"
    "Formula simplification (before translation):\n"
    "  -r1   reduce formula using basic rewriting\n"
    "  -r2   reduce formula using class of eventuality and universality\n"
    "  -r3   reduce formula using implication between sub-formulae\n"
    "  -r4   reduce formula using all above rules\n"
    "  -r5   reduce formula using tau03\n"
    "  -r6   reduce formula using tau03+\n"
    "  -r7   reduce formula using tau03+ and -r4\n"
    "  -rd   display the reduced formula\n"
    "  -rD   dump statistics about the simplifier cache\n"
    "  -rL   disable basic rewritings producing larger formulas\n"
    "  -ru   lift formulae that are eventual and universal\n"
    "\n"
    "Automaton degeneralization (after translation):\n"
    "  -DT   degeneralize the automaton as a TBA\n"
    "  -DS   degeneralize the automaton as an SBA\n"
    "          (append z/Z, o/O, l/L: to turn on/off options "
    "(default: zol)\n "
    "          z: level resetting, o: adaptive order, "
    "l: level cache)\n"
    "\n"
    "Automaton simplifications (after translation):\n"
    "  -R3   use SCCs to remove useless states and acceptance sets\n"
    "  -R3f  clean more acceptance sets than -R3\n"
    "          "
    "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)\n"
    "  -RDS  reduce the automaton with direct simulation\n"
    "  -RRS  reduce the automaton with reverse simulation\n"
    "  -RIS  iterate both direct and reverse simulations\n"
    "  -Rm   attempt to WDBA-minimize the automaton\n"
    "  -RM   attempt to WDBA-minimize the automaton unless the "
    "result is bigger\n"
    "  -RQ   determinize a TGBA (assuming it's legal!)\n"
    "\n"
    "Automaton conversion:\n"
    "  -M    convert into a det. minimal monitor (implies -R3 or R3b)\n"
    "  -s    convert to explicit automaton, and number states in DFS order\n"
    "  -S    convert to explicit automaton, and number states in BFS order\n"
    "\n"
    "Conversion to Testing Automaton:\n"
    "  -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\n"
    "  -RT   reduce the (G)TA/TGTA using bisimulation.\n"
    "\n"
    "Options for performing emptiness checks (on TGBA):\n"
    "  -e[ALGO]  run emptiness check, expect and compute an "
    "accepting run\n"
    "  -E[ALGO]  run emptiness check, expect no accepting run\n"
    "  -C    compute an accepting run (Counterexample) if it exists\n"
    "  -CR   compute and replay an accepting run (implies -C)\n"
    "  -G    graph the accepting run seen as an automaton (requires -e)\n"
    "  -m    try to reduce accepting runs, in a second pass\n"
    "Where ALGO should be one of:\n"
    "  Cou99(OPTIONS) (the default)\n"
    "  CVWY90(OPTIONS)\n"
    "  GV04(OPTIONS)\n"
    "  SE05(OPTIONS)\n"
    "  Tau03(OPTIONS)\n"
    "  Tau03_opt(OPTIONS)\n"
    "\n"
    "If no emptiness check is run, the automaton will be output "
    "in dot format\nby default.  This can be "
    "changed with the following options.\n"
    "\n"
    "Output options (if no emptiness check):\n"
    "  -ks   display statistics on the automaton (size only)\n"
    "  -kt   display statistics on the automaton (size + subtransitions)\n"
    "  -K    dump the graph of SCCs in dot format\n"
    "  -KC   list cycles in automaton\n"
    "  -KW   list weak SCCs\n"
    "  -N    output the never clain for Spin (implies -DS)\n"
    "  -NN   output the never clain for Spin, with commented states"
    " (implies -DS)\n"
    "  -O    tell if a formula represents a safety, guarantee, "
    "or obligation property\n"
    "  -t    output automaton in LBTT's format\n"
    "\n"
    "Miscellaneous options:\n"
    "  -0    produce minimal output dedicated to the paper\n"
    "  -8    output UTF-8 formulae\n"
    "  -d    turn on traces during parsing\n"
    "  -T    time the different phases of the translation\n"
    "  -v    display the BDD variables used by the automaton\n";
213
214
215
  exit(2);
}

Thomas Badie's avatar
Thomas Badie committed
216
217
218
219
220
221
static int
to_int(const char* s)
{
  char* endptr;
  int res = strtol(s, &endptr, 10);
  if (*endptr)
222
    {
223
      std::cerr << "Failed to parse `" << s << "' as an integer.\n";
224
225
      exit(1);
    }
Thomas Badie's avatar
Thomas Badie committed
226
227
228
  return res;
}

229
230
static spot::twa_graph_ptr
ensure_digraph(const spot::twa_ptr& a)
231
{
232
  auto aa = std::dynamic_pointer_cast<spot::twa_graph>(a);
233
234
  if (aa)
    return aa;
235
  return spot::make_twa_graph(a, spot::twa::prop_set::all());
236
237
}

238
static int
239
checked_main(int argc, char** argv)
240
241
242
{
  int exit_code = 0;

243
  bool debug_opt = false;
244
  bool paper_opt = false;
245
  bool utf8_opt = false;
246
  enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
247
  enum { TransFM, TransTAA, TransCompo } translation = TransFM;
248
  bool fm_red = false;
249
  bool fm_exprop_opt = false;
250
  bool fm_symb_merge_opt = true;
251
  bool fm_unambiguous = false;
252
  bool file_opt = false;
253
  bool degen_reset = true;
254
  bool degen_order = false;
255
  bool degen_cache = true;
256
  int output = 0;
257
  int formula_index = 0;
258
259
  const char* echeck_algo = nullptr;
  spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
260
  bool dupexp = false;
261
  bool expect_counter_example = false;
262
263
  bool accepting_run = false;
  bool accepting_run_replay = false;
264
  bool from_file = false;
265
  bool nra2nba = false;
266
  bool scc_filter = false;
267
  bool simpltl = false;
268
  spot::tl_simplifier_options redopt(false, false, false, false,
269
                                           false, false, false);
270
  bool simpcache_stats = false;
271
  bool scc_filter_all = false;
272
  bool display_reduced_form = false;
273
  bool post_branching = false;
274
  bool fair_loop_approx = false;
275
  bool graph_run_tgba_opt = false;
276
  bool opt_reduce = false;
Felix Abecassis's avatar
Felix Abecassis committed
277
  bool opt_minimize = false;
278
  bool opt_determinize = false;
279
280
  unsigned opt_determinize_threshold = 0;
  unsigned opt_o_threshold = 0;
281
  bool opt_dtwacomp = false;
282
  bool reject_bigger = false;
283
  bool opt_monitor = false;
284
  bool containment = false;
285
286
  bool opt_closure = false;
  bool opt_stutterize = false;
287
288
  const char* opt_never = nullptr;
  const char* hoa_opt = nullptr;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
289
290
  auto& env = spot::default_environment::instance();
  spot::atomic_prop_set* unobservables = nullptr;
291
  spot::twa_ptr system_aut = nullptr;
292
  auto dict = spot::make_bdd_dict();
293
294
  spot::timer_map tm;
  bool use_timer = false;
Thomas Badie's avatar
Thomas Badie committed
295
  bool reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
296
  bool reduction_rev_sim = false;
297
  bool reduction_iterated_sim = false;
298
  bool opt_bisim_ta = false;
299
  bool ta_opt = false;
300
  bool tgta_opt = false;
301
  bool opt_with_artificial_initial_state = true;
302
303
  bool opt_single_pass_emptiness_check = false;
  bool opt_with_artificial_livelock = false;
304
305
306
307
308
  bool cs_nowdba = true;
  bool cs_wdba_smaller = false;
  bool cs_nosimul = true;
  bool cs_early_start = false;
  bool cs_oblig = false;
309
310
  bool opt_complete = false;
  int opt_dtbasat = -1;
311
  int opt_dtwasat = -1;
312

313
  for (;;)
314
    {
315
      if (argc < formula_index + 2)
316
        syntax(argv[0]);
317
318
319

      ++formula_index;

320
      if (!strcmp(argv[formula_index], "-0"))
321
322
323
        {
          paper_opt = true;
        }
324
      else if (!strcmp(argv[formula_index], "-8"))
325
326
327
328
        {
          utf8_opt = true;
          spot::enable_utf8();
        }
329
      else if (!strcmp(argv[formula_index], "-c"))
330
331
332
333
        {
          containment = true;
          translation = TransTAA;
        }
334
      else if (!strcmp(argv[formula_index], "-C"))
335
336
337
        {
          accepting_run = true;
        }
338
      else if (!strcmp(argv[formula_index], "-CR"))
339
340
341
342
        {
          accepting_run = true;
          accepting_run_replay = true;
        }
343
      else if (!strcmp(argv[formula_index], "-d"))
344
345
346
        {
          debug_opt = true;
        }
347
      else if (!strcmp(argv[formula_index], "-D"))
348
349
350
351
        {
          std::cerr << "-D was renamed to -DT\n";
          abort();
        }
352
      else if (!strcmp(argv[formula_index], "-DC"))
353
354
355
        {
          opt_dtwacomp = true;
        }
356
      else if (!strncmp(argv[formula_index], "-DS", 3)
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
               || !strncmp(argv[formula_index], "-DT", 3))
        {
          degeneralize_opt =
            argv[formula_index][2] == 'S' ? DegenSBA : DegenTBA;
          const char* p = argv[formula_index] + 3;
          while (*p)
            {
              switch (*p++)
                {
                case 'o':
                  degen_order = true;
                  break;
                case 'O':
                  degen_order = false;
                  break;
                case 'z':
                  degen_reset = true;
                  break;
                case 'Z':
                  degen_reset = false;
                  break;
                case 'l':
                  degen_cache = true;
                  break;
                case 'L':
                  degen_cache = false;
                  break;
                }
            }
        }
387
      else if (!strncmp(argv[formula_index], "-e", 2))
388
        {
389
390
391
392
393
394
395
396
397
398
399
400
401
          echeck_algo = 2 + argv[formula_index];
          if (!*echeck_algo)
            echeck_algo = "Cou99";

          const char* err;
          echeck_inst =
            spot::make_emptiness_check_instantiator(echeck_algo, &err);
          if (!echeck_inst)
            {
              std::cerr << "Failed to parse argument of -e near `"
                        << err <<  '\'' << std::endl;
              exit(2);
            }
402
403
404
          expect_counter_example = true;
          output = -1;
        }
405
      else if (!strncmp(argv[formula_index], "-E", 2))
406
        {
407
408
409
410
411
412
413
414
415
416
417
418
419
          const char* echeck_algo = 2 + argv[formula_index];
          if (!*echeck_algo)
            echeck_algo = "Cou99";

          const char* err;
          echeck_inst =
            spot::make_emptiness_check_instantiator(echeck_algo, &err);
          if (!echeck_inst)
            {
              std::cerr << "Failed to parse argument of -e near `"
                        << err <<  '\'' << std::endl;
              exit(2);
            }
420
421
422
          expect_counter_example = false;
          output = -1;
        }
423
      else if (!strcmp(argv[formula_index], "-f"))
424
425
426
        {
          translation = TransFM;
        }
427
      else if (!strcmp(argv[formula_index], "-fr"))
428
429
430
431
        {
          fm_red = true;
          translation = TransFM;
        }
432
      else if (!strcmp(argv[formula_index], "-fu"))
433
434
435
436
437
        {
          fm_unambiguous = true;
          fm_exprop_opt = true;
          translation = TransFM;
        }
438
      else if (!strcmp(argv[formula_index], "-F"))
439
440
441
        {
          file_opt = true;
        }
442
      else if (!strcmp(argv[formula_index], "-G"))
443
444
445
446
        {
          accepting_run = true;
          graph_run_tgba_opt = true;
        }
447
      else if (!strncmp(argv[formula_index], "-H", 2))
448
449
450
451
        {
          output = 17;
          hoa_opt = argv[formula_index] + 2;
        }
452
      else if (!strcmp(argv[formula_index], "-ks"))
453
454
455
        {
          output = 12;
        }
456
      else if (!strcmp(argv[formula_index], "-kt"))
457
458
459
        {
          output = 13;
        }
460
      else if (!strcmp(argv[formula_index], "-K"))
461
462
463
        {
          output = 10;
        }
464
      else if (!strncmp(argv[formula_index], "-KP", 3))
465
466
467
468
469
470
471
472
473
474
475
        {
          tm.start("reading -KP's argument");
          spot::automaton_parser_options opts;
          opts.debug = debug_opt;
          opts.want_kripke = true;
          auto paut = spot::parse_aut(argv[formula_index] + 3, dict, env, opts);
          if (paut->format_errors(std::cerr))
            return 2;
          system_aut = paut->ks;
          tm.stop("reading -KP's argument");
        }
476
      else if (!strcmp(argv[formula_index], "-KC"))
477
478
479
        {
          output = 15;
        }
480
      else if (!strcmp(argv[formula_index], "-KW"))
481
482
483
        {
          output = 16;
        }
484
      else if (!strcmp(argv[formula_index], "-L"))
485
486
487
488
        {
          fair_loop_approx = true;
          translation = TransFM;
        }
489
      else if (!strcmp(argv[formula_index], "-m"))
490
491
492
        {
          opt_reduce = true;
        }
martinez's avatar
martinez committed
493
      else if (!strcmp(argv[formula_index], "-N"))
494
495
496
497
498
        {
          degeneralize_opt = DegenSBA;
          output = 8;
          opt_never = nullptr;
        }
499
      else if (!strcmp(argv[formula_index], "-NN"))
500
501
502
503
504
        {
          degeneralize_opt = DegenSBA;
          output = 8;
          opt_never = "c";
        }
505
      else if (!strncmp(argv[formula_index], "-O", 2))
506
507
        {
          output = 14;
508
          opt_minimize = true;
509
510
511
          if (argv[formula_index][2] != 0)
            opt_o_threshold = to_int(argv[formula_index] + 2);
        }
512
      else if (!strcmp(argv[formula_index], "-p"))
513
514
515
516
        {
          post_branching = true;
          translation = TransFM;
        }
517
      else if (!strncmp(argv[formula_index], "-P", 2))
518
519
520
521
522
523
524
525
526
527
528
529
        {
          tm.start("reading -P's argument");

          spot::automaton_parser_options opts;
          opts.debug = debug_opt;
          auto daut = spot::parse_aut(argv[formula_index] + 2, dict, env, opts);
          if (daut->format_errors(std::cerr))
            return 2;
          daut->aut->merge_edges();
          system_aut = daut->aut;
          tm.stop("reading -P's argument");
        }
530
      else if (!strcmp(argv[formula_index], "-r1"))
531
532
533
534
        {
          simpltl = true;
          redopt.reduce_basics = true;
        }
535
      else if (!strcmp(argv[formula_index], "-r2"))
536
537
538
539
        {
          simpltl = true;
          redopt.event_univ = true;
        }
540
      else if (!strcmp(argv[formula_index], "-r3"))
541
542
543
544
        {
          simpltl = true;
          redopt.synt_impl = true;
        }
545
      else if (!strcmp(argv[formula_index], "-r4"))
546
547
548
549
550
551
        {
          simpltl = true;
          redopt.reduce_basics = true;
          redopt.event_univ = true;
          redopt.synt_impl = true;
        }
552
      else if (!strcmp(argv[formula_index], "-r5"))
553
554
555
556
        {
          simpltl = true;
          redopt.containment_checks = true;
        }
557
      else if (!strcmp(argv[formula_index], "-r6"))
558
559
560
561
562
        {
          simpltl = true;
          redopt.containment_checks = true;
          redopt.containment_checks_stronger = true;
        }
563
      else if (!strcmp(argv[formula_index], "-r7"))
564
565
566
567
568
569
570
571
        {
          simpltl = true;
          redopt.reduce_basics = true;
          redopt.event_univ = true;
          redopt.synt_impl = true;
          redopt.containment_checks = true;
          redopt.containment_checks_stronger = true;
        }
572
      else if (!strcmp(argv[formula_index], "-R1q")
573
574
575
576
577
578
579
580
               || !strcmp(argv[formula_index], "-R1t")
               || !strcmp(argv[formula_index], "-R2q")
               || !strcmp(argv[formula_index], "-R2t"))
        {
          // For backward compatibility, make all these options
          // equal to -RDS.
          reduction_dir_sim = true;
        }
Thomas Badie's avatar
Thomas Badie committed
581
582
583
584
      else if (!strcmp(argv[formula_index], "-RRS"))
        {
          reduction_rev_sim = true;
        }
585
      else if (!strcmp(argv[formula_index], "-R3"))
586
587
588
        {
          scc_filter = true;
        }
589
      else if (!strcmp(argv[formula_index], "-R3f"))
590
591
592
593
        {
          scc_filter = true;
          scc_filter_all = true;
        }
594
      else if (!strcmp(argv[formula_index], "-rd"))
595
596
597
        {
          display_reduced_form = true;
        }
598
      else if (!strcmp(argv[formula_index], "-rD"))
599
600
601
        {
          simpcache_stats = true;
        }
602
      else if (!strcmp(argv[formula_index], "-RC"))
603
604
605
        {
          opt_complete = true;
        }
606
      else if (!strcmp(argv[formula_index], "-RDS"))
Felix Abecassis's avatar
Felix Abecassis committed
607
        {
608
          reduction_dir_sim = true;
Felix Abecassis's avatar
Felix Abecassis committed
609
        }
610
611
612
613
      else if (!strcmp(argv[formula_index], "-RIS"))
        {
          reduction_iterated_sim = true;
        }
614
      else if (!strcmp(argv[formula_index], "-rL"))
615
        {
616
617
618
          simpltl = true;
          redopt.reduce_basics = true;
          redopt.reduce_size_strictly = true;
619
        }
620
621
      else if (!strncmp(argv[formula_index], "-RG", 3))
        {
622
623
624
625
          if (argv[formula_index][3] != 0)
            opt_dtwasat = to_int(argv[formula_index] + 3);
          else
            opt_dtwasat = 0;
626
627
          //output = -1;
        }
628
629
630
631
      else if (!strcmp(argv[formula_index], "-Rm"))
        {
          opt_minimize = true;
        }
632
633
634
      else if (!strcmp(argv[formula_index], "-RM"))
        {
          opt_minimize = true;
635
          reject_bigger = true;
636
        }
637
      else if (!strncmp(argv[formula_index], "-RQ", 3))
638
639
        {
          opt_determinize = true;
640
641
          if (argv[formula_index][3] != 0)
            opt_determinize_threshold = to_int(argv[formula_index] + 3);
642
        }
643
644
      else if (!strncmp(argv[formula_index], "-RS", 3))
        {
645
646
647
648
          if (argv[formula_index][3] != 0)
            opt_dtbasat = to_int(argv[formula_index] + 3);
          else
            opt_dtbasat = 0;
649
650
          //output = -1;
        }
651
652
653
      else if (!strcmp(argv[formula_index], "-RT"))
        {
          opt_bisim_ta = true;
654
        }
655
656
      else if (!strcmp(argv[formula_index], "-ru"))
        {
657
658
659
          simpltl = true;
          redopt.event_univ = true;
          redopt.favor_event_univ = true;
660
        }
661
662
663
664
      else if (!strcmp(argv[formula_index], "-M"))
        {
          opt_monitor = true;
        }
665
      else if (!strcmp(argv[formula_index], "-S"))
666
667
668
        {
          dupexp = true;
        }
669
      else if (!strcmp(argv[formula_index], "-CL"))
670
671
672
        {
          opt_closure = true;
        }
673
      else if (!strcmp(argv[formula_index], "-ST"))
674
675
676
        {
          opt_stutterize = true;
        }
677
      else if (!strcmp(argv[formula_index], "-t"))
678
679
680
        {
          output = 6;
        }
681
      else if (!strcmp(argv[formula_index], "-T"))
682
683
684
        {
          use_timer = true;
        }
685
686
687
688
      else if (!strcmp(argv[formula_index], "-TA"))
        {
          ta_opt = true;
        }
689
      else if (!strcmp(argv[formula_index], "-TGTA"))
690
        {
691
          tgta_opt = true;
692
        }
693
694
695
696
      else if (!strcmp(argv[formula_index], "-lv"))
        {
          opt_with_artificial_livelock = true;
        }
697
698
699
700
      else if (!strcmp(argv[formula_index], "-sp"))
        {
          opt_single_pass_emptiness_check = true;
        }
701
702
703
704
      else if (!strcmp(argv[formula_index], "-in"))
        {
          opt_with_artificial_initial_state = false;
        }
705
      else if (!strcmp(argv[formula_index], "-taa"))
706
707
708
        {
          translation = TransTAA;
        }
709
      else if (!strncmp(argv[formula_index], "-U", 2))
710
711
712
713
714
715
716
717
718
719
720
        {
          unobservables = new spot::atomic_prop_set;
          translation = TransFM;
          // Parse -U's argument.
          const char* tok = strtok(argv[formula_index] + 2, ", \t;");
          while (tok)
            {
              unobservables->insert(env.require(tok));
              tok = strtok(nullptr, ", \t;");
            }
        }
721
      else if (!strncmp(argv[formula_index], "-u", 2))
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
        {
          translation = TransCompo;
          const char* c = argv[formula_index] + 2;
          while (*c != 0)
            {
              switch (*c)
                {
                case '2':
                  cs_nowdba = false;
                  cs_wdba_smaller = true;
                  break;
                case 'w':
                  cs_nowdba = false;
                  cs_wdba_smaller = false;
                  break;
                case 's':
                  cs_nosimul = false;
                  break;
                case 'e':
                  cs_early_start = true;
                  break;
                case 'W':
                  cs_nowdba = true;
                  break;
                case 'S':
                  cs_nosimul = true;
                  break;
                case 'E':
                  cs_early_start = false;
                  break;
                case 'o':
                  cs_oblig = true;
                  break;
                case 'O':
                  cs_oblig = false;
                  break;
                default:
                  std::cerr << "Unknown suboption `" << *c
760
                            << "' for option -u\n";
761
762
763
764
                }
              ++c;
            }
        }
765
      else if (!strcmp(argv[formula_index], "-v"))
766
767
768
        {
          output = 5;
        }
769
      else if (!strcmp(argv[formula_index], "-x"))
770
771
772
773
        {
          translation = TransFM;
          fm_exprop_opt = true;
        }
774
      else if (!strcmp(argv[formula_index], "-XD"))
775
776
777
        {
          from_file = true;
        }
778
      else if (!strcmp(argv[formula_index], "-XDB"))
779
780
781
782
        {
          from_file = true;
          nra2nba = true;
        }
783
      else if (!strcmp(argv[formula_index], "-XH"))
784
785
786
        {
          from_file = true;
        }
787
      else if (!strcmp(argv[formula_index], "-XL"))
788
789
790
        {
          from_file = true;
        }
791
      else if (!strcmp(argv[formula_index], "-XN")) // now synonym for -XH
792
793
794
        {
          from_file = true;
        }
795
      else if (!strcmp(argv[formula_index], "-y"))
796
797
798
799
        {
          translation = TransFM;
          fm_symb_merge_opt = false;
        }
800
      else
801
802
803
        {
          break;
        }
804
805
    }

806
  if ((graph_run_tgba_opt)
807
      && (!echeck_inst || !expect_counter_example))
808
    {
809
      std::cerr << argv[0] << ": error: -G requires -e.\n";
810
811
812
      exit(1);
    }

813
814
815
816
  std::string input;

  if (file_opt)
    {
817
      tm.start("reading formula");
818
      if (strcmp(argv[formula_index], "-"))
819
820
821
822
823
824
825
826
827
828
829
830
831
832
        {
          std::ifstream fin(argv[formula_index]);
          if (!fin)
            {
              std::cerr << "Cannot open " << argv[formula_index] << std::endl;
              exit(2);
            }

          if (!std::getline(fin, input, '\0'))
            {
              std::cerr << "Cannot read " << argv[formula_index] << std::endl;
              exit(2);
            }
        }
833
      else
834
835
836
        {
          std::getline(std::cin, input, '\0');
        }
837
      tm.stop("reading formula");
838
839
840
841
842
843
    }
  else
    {
      input = argv[formula_index];
    }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
844
  spot::formula f = nullptr;
845
  if (!from_file) // Reading a formula, not reading an automaton from a file.
846
    {
847
      switch (translation)
848
849
850
851
852
853
854
855
856
857
858
859
860
        {
        case TransFM:
        case TransTAA:
        case TransCompo:
          {
            tm.start("parsing formula");
            auto pf = spot::parse_infix_psl(input, env, debug_opt);
            tm.stop("parsing formula");
            exit_code = pf.format_errors(std::cerr);
            f = pf.f;
          }
          break;
        }
861
    }
862

863
  if (f || from_file)
864
    {
865
      spot::twa_ptr a = nullptr;
866
      bool assume_sba = false;
867

868
      if (from_file)
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
        {
          tm.start("parsing hoa");
          spot::automaton_parser_options opts;
          opts.debug = debug_opt;
          auto daut = spot::parse_aut(input, dict, env, opts);
          tm.stop("parsing hoa");
          if (daut->format_errors(std::cerr))
            return 2;
          daut->aut->merge_edges();
          a = daut->aut;

          if (nra2nba)
            a = spot::to_generalized_buchi(daut->aut);
          assume_sba = a->is_sba().is_true();
        }
884
      else
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
        {
          spot::tl_simplifier* simp = nullptr;
          if (simpltl)
            simp = new spot::tl_simplifier(redopt, dict);

          if (simp)
            {
              tm.start("reducing formula");
              spot::formula t = simp->simplify(f);
              tm.stop("reducing formula");
              f = t;
              if (display_reduced_form)
                {
                  if (utf8_opt)
                    print_utf8_psl(std::cout, f) << '\n';
                  else
                    print_psl(std::cout, f) << '\n';
                }
              // This helps ltl_to_tgba_fm() to order BDD variables in
              // a more natural way.
              simp->clear_as_bdd_cache();
            }

          if (f.is_psl_formula()
              && !f.is_ltl_formula()
              && (translation != TransFM && translation != TransCompo))
            {
              std::cerr << "Only the FM algorithm can translate PSL formulae;"
913
                        << " I'm using it for this formula.\n";
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
              translation = TransFM;
            }

          tm.start("translating formula");
          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,
                                       fm_red ? simp : nullptr,
                                       fm_unambiguous);
              break;
            case TransCompo:
              {
                a = spot::compsusp(f, dict,
                                   cs_nowdba, cs_nosimul, cs_early_start,
                                   false, cs_wdba_smaller, cs_oblig);
                break;
              }
            case TransTAA:
              a = spot::ltl_to_taa(f, dict, containment);
              break;
            }
          tm.stop("translating formula");

          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);
            }
          delete simp;
        }
961

962
      if (opt_monitor && !scc_filter)
963
        scc_filter = true;
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
964

965
966
      // Remove dead SCCs and useless acceptance conditions before
      // degeneralization.
967
      if (scc_filter)
968
969
970
971
972
973
974
975
976
        {
          tm.start("SCC-filter");
          if (a->prop_state_acc().is_true() & !scc_filter_all)
            a = spot::scc_filter_states(ensure_digraph(a));
          else
            a = spot::scc_filter(ensure_digraph(a), scc_filter_all);
          tm.stop("SCC-filter");
          assume_sba = false;
        }
977

978
      bool wdba_minimization_is_success = false;
979
      if (opt_minimize)
980
981
982
983
984
985
986
987
988
989
990
991
        {
          auto aa = ensure_digraph(a);
          tm.start("obligation minimization");
          auto minimized = minimize_obligation(aa, f, nullptr, reject_bigger);
          tm.stop("obligation minimization");

          if (!minimized)
            {
              // if (!f)
                {
                  std::cerr << "Error: Without a formula I cannot make "
                            << "sure that the automaton built with -Rm\n"
992
                            << "       is correct.\n";
993
994
995
996
997
998
999
1000
1001
1002
1003
                  exit(2);
                }
            }
          else if (minimized == aa)
            {
              minimized = nullptr;
            }
          else
            {
              a = minimized;
              wdba_minimization_is_success = true;
Thomas Badie's avatar
Thomas Badie committed
1004
1005
              // When the minimization succeed, simulation is useless.
              reduction_dir_sim = false;
Thomas Badie's avatar
Thomas Badie committed
1006
              reduction_rev_sim = false;
Thomas Badie's avatar
Thomas Badie committed
1007
              reduction_iterated_sim = false;
1008
1009
1010
              assume_sba = true;
            }
        }
Felix Abecassis's avatar
Felix Abecassis committed
1011

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1012
      if (reduction_dir_sim && !reduction_iterated_sim)
1013
        {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1014
          tm.start("direct simulation");
1015
          a = spot::simulation(ensure_digraph(a));
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1016
          tm.stop("direct simulation");
1017
          assume_sba = false;
1018
1019
        }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1020
      if (reduction_rev_sim && !reduction_iterated_sim)
Thomas Badie's avatar
Thomas Badie committed
1021
        {
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1022
          tm.start("reverse simulation");
1023
          a = spot::cosimulation(ensure_digraph(a));
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1024
          tm.stop("reverse simulation");
1025
          assume_sba = false;
Thomas Badie's avatar
Thomas Badie committed
1026
1027
        }

Thomas Badie's avatar
Thomas Badie committed
1028

1029
1030
1031
      if (reduction_iterated_sim)
        {
          tm.start("Reduction w/ iterated simulations");
1032
          a = spot::iterated_simulations(ensure_digraph(a));
1033
          tm.stop("Reduction w/ iterated simulations");
1034
          assume_sba = false;
1035
1036
        }

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1037
      if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
1038
1039
1040
1041
1042
        {
          tm.start("SCC-filter post-sim");
          a = spot::scc_filter(ensure_digraph(a), scc_filter_all);
          tm.stop("SCC-filter post-sim");
        }
Thomas Badie's avatar
Thomas Badie committed
1043

1044
      unsigned int n_acc = a->acc().num_sets();
1045
      if (echeck_inst
1046
1047
1048
1049
1050
1051
1052
          && degeneralize_opt == NoDegen
          && n_acc > 1
          && echeck_inst->max_sets() < n_acc)
        {
          degeneralize_opt = DegenTBA;
          assume_sba = false;
        }
1053
1054

      if (!assume_sba && !opt_monitor)
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
        {
          if (degeneralize_opt == DegenTBA)
            {
              a = spot::degeneralize_tba(ensure_digraph(a),
                                         degen_reset, degen_order, degen_cache);
            }
          else if (degeneralize_opt == DegenSBA)
            {
              tm.start("degeneralization");
              a = spot::degeneralize(ensure_digraph(a),
                                     degen_reset, degen_order, degen_cache);
              tm.stop("degeneralization");
              assume_sba = true;
            }
        }
1070

1071
      if (opt_determinize && a->acc().num_sets() <= 1
1072
1073
1074
1075
1076
1077
1078
1079
1080
          && (!f || f.is_syntactic_recurrence()))
        {
          tm.start("determinization 2");
          auto determinized = tba_determinize(ensure_digraph(a), 0,
                                              opt_determinize_threshold);
          tm.stop("determinization 2");
          if (determinized)
            a = determinized;
        }
1081

1082
      if (opt_monitor)
1083
1084
1085
1086
1087
1088
1089
1090
        {
          tm.start("Monitor minimization");
          a = minimize_monitor(ensure_digraph(a));
          tm.stop("Monitor minimization");
          assume_sba = false;         // All states are accepting, so double
                                // circles in the dot output are
                                // pointless.
        }
1091

1092
      if (degeneralize_opt != NoDegen || opt_determinize)
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
        {
          if (reduction_dir_sim && !reduction_iterated_sim)
            {
              tm.start("direct simulation 2");
              a = spot::simulation(ensure_digraph(a));
              tm.stop("direct simulation 2");
              assume_sba = false;
            }

          if (reduction_rev_sim && !reduction_iterated_sim)
            {
              tm.start("reverse simulation 2");
              a = spot::cosimulation(ensure_digraph(a));
              tm.stop("reverse simulation 2");
              assume_sba = false;
            }

          if (reduction_iterated_sim)
            {
              tm.start("Reduction w/ iterated simulations");
              a = spot::iterated_simulations(ensure_digraph(a));
              tm.stop("Reduction w/ iterated simulations");
              assume_sba = false;
            }
        }
1118
1119

      if (opt_complete)
1120
1121
1122
1123
1124
        {
          tm.start("completion");
          a = complete(a);
          tm.stop("completion");
        }
1125
1126

      if (opt_dtbasat >= 0)
1127
1128
1129
1130
1131
1132
1133
1134
        {
          tm.start("dtbasat");
          auto satminimized =
            dtba_sat_synthetize(ensure_digraph(a), opt_dtbasat);
          tm.stop("dtbasat");
          if (satminimized)
            a = satminimized;
        }
1135
      else if (opt_dtwasat >= 0)
1136
1137
1138
1139
1140
1141
1142
1143
1144
        {
          tm.start("dtwasat");
          auto satminimized = dtwa_sat_minimize
            (ensure_digraph(a), opt_dtwasat,
             spot::acc_cond::acc_code::generalized_buchi(opt_dtwasat));
          tm.stop("dtwasat");
          if (satminimized)
            a = satminimized;
        }
1145

1146
      if (opt_dtwacomp)
1147
1148
        {
          tm.start("DTωA complement");
1149
          a = remove_fin(dualize(ensure_digraph(a)));
1150
1151
          tm.stop("DTωA complement");
        }
1152

1153
      if (opt_determinize || opt_dtwacomp || opt_dtbasat >= 0
1154
1155
1156
1157
1158
          || opt_dtwasat >= 0)
        {
          if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
            {
              tm.start("SCC-filter post-sim");
1159
              auto aa = down_cast<spot::const_twa_graph_ptr>(a);
1160
1161
1162
1163
1164
1165
              // Do not filter_all for SBA
              a = spot::scc_filter(aa, assume_sba ?
                                   false : scc_filter_all);
              tm.stop("SCC-filter post-sim");
            }
        }
1166

1167
      if (opt_closure)