1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2007-2019, 2021 Laboratoire de Recherche et
3 // Développement de l'Epita (LRDE).
4 // Copyright (C) 2003-2007 Laboratoire d'Informatique de Paris 6
5 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
6 // Pierre et Marie Curie.
7 //
8 // This file is part of Spot, a model checking library.
9 //
10 // Spot is free software; you can redistribute it and/or modify it
11 // 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 // (at your option) any later version.
14 //
15 // Spot is distributed in the hope that it will be useful, but WITHOUT
16 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
17 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
18 // License for more details.
19 //
20 // 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 "config.h"
24 #include <iostream>
25 #include <iomanip>
26 #include <cassert>
27 #include <fstream>
28 #include <string>
29 #include <cstdlib>
30 #include <spot/tl/print.hh>
31 #include <spot/tl/apcollect.hh>
32 #include <spot/tl/formula.hh>
33 #include <spot/tl/parse.hh>
34 #include <spot/twaalgos/ltl2tgba_fm.hh>
35 #include <spot/twaalgos/ltl2taa.hh>
36 #include <spot/twa/bddprint.hh>
37 #include <spot/twaalgos/dot.hh>
38 #include <spot/twaalgos/lbtt.hh>
39 #include <spot/twaalgos/hoa.hh>
40 #include <spot/twaalgos/degen.hh>
41 #include <spot/twa/twaproduct.hh>
42 #include <spot/parseaut/public.hh>
43 #include <spot/twaalgos/minimize.hh>
44 #include <spot/taalgos/minimize.hh>
45 #include <spot/twaalgos/neverclaim.hh>
46 #include <spot/twaalgos/sccfilter.hh>
47 #include <spot/twaalgos/strength.hh>
48 #include <spot/twaalgos/gtec/gtec.hh>
49 #include <spot/misc/timer.hh>
50 #include <spot/twaalgos/stats.hh>
51 #include <spot/twaalgos/sccinfo.hh>
52 #include <spot/twaalgos/emptiness_stats.hh>
53 #include <spot/twaalgos/sccinfo.hh>
54 #include <spot/twaalgos/isdet.hh>
55 #include <spot/twaalgos/cycles.hh>
56 #include <spot/twaalgos/isweakscc.hh>
57 #include <spot/twaalgos/simulation.hh>
58 #include <spot/twaalgos/compsusp.hh>
59 #include <spot/twaalgos/powerset.hh>
60 #include <spot/twaalgos/dualize.hh>
61 #include <spot/twaalgos/remfin.hh>
62 #include <spot/twaalgos/complete.hh>
63 #include <spot/twaalgos/dtbasat.hh>
64 #include <spot/twaalgos/dtwasat.hh>
65 #include <spot/twaalgos/stutter.hh>
66 #include <spot/twaalgos/totgba.hh>
67
68 #include <spot/taalgos/tgba2ta.hh>
69 #include <spot/taalgos/dot.hh>
70 #include <spot/taalgos/stats.hh>
71
72 static void
syntax(char * prog)73 syntax(char* prog)
74 {
75 // Display the supplied name unless it appears to be a libtool wrapper.
76 char* slash = strrchr(prog, '/');
77 if (slash && (strncmp(slash + 1, "lt-", 3) == 0))
78 prog = slash + 4;
79
80 std::cerr <<
81 "Usage: " << prog << " [-f|-l|-taa] [OPTIONS...] formula\n"
82 " " << prog << " [-f|-l|-taa] -F [OPTIONS...] file\n"
83 " " << prog << " -XH [OPTIONS...] file\n"
84 "\n"
85 "Translate an LTL formula into an automaton, or read the automaton from "
86 "a file.\n"
87 "Optionally multiply this automaton by another automaton read "
88 "from a file.\n"
89 "Output the result in various formats, or perform an emptiness check."
90 "\n\n"
91 "Input options:\n"
92 " -F read the formula from a file, not from the command line\n"
93 " -XD do not compute an automaton, read it from an ltl2dstar file\n"
94 " -XDB like -XD, and convert it to TGBA\n"
95 " -XH do not compute an automaton, read it from a HOA file\n"
96 " -XL do not compute an automaton, read it from an LBTT file\n"
97 " -XN do not compute an automaton, read it from a neverclaim file\n"
98 " -Pfile multiply the formula automaton with the TGBA read"
99 " from `file'\n"
100 " -KPfile multiply the formula automaton with the Kripke"
101 " structure from `file'\n"
102 "\n"
103 "Translation algorithm:\n"
104 " -f use Couvreur's FM algorithm for LTL (default)\n"
105 " -taa use Tauriainen's TAA-based algorithm for LTL\n"
106 " -u use Compositional translation\n"
107 "\n"
108 "Options for Couvreur's FM algorithm (-f):\n"
109 " -fr reduce formula at each step of FM\n"
110 " as specified with the -r{1..7} options\n"
111 " -fu build unambiguous automata\n"
112 " -L fair-loop approximation (implies -f)\n"
113 " -p branching postponement (implies -f)\n"
114 " -U[PROPS] consider atomic properties of the formula as "
115 "exclusive events, and\n"
116 " PROPS as unobservables events (implies -f)\n"
117 " -x try to produce a more deterministic automaton "
118 "(implies -f)\n"
119 " -y do not merge states with same symbolic representation "
120 "(implies -f)\n"
121 "\n"
122 "Options for Tauriainen's TAA-based algorithm (-taa):\n"
123 " -c enable language containment checks (implies -taa)\n"
124 "\n"
125 "Formula simplification (before translation):\n"
126 " -r1 reduce formula using basic rewriting\n"
127 " -r2 reduce formula using class of eventuality and universality\n"
128 " -r3 reduce formula using implication between sub-formulae\n"
129 " -r4 reduce formula using all above rules\n"
130 " -r5 reduce formula using tau03\n"
131 " -r6 reduce formula using tau03+\n"
132 " -r7 reduce formula using tau03+ and -r4\n"
133 " -rd display the reduced formula\n"
134 " -rD dump statistics about the simplifier cache\n"
135 " -rL disable basic rewritings producing larger formulas\n"
136 " -ru lift formulae that are eventual and universal\n"
137 "\n"
138 "Automaton degeneralization (after translation):\n"
139 " -DT degeneralize the automaton as a TBA\n"
140 " -DS degeneralize the automaton as an SBA\n"
141 " (append z/Z, o/O, l/L: to turn on/off options "
142 "(default: zol)\n "
143 " z: level resetting, o: adaptive order, "
144 "l: level cache)\n"
145 "\n"
146 "Automaton simplifications (after translation):\n"
147 " -R3 use SCCs to remove useless states and acceptance sets\n"
148 " -R3f clean more acceptance sets than -R3\n"
149 " "
150 "(prefer -R3 over -R3f if you degeneralize with -D, -DS, or -N)\n"
151 " -RDS reduce the automaton with direct simulation\n"
152 " -RRS reduce the automaton with reverse simulation\n"
153 " -RIS iterate both direct and reverse simulations\n"
154 " -Rm attempt to WDBA-minimize the automaton\n"
155 " -RM attempt to WDBA-minimize the automaton unless the "
156 "result is bigger\n"
157 " -RQ determinize a TGBA (assuming it's legal!)\n"
158 "\n"
159 "Automaton conversion:\n"
160 " -M convert into a det. minimal monitor (implies -R3 or R3b)\n"
161 " -s convert to explicit automaton, and number states in DFS order\n"
162 " -S convert to explicit automaton, and number states in BFS order\n"
163 "\n"
164 "Conversion to Testing Automaton:\n"
165 " -TA output a Generalized Testing Automaton (GTA),\n"
166 " or a Testing Automaton (TA) with -DS\n"
167 " -lv add an artificial livelock state to obtain a Single-pass (G)TA\n"
168 " -sp convert into a single-pass (G)TA without artificial "
169 "livelock state\n"
170 " -in do not use an artificial initial state\n"
171 " -TGTA output a Transition-based Generalized TA\n"
172 " -RT reduce the (G)TA/TGTA using bisimulation.\n"
173 "\n"
174 "Options for performing emptiness checks (on TGBA):\n"
175 " -e[ALGO] run emptiness check, expect and compute an "
176 "accepting run\n"
177 " -E[ALGO] run emptiness check, expect no accepting run\n"
178 " -C compute an accepting run (Counterexample) if it exists\n"
179 " -CR compute and replay an accepting run (implies -C)\n"
180 " -G graph the accepting run seen as an automaton (requires -e)\n"
181 " -m try to reduce accepting runs, in a second pass\n"
182 "Where ALGO should be one of:\n"
183 " Cou99(OPTIONS) (the default)\n"
184 " CVWY90(OPTIONS)\n"
185 " GV04(OPTIONS)\n"
186 " SE05(OPTIONS)\n"
187 " Tau03(OPTIONS)\n"
188 " Tau03_opt(OPTIONS)\n"
189 "\n"
190 "If no emptiness check is run, the automaton will be output "
191 "in dot format\nby default. This can be "
192 "changed with the following options.\n"
193 "\n"
194 "Output options (if no emptiness check):\n"
195 " -ks display statistics on the automaton (size only)\n"
196 " -kt display statistics on the automaton (size + subtransitions)\n"
197 " -K dump the graph of SCCs in dot format\n"
198 " -KC list cycles in automaton\n"
199 " -KW list weak SCCs\n"
200 " -N output the never clain for Spin (implies -DS)\n"
201 " -NN output the never clain for Spin, with commented states"
202 " (implies -DS)\n"
203 " -O tell if a formula represents a safety, guarantee, "
204 "or obligation property\n"
205 " -t output automaton in LBTT's format\n"
206 "\n"
207 "Miscellaneous options:\n"
208 " -0 produce minimal output dedicated to the paper\n"
209 " -8 output UTF-8 formulae\n"
210 " -d turn on traces during parsing\n"
211 " -T time the different phases of the translation\n"
212 " -v display the BDD variables used by the automaton\n";
213 exit(2);
214 }
215
216 static int
to_int(const char * s)217 to_int(const char* s)
218 {
219 char* endptr;
220 int res = strtol(s, &endptr, 10);
221 if (*endptr)
222 {
223 std::cerr << "Failed to parse `" << s << "' as an integer.\n";
224 exit(1);
225 }
226 return res;
227 }
228
229 static spot::twa_graph_ptr
ensure_digraph(const spot::twa_ptr & a)230 ensure_digraph(const spot::twa_ptr& a)
231 {
232 auto aa = std::dynamic_pointer_cast<spot::twa_graph>(a);
233 if (aa)
234 return aa;
235 return spot::make_twa_graph(a, spot::twa::prop_set::all());
236 }
237
238 static int
checked_main(int argc,char ** argv)239 checked_main(int argc, char** argv)
240 {
241 int exit_code = 0;
242
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 const char* echeck_algo = nullptr;
259 spot::emptiness_check_instantiator_ptr echeck_inst = nullptr;
260 bool dupexp = false;
261 bool expect_counter_example = false;
262 bool accepting_run = false;
263 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;
277 bool opt_minimize = false;
278 bool opt_determinize = false;
279 unsigned opt_determinize_threshold = 0;
280 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 bool opt_closure = false;
286 bool opt_stutterize = false;
287 const char* opt_never = nullptr;
288 const char* hoa_opt = nullptr;
289 auto& env = spot::default_environment::instance();
290 spot::atomic_prop_set* unobservables = nullptr;
291 spot::twa_ptr system_aut = nullptr;
292 auto dict = spot::make_bdd_dict();
293 spot::timer_map tm;
294 bool use_timer = false;
295 bool reduction_dir_sim = false;
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 bool opt_single_pass_emptiness_check = false;
303 bool opt_with_artificial_livelock = false;
304 bool cs_nowdba = true;
305 bool cs_wdba_smaller = false;
306 bool cs_nosimul = true;
307 bool cs_early_start = false;
308 bool cs_oblig = false;
309 bool opt_complete = false;
310 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 ++formula_index;
319
320 if (!strcmp(argv[formula_index], "-0"))
321 {
322 paper_opt = true;
323 }
324 else if (!strcmp(argv[formula_index], "-8"))
325 {
326 utf8_opt = true;
327 spot::enable_utf8();
328 }
329 else if (!strcmp(argv[formula_index], "-c"))
330 {
331 containment = true;
332 translation = TransTAA;
333 }
334 else if (!strcmp(argv[formula_index], "-C"))
335 {
336 accepting_run = true;
337 }
338 else if (!strcmp(argv[formula_index], "-CR"))
339 {
340 accepting_run = true;
341 accepting_run_replay = true;
342 }
343 else if (!strcmp(argv[formula_index], "-d"))
344 {
345 debug_opt = true;
346 }
347 else if (!strcmp(argv[formula_index], "-D"))
348 {
349 std::cerr << "-D was renamed to -DT\n";
350 abort();
351 }
352 else if (!strcmp(argv[formula_index], "-DC"))
353 {
354 opt_dtwacomp = true;
355 }
356 else if (!strncmp(argv[formula_index], "-DS", 3)
357 || !strncmp(argv[formula_index], "-DT", 3))
358 {
359 degeneralize_opt =
360 argv[formula_index][2] == 'S' ? DegenSBA : DegenTBA;
361 const char* p = argv[formula_index] + 3;
362 while (*p)
363 {
364 switch (*p++)
365 {
366 case 'o':
367 degen_order = true;
368 break;
369 case 'O':
370 degen_order = false;
371 break;
372 case 'z':
373 degen_reset = true;
374 break;
375 case 'Z':
376 degen_reset = false;
377 break;
378 case 'l':
379 degen_cache = true;
380 break;
381 case 'L':
382 degen_cache = false;
383 break;
384 }
385 }
386 }
387 else if (!strncmp(argv[formula_index], "-e", 2))
388 {
389 echeck_algo = 2 + argv[formula_index];
390 if (!*echeck_algo)
391 echeck_algo = "Cou99";
392
393 const char* err;
394 echeck_inst =
395 spot::make_emptiness_check_instantiator(echeck_algo, &err);
396 if (!echeck_inst)
397 {
398 std::cerr << "Failed to parse argument of -e near `"
399 << err << "'\n";
400 exit(2);
401 }
402 expect_counter_example = true;
403 output = -1;
404 }
405 else if (!strncmp(argv[formula_index], "-E", 2))
406 {
407 const char* echeck_algo = 2 + argv[formula_index];
408 if (!*echeck_algo)
409 echeck_algo = "Cou99";
410
411 const char* err;
412 echeck_inst =
413 spot::make_emptiness_check_instantiator(echeck_algo, &err);
414 if (!echeck_inst)
415 {
416 std::cerr << "Failed to parse argument of -e near `"
417 << err << "'\n";
418 exit(2);
419 }
420 expect_counter_example = false;
421 output = -1;
422 }
423 else if (!strcmp(argv[formula_index], "-f"))
424 {
425 translation = TransFM;
426 }
427 else if (!strcmp(argv[formula_index], "-fr"))
428 {
429 fm_red = true;
430 translation = TransFM;
431 }
432 else if (!strcmp(argv[formula_index], "-fu"))
433 {
434 fm_unambiguous = true;
435 fm_exprop_opt = true;
436 translation = TransFM;
437 }
438 else if (!strcmp(argv[formula_index], "-F"))
439 {
440 file_opt = true;
441 }
442 else if (!strcmp(argv[formula_index], "-G"))
443 {
444 accepting_run = true;
445 graph_run_tgba_opt = true;
446 }
447 else if (!strncmp(argv[formula_index], "-H", 2))
448 {
449 output = 17;
450 hoa_opt = argv[formula_index] + 2;
451 }
452 else if (!strcmp(argv[formula_index], "-ks"))
453 {
454 output = 12;
455 }
456 else if (!strcmp(argv[formula_index], "-kt"))
457 {
458 output = 13;
459 }
460 else if (!strcmp(argv[formula_index], "-K"))
461 {
462 output = 10;
463 }
464 else if (!strncmp(argv[formula_index], "-KP", 3))
465 {
466 tm.start("reading -KP's argument");
467 spot::automaton_parser_options opts;
468 opts.debug = debug_opt;
469 opts.want_kripke = true;
470 auto paut = spot::parse_aut(argv[formula_index] + 3, dict, env, opts);
471 if (paut->format_errors(std::cerr))
472 return 2;
473 system_aut = paut->ks;
474 tm.stop("reading -KP's argument");
475 }
476 else if (!strcmp(argv[formula_index], "-KC"))
477 {
478 output = 15;
479 }
480 else if (!strcmp(argv[formula_index], "-KW"))
481 {
482 output = 16;
483 }
484 else if (!strcmp(argv[formula_index], "-L"))
485 {
486 fair_loop_approx = true;
487 translation = TransFM;
488 }
489 else if (!strcmp(argv[formula_index], "-m"))
490 {
491 opt_reduce = true;
492 }
493 else if (!strcmp(argv[formula_index], "-N"))
494 {
495 degeneralize_opt = DegenSBA;
496 output = 8;
497 opt_never = nullptr;
498 }
499 else if (!strcmp(argv[formula_index], "-NN"))
500 {
501 degeneralize_opt = DegenSBA;
502 output = 8;
503 opt_never = "c";
504 }
505 else if (!strncmp(argv[formula_index], "-O", 2))
506 {
507 output = 14;
508 opt_minimize = true;
509 if (argv[formula_index][2] != 0)
510 opt_o_threshold = to_int(argv[formula_index] + 2);
511 }
512 else if (!strcmp(argv[formula_index], "-p"))
513 {
514 post_branching = true;
515 translation = TransFM;
516 }
517 else if (!strncmp(argv[formula_index], "-P", 2))
518 {
519 tm.start("reading -P's argument");
520
521 spot::automaton_parser_options opts;
522 opts.debug = debug_opt;
523 auto daut = spot::parse_aut(argv[formula_index] + 2, dict, env, opts);
524 if (daut->format_errors(std::cerr))
525 return 2;
526 daut->aut->merge_edges();
527 system_aut = daut->aut;
528 tm.stop("reading -P's argument");
529 }
530 else if (!strcmp(argv[formula_index], "-r1"))
531 {
532 simpltl = true;
533 redopt.reduce_basics = true;
534 }
535 else if (!strcmp(argv[formula_index], "-r2"))
536 {
537 simpltl = true;
538 redopt.event_univ = true;
539 }
540 else if (!strcmp(argv[formula_index], "-r3"))
541 {
542 simpltl = true;
543 redopt.synt_impl = true;
544 }
545 else if (!strcmp(argv[formula_index], "-r4"))
546 {
547 simpltl = true;
548 redopt.reduce_basics = true;
549 redopt.event_univ = true;
550 redopt.synt_impl = true;
551 }
552 else if (!strcmp(argv[formula_index], "-r5"))
553 {
554 simpltl = true;
555 redopt.containment_checks = true;
556 }
557 else if (!strcmp(argv[formula_index], "-r6"))
558 {
559 simpltl = true;
560 redopt.containment_checks = true;
561 redopt.containment_checks_stronger = true;
562 }
563 else if (!strcmp(argv[formula_index], "-r7"))
564 {
565 simpltl = true;
566 redopt.reduce_basics = true;
567 redopt.event_univ = true;
568 redopt.synt_impl = true;
569 redopt.containment_checks = true;
570 redopt.containment_checks_stronger = true;
571 }
572 else if (!strcmp(argv[formula_index], "-R1q")
573 || !strcmp(argv[formula_index], "-R1t")
574 || !strcmp(argv[formula_index], "-R2q")
575 || !strcmp(argv[formula_index], "-R2t"))
576 {
577 // For backward compatibility, make all these options
578 // equal to -RDS.
579 reduction_dir_sim = true;
580 }
581 else if (!strcmp(argv[formula_index], "-RRS"))
582 {
583 reduction_rev_sim = true;
584 }
585 else if (!strcmp(argv[formula_index], "-R3"))
586 {
587 scc_filter = true;
588 }
589 else if (!strcmp(argv[formula_index], "-R3f"))
590 {
591 scc_filter = true;
592 scc_filter_all = true;
593 }
594 else if (!strcmp(argv[formula_index], "-rd"))
595 {
596 display_reduced_form = true;
597 }
598 else if (!strcmp(argv[formula_index], "-rD"))
599 {
600 simpcache_stats = true;
601 }
602 else if (!strcmp(argv[formula_index], "-RC"))
603 {
604 opt_complete = true;
605 }
606 else if (!strcmp(argv[formula_index], "-RDS"))
607 {
608 reduction_dir_sim = true;
609 }
610 else if (!strcmp(argv[formula_index], "-RIS"))
611 {
612 reduction_iterated_sim = true;
613 }
614 else if (!strcmp(argv[formula_index], "-rL"))
615 {
616 simpltl = true;
617 redopt.reduce_basics = true;
618 redopt.reduce_size_strictly = true;
619 }
620 else if (!strncmp(argv[formula_index], "-RG", 3))
621 {
622 if (argv[formula_index][3] != 0)
623 opt_dtwasat = to_int(argv[formula_index] + 3);
624 else
625 opt_dtwasat = 0;
626 //output = -1;
627 }
628 else if (!strcmp(argv[formula_index], "-Rm"))
629 {
630 opt_minimize = true;
631 }
632 else if (!strcmp(argv[formula_index], "-RM"))
633 {
634 opt_minimize = true;
635 reject_bigger = true;
636 }
637 else if (!strncmp(argv[formula_index], "-RQ", 3))
638 {
639 opt_determinize = true;
640 if (argv[formula_index][3] != 0)
641 opt_determinize_threshold = to_int(argv[formula_index] + 3);
642 }
643 else if (!strncmp(argv[formula_index], "-RS", 3))
644 {
645 if (argv[formula_index][3] != 0)
646 opt_dtbasat = to_int(argv[formula_index] + 3);
647 else
648 opt_dtbasat = 0;
649 //output = -1;
650 }
651 else if (!strcmp(argv[formula_index], "-RT"))
652 {
653 opt_bisim_ta = true;
654 }
655 else if (!strcmp(argv[formula_index], "-ru"))
656 {
657 simpltl = true;
658 redopt.event_univ = true;
659 redopt.favor_event_univ = true;
660 }
661 else if (!strcmp(argv[formula_index], "-M"))
662 {
663 opt_monitor = true;
664 }
665 else if (!strcmp(argv[formula_index], "-S"))
666 {
667 dupexp = true;
668 }
669 else if (!strcmp(argv[formula_index], "-CL"))
670 {
671 opt_closure = true;
672 }
673 else if (!strcmp(argv[formula_index], "-ST"))
674 {
675 opt_stutterize = true;
676 }
677 else if (!strcmp(argv[formula_index], "-t"))
678 {
679 output = 6;
680 }
681 else if (!strcmp(argv[formula_index], "-T"))
682 {
683 use_timer = true;
684 }
685 else if (!strcmp(argv[formula_index], "-TA"))
686 {
687 ta_opt = true;
688 }
689 else if (!strcmp(argv[formula_index], "-TGTA"))
690 {
691 tgta_opt = true;
692 }
693 else if (!strcmp(argv[formula_index], "-lv"))
694 {
695 opt_with_artificial_livelock = true;
696 }
697 else if (!strcmp(argv[formula_index], "-sp"))
698 {
699 opt_single_pass_emptiness_check = true;
700 }
701 else if (!strcmp(argv[formula_index], "-in"))
702 {
703 opt_with_artificial_initial_state = false;
704 }
705 else if (!strcmp(argv[formula_index], "-taa"))
706 {
707 translation = TransTAA;
708 }
709 else if (!strncmp(argv[formula_index], "-U", 2))
710 {
711 unobservables = new spot::atomic_prop_set;
712 translation = TransFM;
713 // Parse -U's argument.
714 const char* tok = strtok(argv[formula_index] + 2, ", \t;");
715 while (tok)
716 {
717 unobservables->insert(env.require(tok));
718 tok = strtok(nullptr, ", \t;");
719 }
720 }
721 else if (!strncmp(argv[formula_index], "-u", 2))
722 {
723 translation = TransCompo;
724 const char* c = argv[formula_index] + 2;
725 while (*c != 0)
726 {
727 switch (*c)
728 {
729 case '2':
730 cs_nowdba = false;
731 cs_wdba_smaller = true;
732 break;
733 case 'w':
734 cs_nowdba = false;
735 cs_wdba_smaller = false;
736 break;
737 case 's':
738 cs_nosimul = false;
739 break;
740 case 'e':
741 cs_early_start = true;
742 break;
743 case 'W':
744 cs_nowdba = true;
745 break;
746 case 'S':
747 cs_nosimul = true;
748 break;
749 case 'E':
750 cs_early_start = false;
751 break;
752 case 'o':
753 cs_oblig = true;
754 break;
755 case 'O':
756 cs_oblig = false;
757 break;
758 default:
759 std::cerr << "Unknown suboption `" << *c
760 << "' for option -u\n";
761 }
762 ++c;
763 }
764 }
765 else if (!strcmp(argv[formula_index], "-v"))
766 {
767 output = 5;
768 }
769 else if (!strcmp(argv[formula_index], "-x"))
770 {
771 translation = TransFM;
772 fm_exprop_opt = true;
773 }
774 else if (!strcmp(argv[formula_index], "-XD"))
775 {
776 from_file = true;
777 }
778 else if (!strcmp(argv[formula_index], "-XDB"))
779 {
780 from_file = true;
781 nra2nba = true;
782 }
783 else if (!strcmp(argv[formula_index], "-XH"))
784 {
785 from_file = true;
786 }
787 else if (!strcmp(argv[formula_index], "-XL"))
788 {
789 from_file = true;
790 }
791 else if (!strcmp(argv[formula_index], "-XN")) // now synonym for -XH
792 {
793 from_file = true;
794 }
795 else if (!strcmp(argv[formula_index], "-y"))
796 {
797 translation = TransFM;
798 fm_symb_merge_opt = false;
799 }
800 else
801 {
802 break;
803 }
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 exit(1);
811 }
812
813 std::string input;
814
815 if (file_opt)
816 {
817 tm.start("reading formula");
818 if (strcmp(argv[formula_index], "-"))
819 {
820 std::ifstream fin(argv[formula_index]);
821 if (!fin)
822 {
823 std::cerr << "Cannot open " << argv[formula_index] << '\n';
824 exit(2);
825 }
826
827 if (!std::getline(fin, input, '\0'))
828 {
829 std::cerr << "Cannot read " << argv[formula_index] << '\n';
830 exit(2);
831 }
832 }
833 else
834 {
835 std::getline(std::cin, input, '\0');
836 }
837 tm.stop("reading formula");
838 }
839 else
840 {
841 input = argv[formula_index];
842 }
843
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 case TransFM:
850 case TransTAA:
851 case TransCompo:
852 {
853 tm.start("parsing formula");
854 auto pf = spot::parse_infix_psl(input, env, debug_opt);
855 tm.stop("parsing formula");
856 exit_code = pf.format_errors(std::cerr);
857 f = pf.f;
858 }
859 break;
860 }
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 tm.start("parsing hoa");
871 spot::automaton_parser_options opts;
872 opts.debug = debug_opt;
873 auto daut = spot::parse_aut(input, dict, env, opts);
874 tm.stop("parsing hoa");
875 if (daut->format_errors(std::cerr))
876 return 2;
877 daut->aut->merge_edges();
878 a = daut->aut;
879
880 if (nra2nba)
881 a = spot::to_generalized_buchi(daut->aut);
882 assume_sba = a->is_sba().is_true();
883 }
884 else
885 {
886 spot::tl_simplifier* simp = nullptr;
887 if (simpltl)
888 simp = new spot::tl_simplifier(redopt, dict);
889
890 if (simp)
891 {
892 tm.start("reducing formula");
893 spot::formula t = simp->simplify(f);
894 tm.stop("reducing formula");
895 f = t;
896 if (display_reduced_form)
897 {
898 if (utf8_opt)
899 print_utf8_psl(std::cout, f) << '\n';
900 else
901 print_psl(std::cout, f) << '\n';
902 }
903 // This helps ltl_to_tgba_fm() to order BDD variables in
904 // a more natural way.
905 simp->clear_as_bdd_cache();
906 }
907
908 if (f.is_psl_formula()
909 && !f.is_ltl_formula()
910 && (translation != TransFM && translation != TransCompo))
911 {
912 std::cerr << "Only the FM algorithm can translate PSL formulae;"
913 << " I'm using it for this formula.\n";
914 translation = TransFM;
915 }
916
917 tm.start("translating formula");
918 switch (translation)
919 {
920 case TransFM:
921 a = spot::ltl_to_tgba_fm(f, dict, fm_exprop_opt,
922 fm_symb_merge_opt,
923 post_branching,
924 fair_loop_approx,
925 unobservables,
926 fm_red ? simp : nullptr,
927 fm_unambiguous);
928 break;
929 case TransCompo:
930 {
931 a = spot::compsusp(f, dict,
932 cs_nowdba, cs_nosimul, cs_early_start,
933 false, cs_wdba_smaller, cs_oblig);
934 break;
935 }
936 case TransTAA:
937 a = spot::ltl_to_taa(f, dict, containment);
938 break;
939 }
940 tm.stop("translating formula");
941
942 if (simp && simpcache_stats)
943 {
944 simp->print_stats(std::cerr);
945 bddStat s;
946 bdd_stats(&s);
947 std::cerr << "BDD produced: " << s.produced
948 << "\n nodenum: " << s.nodenum
949 << "\n maxnodenum: " << s.maxnodenum
950 << "\n freenodes: " << s.freenodes
951 << "\n minfreenodes: " << s.minfreenodes
952 << "\n varnum: " << s.varnum
953 << "\n cachesize: " << s.cachesize
954 << "\n gbcnum: " << s.gbcnum
955 << '\n';
956 bdd_fprintstat(stderr);
957 dict->dump(std::cerr);
958 }
959 delete simp;
960 }
961
962 if (opt_monitor && !scc_filter)
963 scc_filter = true;
964
965 // Remove dead SCCs and useless acceptance conditions before
966 // degeneralization.
967 if (scc_filter)
968 {
969 tm.start("SCC-filter");
970 if (a->prop_state_acc().is_true() & !scc_filter_all)
971 a = spot::scc_filter_states(ensure_digraph(a));
972 else
973 a = spot::scc_filter(ensure_digraph(a), scc_filter_all);
974 tm.stop("SCC-filter");
975 assume_sba = false;
976 }
977
978 bool wdba_minimization_is_success = false;
979 if (opt_minimize)
980 {
981 auto aa = ensure_digraph(a);
982 tm.start("obligation minimization");
983 auto minimized = minimize_obligation(aa, f, nullptr, reject_bigger);
984 tm.stop("obligation minimization");
985
986 if (!minimized)
987 {
988 // if (!f)
989 {
990 std::cerr << "Error: Without a formula I cannot make "
991 << "sure that the automaton built with -Rm\n"
992 << " is correct.\n";
993 exit(2);
994 }
995 }
996 else if (minimized == aa)
997 {
998 minimized = nullptr;
999 }
1000 else
1001 {
1002 a = minimized;
1003 wdba_minimization_is_success = true;
1004 // When the minimization succeed, simulation is useless.
1005 reduction_dir_sim = false;
1006 reduction_rev_sim = false;
1007 reduction_iterated_sim = false;
1008 assume_sba = true;
1009 }
1010 }
1011
1012 if (reduction_dir_sim && !reduction_iterated_sim)
1013 {
1014 tm.start("direct simulation");
1015 a = spot::simulation(ensure_digraph(a));
1016 tm.stop("direct simulation");
1017 assume_sba = false;
1018 }
1019
1020 if (reduction_rev_sim && !reduction_iterated_sim)
1021 {
1022 tm.start("reverse simulation");
1023 a = spot::cosimulation(ensure_digraph(a));
1024 tm.stop("reverse simulation");
1025 assume_sba = false;
1026 }
1027
1028
1029 if (reduction_iterated_sim)
1030 {
1031 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
1037 if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
1038 {
1039 tm.start("SCC-filter post-sim");
1040 a = spot::scc_filter(ensure_digraph(a), scc_filter_all);
1041 tm.stop("SCC-filter post-sim");
1042 }
1043
1044 unsigned int n_acc = a->acc().num_sets();
1045 if (echeck_inst
1046 && degeneralize_opt == NoDegen
1047 && n_acc > 1
1048 && echeck_inst->max_sets() < n_acc)
1049 {
1050 degeneralize_opt = DegenTBA;
1051 assume_sba = false;
1052 }
1053
1054 if (!assume_sba && !opt_monitor)
1055 {
1056 if (degeneralize_opt == DegenTBA)
1057 {
1058 a = spot::degeneralize_tba(ensure_digraph(a),
1059 degen_reset, degen_order, degen_cache);
1060 }
1061 else if (degeneralize_opt == DegenSBA)
1062 {
1063 tm.start("degeneralization");
1064 a = spot::degeneralize(ensure_digraph(a),
1065 degen_reset, degen_order, degen_cache);
1066 tm.stop("degeneralization");
1067 assume_sba = true;
1068 }
1069 }
1070
1071 if (opt_determinize && a->acc().num_sets() <= 1
1072 && (!f || f.is_syntactic_recurrence()))
1073 {
1074 tm.start("determinization 2");
1075 auto determinized = tba_determinize(ensure_digraph(a), 0,
1076 opt_determinize_threshold);
1077 tm.stop("determinization 2");
1078 if (determinized)
1079 a = determinized;
1080 }
1081
1082 if (opt_monitor)
1083 {
1084 tm.start("Monitor minimization");
1085 a = minimize_monitor(ensure_digraph(a));
1086 tm.stop("Monitor minimization");
1087 assume_sba = false; // All states are accepting, so double
1088 // circles in the dot output are
1089 // pointless.
1090 }
1091
1092 if (degeneralize_opt != NoDegen || opt_determinize)
1093 {
1094 if (reduction_dir_sim && !reduction_iterated_sim)
1095 {
1096 tm.start("direct simulation 2");
1097 a = spot::simulation(ensure_digraph(a));
1098 tm.stop("direct simulation 2");
1099 assume_sba = false;
1100 }
1101
1102 if (reduction_rev_sim && !reduction_iterated_sim)
1103 {
1104 tm.start("reverse simulation 2");
1105 a = spot::cosimulation(ensure_digraph(a));
1106 tm.stop("reverse simulation 2");
1107 assume_sba = false;
1108 }
1109
1110 if (reduction_iterated_sim)
1111 {
1112 tm.start("Reduction w/ iterated simulations");
1113 a = spot::iterated_simulations(ensure_digraph(a));
1114 tm.stop("Reduction w/ iterated simulations");
1115 assume_sba = false;
1116 }
1117 }
1118
1119 if (opt_complete)
1120 {
1121 tm.start("completion");
1122 a = complete(a);
1123 tm.stop("completion");
1124 }
1125
1126 if (opt_dtbasat >= 0)
1127 {
1128 tm.start("dtbasat");
1129 auto satminimized =
1130 dtba_sat_synthetize(ensure_digraph(a), opt_dtbasat);
1131 tm.stop("dtbasat");
1132 if (satminimized)
1133 a = satminimized;
1134 }
1135 else if (opt_dtwasat >= 0)
1136 {
1137 tm.start("dtwasat");
1138 auto satminimized = dtwa_sat_minimize
1139 (ensure_digraph(a), opt_dtwasat,
1140 spot::acc_cond::acc_code::generalized_buchi(opt_dtwasat));
1141 tm.stop("dtwasat");
1142 if (satminimized)
1143 a = satminimized;
1144 }
1145
1146 if (opt_dtwacomp)
1147 {
1148 tm.start("DTωA complement");
1149 a = remove_fin(dualize(ensure_digraph(a)));
1150 tm.stop("DTωA complement");
1151 }
1152
1153 if (opt_determinize || opt_dtwacomp || opt_dtbasat >= 0
1154 || opt_dtwasat >= 0)
1155 {
1156 if (scc_filter && (reduction_dir_sim || reduction_rev_sim))
1157 {
1158 tm.start("SCC-filter post-sim");
1159 auto aa = spot::down_cast<spot::const_twa_graph_ptr>(a);
1160 // Do not filter_all for SBA
1161 a = spot::scc_filter(aa, assume_sba ?
1162 false : scc_filter_all);
1163 tm.stop("SCC-filter post-sim");
1164 }
1165 }
1166
1167 if (opt_closure)
1168 {
1169 a = closure(ensure_digraph(a));
1170 }
1171
1172 if (opt_stutterize)
1173 {
1174 a = sl(ensure_digraph(a));
1175 }
1176
1177 if (opt_monitor)
1178 {
1179 tm.start("Monitor minimization");
1180 a = minimize_monitor(ensure_digraph(a));
1181 tm.stop("Monitor minimization");
1182 assume_sba = false; // All states are accepting, so double
1183 // circles in the dot output are
1184 // pointless.
1185 }
1186
1187 if (dupexp)
1188 a = make_twa_graph(a, spot::twa::prop_set::all());
1189
1190 //TA, STA, GTA, SGTA and TGTA
1191 if (ta_opt || tgta_opt)
1192 {
1193 bdd atomic_props_set_bdd = atomic_prop_collect_as_bdd(f, a);
1194
1195 if (ta_opt)
1196 {
1197 tm.start("conversion to TA");
1198 auto testing_automaton
1199 = tgba_to_ta(a, atomic_props_set_bdd, degeneralize_opt
1200 == DegenSBA, opt_with_artificial_initial_state,
1201 opt_single_pass_emptiness_check,
1202 opt_with_artificial_livelock);
1203 tm.stop("conversion to TA");
1204
1205 if (opt_bisim_ta)
1206 {
1207 tm.start("TA bisimulation");
1208 testing_automaton = minimize_ta(testing_automaton);
1209 tm.stop("TA bisimulation");
1210 }
1211
1212 if (output != -1)
1213 {
1214 tm.start("producing output");
1215 switch (output)
1216 {
1217 case 0:
1218 spot::print_dot(std::cout, testing_automaton);
1219 break;
1220 case 12:
1221 stats_reachable(testing_automaton).dump(std::cout);
1222 break;
1223 default:
1224 std::cerr << "unsupported output option\n";
1225 exit(1);
1226 }
1227 tm.stop("producing output");
1228 }
1229 a = nullptr;
1230 output = -1;
1231 }
1232 if (tgta_opt)
1233 {
1234 auto tgta = tgba_to_tgta(a, atomic_props_set_bdd);
1235 if (opt_bisim_ta)
1236 {
1237 tm.start("TA bisimulation");
1238 a = minimize_tgta(tgta);
1239 tm.stop("TA bisimulation");
1240 }
1241 else
1242 {
1243 a = tgta;
1244 }
1245
1246 if (output != -1)
1247 {
1248 tm.start("producing output");
1249 switch (output)
1250 {
1251 case 0:
1252 spot::print_dot(std::cout, std::static_pointer_cast
1253 <spot::tgta_explicit>(a)->get_ta());
1254 break;
1255 case 12:
1256 stats_reachable(a).dump(std::cout);
1257 break;
1258 default:
1259 std::cerr << "unsupported output option\n";
1260 exit(1);
1261 }
1262 tm.stop("producing output");
1263 }
1264 output = -1;
1265 }
1266 }
1267
1268 if (system_aut)
1269 {
1270 a = spot::otf_product(system_aut, a);
1271
1272 assume_sba = false;
1273
1274 unsigned int n_acc = a->acc().num_sets();
1275 if (echeck_inst
1276 && degeneralize_opt == NoDegen
1277 && n_acc > 1
1278 && echeck_inst->max_sets() < n_acc)
1279 degeneralize_opt = DegenTBA;
1280 if (degeneralize_opt == DegenTBA)
1281 {
1282 tm.start("degeneralize product");
1283 a = spot::degeneralize_tba(ensure_digraph(a),
1284 degen_reset,
1285 degen_order,
1286 degen_cache);
1287 tm.stop("degeneralize product");
1288 }
1289 else if (degeneralize_opt == DegenSBA)
1290 {
1291 tm.start("degeneralize product");
1292 a = spot::degeneralize(ensure_digraph(a),
1293 degen_reset,
1294 degen_order,
1295 degen_cache);
1296 tm.stop("degeneralize product");
1297 assume_sba = true;
1298 }
1299 }
1300
1301
1302 if (echeck_inst
1303 && (a->acc().num_sets() < echeck_inst->min_sets()))
1304 {
1305 if (!paper_opt)
1306 {
1307 std::cerr << echeck_algo << " requires at least "
1308 << echeck_inst->min_sets()
1309 << " acceptance sets.\n";
1310 exit(1);
1311 }
1312 else
1313 {
1314 std::cout << std::endl;
1315 exit(0);
1316 }
1317 }
1318
1319 if (f)
1320 a->set_named_prop("automaton-name", new std::string(str_psl(f)));
1321
1322 if (output != -1)
1323 {
1324 tm.start("producing output");
1325 switch (output)
1326 {
1327 case 0:
1328 spot::print_dot(std::cout, a);
1329 break;
1330 case 5:
1331 a->get_dict()->dump(std::cout);
1332 break;
1333 case 6:
1334 spot::print_lbtt(std::cout, a);
1335 break;
1336 case 8:
1337 {
1338 assert(degeneralize_opt == DegenSBA);
1339 if (assume_sba)
1340 spot::print_never_claim(std::cout, a, opt_never);
1341 else
1342 {
1343 // It is possible that we have applied other
1344 // operations to the automaton since its initial
1345 // degeneralization. Let's degeneralize again!
1346 auto s = spot::degeneralize(ensure_digraph(a), degen_reset,
1347 degen_order, degen_cache);
1348 spot::print_never_claim(std::cout, s, opt_never);
1349 }
1350 break;
1351 }
1352 case 10:
1353 dump_scc_info_dot(std::cout, ensure_digraph(a));
1354 break;
1355 case 12:
1356 stats_reachable(a).dump(std::cout);
1357 break;
1358 case 13:
1359 sub_stats_reachable(a).dump(std::cout);
1360 std::cout << "nondeterministic states: "
1361 << count_nondet_states(ensure_digraph(a)) << std::endl;
1362 break;
1363 case 14:
1364 if (!wdba_minimization_is_success)
1365 {
1366 std::cout << "this is not an obligation property";
1367 auto tmp = tba_determinize_check(ensure_digraph(a),
1368 0, opt_o_threshold,
1369 f, nullptr);
1370 if (tmp && tmp != a)
1371 std::cout << ", but it is a recurrence property";
1372 }
1373 else
1374 {
1375 bool g = is_terminal_automaton(ensure_digraph(a),
1376 nullptr, true);
1377 bool s = is_safety_automaton(ensure_digraph(a));
1378 if (g && !s)
1379 {
1380 std::cout << "this is a guarantee property (hence, "
1381 << "an obligation property)";
1382 }
1383 else if (s && !g)
1384 {
1385 std::cout << "this is a safety property (hence, "
1386 << "an obligation property)";
1387 }
1388 else if (s && g)
1389 {
1390 std::cout << "this is a guarantee and a safety property"
1391 << " (and of course an obligation property)";
1392 }
1393 else
1394 {
1395 std::cout << "this is an obligation property that is "
1396 << "neither a safety nor a guarantee";
1397 }
1398 }
1399 std::cout << std::endl;
1400
1401 break;
1402 case 15:
1403 {
1404 spot::scc_info m(ensure_digraph(a));
1405 spot::enumerate_cycles c(m);
1406 unsigned max = m.scc_count();
1407 for (unsigned n = 0; n < max; ++n)
1408 {
1409 std::cout << "Cycles in SCC #" << n << std::endl;
1410 c.run(n);
1411 }
1412 break;
1413 }
1414 case 16:
1415 {
1416 spot::scc_info m(ensure_digraph(a));
1417 unsigned max = m.scc_count();
1418 for (unsigned n = 0; n < max; ++n)
1419 {
1420 bool w = spot::is_weak_scc(m, n);
1421 std::cout << "SCC #" << n
1422 << (w ? " is weak" : " is not weak")
1423 << std::endl;
1424 }
1425 break;
1426 }
1427 case 17:
1428 {
1429 print_hoa(std::cout, a, hoa_opt) << '\n';
1430 break;
1431 }
1432 default:
1433 SPOT_UNREACHABLE();
1434 }
1435 tm.stop("producing output");
1436 }
1437
1438 if (echeck_inst)
1439 {
1440 auto ec = echeck_inst->instantiate(a);
1441 bool search_many = echeck_inst->options().get("repeated");
1442 assert(ec);
1443 do
1444 {
1445 tm.start("running emptiness check");
1446 auto res = ec->check();
1447 tm.stop("running emptiness check");
1448
1449 if (paper_opt)
1450 {
1451 std::ios::fmtflags old = std::cout.flags();
1452 std::cout << std::left << std::setw(25)
1453 << echeck_algo << ", ";
1454 spot::twa_statistics a_size =
1455 spot::stats_reachable(ec->automaton());
1456 std::cout << std::right << std::setw(10)
1457 << a_size.states << ", "
1458 << std::right << std::setw(10)
1459 << a_size.edges << ", ";
1460 std::cout << ec->automaton()->acc().num_sets()
1461 << ", ";
1462 auto ecs = ec->emptiness_check_statistics();
1463 if (ecs)
1464 std::cout << std::right << std::setw(10)
1465 << ecs->states() << ", "
1466 << std::right << std::setw(10)
1467 << ecs->transitions() << ", "
1468 << std::right << std::setw(10)
1469 << ecs->max_depth();
1470 else
1471 std::cout << "no stats, , ";
1472 if (res)
1473 std::cout << ", accepting run found";
1474 else
1475 std::cout << ", no accepting run found";
1476 std::cout << std::endl;
1477 std::cout << std::setiosflags(old);
1478 }
1479 else
1480 {
1481 if (!graph_run_tgba_opt)
1482 ec->print_stats(std::cout);
1483 if (expect_counter_example != !!res &&
1484 (!expect_counter_example || ec->safe()))
1485 exit_code = 1;
1486
1487 if (!res)
1488 {
1489 std::cout << "no accepting run found";
1490 if (!ec->safe() && expect_counter_example)
1491 {
1492 std::cout << " even if expected\n";
1493 std::cout << "this may be due to the use of the bit"
1494 << " state hashing technique\n";
1495 std::cout << "you can try to increase the heap size "
1496 << "or use an explicit storage"
1497 << std::endl;
1498 }
1499 std::cout << std::endl;
1500 break;
1501 }
1502 else if (accepting_run)
1503 {
1504
1505 tm.start("computing accepting run");
1506 auto run = res->accepting_run();
1507 tm.stop("computing accepting run");
1508
1509 if (!run)
1510 {
1511 std::cout << "an accepting run exists\n";
1512 }
1513 else
1514 {
1515 if (opt_reduce)
1516 {
1517 tm.start("reducing accepting run");
1518 run = run->reduce();
1519 tm.stop("reducing accepting run");
1520 }
1521 if (accepting_run_replay)
1522 {
1523 tm.start("replaying acc. run");
1524 if (!run->replay(std::cout, true))
1525 exit_code = 1;
1526 tm.stop("replaying acc. run");
1527 }
1528 else
1529 {
1530 tm.start("printing accepting run");
1531 if (graph_run_tgba_opt)
1532 spot::print_dot(std::cout, run->as_twa());
1533 else
1534 std::cout << *run;
1535 tm.stop("printing accepting run");
1536 }
1537 }
1538 }
1539 else
1540 {
1541 std::cout << "an accepting run exists "
1542 << "(use -C to print it)\n";
1543 }
1544 }
1545 }
1546 while (search_many);
1547 }
1548 }
1549 else
1550 {
1551 exit_code = 1;
1552 }
1553
1554 if (use_timer)
1555 tm.print(std::cout);
1556
1557 delete unobservables;
1558 return exit_code;
1559 }
1560
1561
1562 int
main(int argc,char ** argv)1563 main(int argc, char** argv)
1564 {
1565 int exit_code = checked_main(argc, argv);
1566 assert(spot::fnode::instances_check());
1567 return exit_code;
1568 }
1569