1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2012-2020 Laboratoire de Recherche et Développement
3 // de l'Epita (LRDE).
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20
21 #include "common_sys.hh"
22
23 #include <string>
24 #include <iostream>
25 #include <sstream>
26 #include <cstdlib>
27 #include <cstdio>
28 #include <argp.h>
29 #include <unistd.h>
30 #include <cmath>
31 #include <sys/wait.h>
32 #include "error.h"
33 #include "argmatch.h"
34
35 #include "common_setup.hh"
36 #include "common_cout.hh"
37 #include "common_conv.hh"
38 #include "common_trans.hh"
39 #include "common_file.hh"
40 #include "common_finput.hh"
41 #include "common_hoaread.hh"
42 #include "common_aoutput.hh"
43 #include "common_color.hh"
44 #include <spot/parseaut/public.hh>
45 #include <spot/tl/print.hh>
46 #include <spot/tl/apcollect.hh>
47 #include <spot/tl/mutation.hh>
48 #include <spot/tl/relabel.hh>
49 #include <spot/twaalgos/lbtt.hh>
50 #include <spot/twaalgos/hoa.hh>
51 #include <spot/twaalgos/product.hh>
52 #include <spot/twaalgos/remfin.hh>
53 #include <spot/twaalgos/gtec/gtec.hh>
54 #include <spot/twaalgos/randomgraph.hh>
55 #include <spot/twaalgos/sccinfo.hh>
56 #include <spot/twaalgos/isweakscc.hh>
57 #include <spot/twaalgos/word.hh>
58 #include <spot/twaalgos/complement.hh>
59 #include <spot/twaalgos/cleanacc.hh>
60 #include <spot/twaalgos/alternation.hh>
61 #include <spot/misc/formater.hh>
62 #include <spot/twaalgos/stats.hh>
63 #include <spot/twaalgos/isdet.hh>
64 #include <spot/twaalgos/isunamb.hh>
65 #include <spot/twaalgos/postproc.hh>
66 #include <spot/misc/escape.hh>
67 #include <spot/misc/hash.hh>
68 #include <spot/misc/random.hh>
69 #include <spot/misc/tmpfile.hh>
70 #include <spot/misc/timer.hh>
71
72 const char argp_program_doc[] ="\
73 Call several LTL/PSL translators and cross-compare their output to detect \
74 bugs, or to gather statistics. The list of formulas to use should be \
75 supplied on standard input, or using the -f or -F options.\v\
76 Exit status:\n\
77 0 everything went fine (without --fail-on-timeout, timeouts are OK)\n\
78 1 some translator failed to output something we understand, or failed\n\
79 sanity checks (statistics were output nonetheless)\n\
80 2 ltlcross aborted on error\n\
81 ";
82
83 enum {
84 OPT_AMBIGUOUS = 256,
85 OPT_AUTOMATA,
86 OPT_BOGUS,
87 OPT_CSV,
88 OPT_DENSITY,
89 OPT_DET_MAX_STATES,
90 OPT_DET_MAX_EDGES,
91 OPT_DUPS,
92 OPT_FAIL_ON_TIMEOUT,
93 OPT_GRIND,
94 OPT_IGNORE_EXEC_FAIL,
95 OPT_JSON,
96 OPT_NOCHECKS,
97 OPT_NOCOMP,
98 OPT_OMIT,
99 OPT_PRODUCTS,
100 OPT_REFERENCE,
101 OPT_SAVE_INCLUSION_PRODUCTS,
102 OPT_SEED,
103 OPT_STATES,
104 OPT_STOP_ERR,
105 OPT_STRENGTH,
106 OPT_VERBOSE,
107 };
108
109 static const argp_option options[] =
110 {
111 { "reference", OPT_REFERENCE, "COMMANDFMT", 0,
112 "register one translator and assume it is correct (do not"
113 "check it for error, but use it to check other translators)", 2 },
114 /**************************************************/
115 { nullptr, 0, nullptr, 0, "ltlcross behavior:", 5 },
116 { "allow-dups", OPT_DUPS, nullptr, 0,
117 "translate duplicate formulas in input", 0 },
118 { "no-checks", OPT_NOCHECKS, nullptr, 0,
119 "do not perform any sanity checks (negated formulas "
120 "will not be translated)", 0 },
121 { "no-complement", OPT_NOCOMP, nullptr, 0,
122 "do not complement deterministic automata to perform extra checks", 0 },
123 { "determinize", 'D', nullptr, 0,
124 "always determinize non-deterministic automata so that they"
125 "can be complemented; also implicitly sets --products=0", 0 },
126 { "determinize-max-states", OPT_DET_MAX_STATES, "N", 0,
127 "attempt to determinize non-deterministic automata so they can be "
128 "complemented, unless the deterministic automaton would have more "
129 "than N states. Without this option or -D, determinizations "
130 "are attempted up to 500 states.", 0 },
131 { "determinize-max-edges", OPT_DET_MAX_EDGES, "N", 0,
132 "attempt to determinize non-deterministic automata so they can be "
133 "complemented, unless the deterministic automaton would have more "
134 "than N edges. Without this option or -D, determinizations "
135 "are attempted up to 5000 edges.", 0 },
136 { "stop-on-error", OPT_STOP_ERR, nullptr, 0,
137 "stop on first execution error or failure to pass"
138 " sanity checks (timeouts are OK)", 0 },
139 { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0,
140 "ignore automata from translators that return with a non-zero exit code,"
141 " but do not flag this as an error", 0 },
142 { "fail-on-timeout", OPT_FAIL_ON_TIMEOUT, nullptr, 0,
143 "consider timeouts as errors", 0 },
144 /**************************************************/
145 { nullptr, 0, nullptr, 0, "State-space generation:", 6 },
146 { "states", OPT_STATES, "INT", 0,
147 "number of the states in the state-spaces (200 by default)", 0 },
148 { "density", OPT_DENSITY, "FLOAT", 0,
149 "probability, between 0.0 and 1.0, to add a transition between "
150 "two states (0.1 by default)", 0 },
151 { "seed", OPT_SEED, "INT", 0,
152 "seed for the random number generator (0 by default)", 0 },
153 { "products", OPT_PRODUCTS, "[+]INT", 0,
154 "number of products to perform (1 by default), statistics will be "
155 "averaged unless the number is prefixed with '+'", 0 },
156 /**************************************************/
157 { nullptr, 0, nullptr, 0, "Statistics output:", 7 },
158 { "json", OPT_JSON, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
159 "output statistics as JSON in FILENAME or on standard output", 0 },
160 { "csv", OPT_CSV, "[>>]FILENAME", OPTION_ARG_OPTIONAL,
161 "output statistics as CSV in FILENAME or on standard output "
162 "(if '>>' is used to request append mode, the header line is "
163 "not output)", 0 },
164 { "omit-missing", OPT_OMIT, nullptr, 0,
165 "do not output statistics for timeouts or failed translations", 0 },
166 { "automata", OPT_AUTOMATA, nullptr, 0,
167 "store automata (in the HOA format) into the CSV or JSON output", 0 },
168 { "strength", OPT_STRENGTH, nullptr, 0,
169 "output statistics about SCC strengths (non-accepting, terminal, weak, "
170 "strong) [not supported for alternating automata]", 0 },
171 { "ambiguous", OPT_AMBIGUOUS, nullptr, 0,
172 "output statistics about ambiguous automata "
173 "[not supported for alternating automata]", 0 },
174 { "unambiguous", 0, nullptr, OPTION_ALIAS, nullptr, 0 },
175 /**************************************************/
176 { nullptr, 0, nullptr, 0, "Output options:", -15 },
177 { "grind", OPT_GRIND, "[>>]FILENAME", 0,
178 "for each formula for which a problem was detected, write a simpler " \
179 "formula that fails on the same test in FILENAME", 0 },
180 { "quiet", 'q', nullptr, 0,
181 "suppress all normal output in absence of error", 0 },
182 { "save-bogus", OPT_BOGUS, "[>>]FILENAME", 0,
183 "save formulas for which problems were detected in FILENAME", 0 },
184 { "save-inclusion-products", OPT_SAVE_INCLUSION_PRODUCTS, "[>>]FILENAME",
185 0, "save automata representing products built to check inclusion "
186 "between automata", 0 },
187 { "verbose", OPT_VERBOSE, nullptr, 0,
188 "print what is being done, for debugging", 0 },
189 { nullptr, 0, nullptr, 0,
190 "If an output FILENAME is prefixed with '>>', it is open "
191 "in append mode instead of being truncated.", -14 },
192 /**************************************************/
193 { nullptr, 0, nullptr, 0, "Miscellaneous options:", -1 },
194 { nullptr, 0, nullptr, 0, nullptr, 0 }
195 };
196
197 const struct argp_child children[] =
198 {
199 { &finput_argp, 0, nullptr, 1 },
200 { &trans_argp, 0, nullptr, 0 },
201 { &hoaread_argp, 0, "Parsing of automata:", 4 },
202 { &color_argp, 0, nullptr, 0 },
203 { &misc_argp, 0, nullptr, -1 },
204 { nullptr, 0, nullptr, 0 }
205 };
206
207 static unsigned states = 200;
208 static float density = 0.1;
209 static const char* json_output = nullptr;
210 static const char* csv_output = nullptr;
211 static bool want_stats = false;
212 static bool allow_dups = false;
213 static bool no_checks = false;
214 static bool no_complement = false;
215 static bool determinize = false;
216 static bool max_det_states_given = false;
217 static bool max_det_edges_given = false;
218 static unsigned max_det_states = 500U;
219 static unsigned max_det_edges = 5000U;
220 static bool stop_on_error = false;
221 static int seed = 0;
222 static unsigned products = 1;
223 static bool products_avg = true;
224 static bool opt_omit = false;
225 static const char* bogus_output_filename = nullptr;
226 static output_file* bogus_output = nullptr;
227 static const char* grind_output_filename = nullptr;
228 static output_file* grind_output = nullptr;
229 static const char* saved_inclusion_products_filename = nullptr;
230 static output_file* saved_inclusion_products = nullptr;
231 static bool verbose = false;
232 static bool quiet = false;
233 static bool ignore_exec_fail = false;
234 static unsigned ignored_exec_fail = 0;
235 static bool fail_on_timeout = false;
236 static bool opt_automata = false;
237 static bool opt_strength = false;
238 static bool opt_ambiguous = false;
239
240 static bool global_error_flag = false;
241 static unsigned oom_count = 0U;
242
243 static std::ostream&
global_error()244 global_error()
245 {
246 global_error_flag = true;
247 std::cerr << bright_red;
248 return std::cerr;
249 }
250
251 static std::ostream&
example()252 example()
253 {
254 std::cerr << bold_std;
255 return std::cerr;
256 }
257
258 static void
end_error()259 end_error()
260 {
261 std::cerr << reset_color;
262 }
263
264
265 struct statistics
266 {
statisticsstatistics267 statistics()
268 : ok(false),
269 alternating(false),
270 status_str(nullptr),
271 status_code(0),
272 time(0),
273 states(0),
274 edges(0),
275 transitions(0),
276 acc(0),
277 scc(0),
278 nonacc_scc(0),
279 terminal_scc(0),
280 weak_scc(0),
281 strong_scc(0),
282 nondetstates(0),
283 nondeterministic(false),
284 terminal_aut(false),
285 weak_aut(false),
286 strong_aut(false)
287 {
288 }
289
290 // If OK is false, only the status_str, status_code, and time fields
291 // should be valid.
292 bool ok;
293 bool alternating;
294 const char* status_str;
295 int status_code;
296 double time;
297 unsigned states;
298 unsigned edges;
299 unsigned long long transitions;
300 unsigned acc;
301 unsigned scc;
302 unsigned nonacc_scc;
303 unsigned terminal_scc;
304 unsigned weak_scc;
305 unsigned strong_scc;
306 unsigned nondetstates;
307 bool nondeterministic;
308 bool terminal_aut;
309 bool weak_aut;
310 bool strong_aut;
311 std::vector<double> product_states;
312 std::vector<double> product_transitions;
313 std::vector<double> product_scc;
314 bool ambiguous;
315 bool complete;
316 std::string hoa_str;
317
318 static void
fieldsstatistics319 fields(std::ostream& os, bool show_exit)
320 {
321 if (show_exit)
322 os << "\"exit_status\",\"exit_code\",";
323 os << ("\"time\","
324 "\"states\","
325 "\"edges\","
326 "\"transitions\","
327 "\"acc\","
328 "\"scc\",");
329 if (opt_strength)
330 os << ("\"nonacc_scc\","
331 "\"terminal_scc\","
332 "\"weak_scc\","
333 "\"strong_scc\",");
334 os << ("\"nondet_states\","
335 "\"nondet_aut\",");
336 if (opt_strength)
337 os << ("\"terminal_aut\","
338 "\"weak_aut\","
339 "\"strong_aut\",");
340 if (opt_ambiguous)
341 os << "\"ambiguous_aut\",";
342 os << "\"complete_aut\"";
343 size_t m = products_avg ? 1U : products;
344 for (size_t i = 0; i < m; ++i)
345 os << ",\"product_states\",\"product_transitions\",\"product_scc\"";
346 if (opt_automata)
347 os << ",\"automaton\"";
348 }
349
350 void
to_csvstatistics351 to_csv(std::ostream& os, bool show_exit, const char* na = "",
352 bool csv_escape = true)
353 {
354 if (show_exit)
355 os << '"' << status_str << "\"," << status_code << ',';
356 os << time << ',';
357 if (ok)
358 {
359 os << states << ','
360 << edges << ','
361 << transitions << ','
362 << acc << ','
363 << scc << ',';
364 if (opt_strength)
365 {
366 if (alternating)
367 os << ",,,,";
368 else
369 os << nonacc_scc << ','
370 << terminal_scc << ','
371 << weak_scc << ','
372 << strong_scc << ',';
373 }
374 os << nondetstates << ','
375 << nondeterministic << ',';
376 if (opt_strength)
377 {
378 if (alternating)
379 os << ",,,";
380 else
381 os << terminal_aut << ','
382 << weak_aut << ','
383 << strong_aut << ',';
384 }
385 if (opt_ambiguous)
386 {
387 if (alternating)
388 os << ',';
389 else
390 os << ambiguous << ',';
391 }
392 os << complete;
393 if (!products_avg)
394 {
395 for (size_t i = 0; i < products; ++i)
396 os << ',' << product_states[i]
397 << ',' << product_transitions[i]
398 << ',' << product_scc[i];
399 }
400 else
401 {
402 double st = 0.0;
403 double tr = 0.0;
404 double sc = 0.0;
405 for (size_t i = 0; i < products; ++i)
406 {
407 st += product_states[i];
408 tr += product_transitions[i];
409 sc += product_scc[i];
410 }
411 os << ',' << (st / products)
412 << ',' << (tr / products)
413 << ',' << (sc / products);
414 }
415 }
416 else
417 {
418 size_t m = products_avg ? 1U : products;
419 m *= 3;
420 m += 7;
421 if (opt_strength)
422 m += 7;
423 if (opt_ambiguous)
424 ++m;
425 os << na;
426 for (size_t i = 0; i < m; ++i)
427 os << ',' << na;
428 }
429 if (opt_automata)
430 {
431 os << ',';
432 if (hoa_str.empty())
433 os << na;
434 else if (csv_escape)
435 spot::escape_rfc4180(os << '"', hoa_str) << '"';
436 else
437 spot::escape_str(os << '"', hoa_str) << '"';
438 }
439 }
440 };
441
442 typedef std::vector<statistics> statistics_formula;
443 typedef std::vector<statistics_formula> statistics_vector;
444 statistics_vector vstats;
445 std::vector<std::string> formulas;
446
447 static int
parse_opt(int key,char * arg,struct argp_state *)448 parse_opt(int key, char* arg, struct argp_state*)
449 {
450 // Called from C code, so should not raise any exception.
451 BEGIN_EXCEPTION_PROTECT;
452 // This switch is alphabetically-ordered.
453 switch (key)
454 {
455 case 'D':
456 determinize = true;
457 products = 0;
458 max_det_states = -1U;
459 max_det_edges = -1U;
460 if (max_det_states_given)
461 error(2, 0, "Options --determinize-max-states and "
462 "--determinize are incompatible.");
463 if (max_det_edges_given)
464 error(2, 0, "Options --determinize-max-edges and "
465 "--determinize are incompatible.");
466 break;
467 case 'q':
468 verbose = false;
469 quiet = true;
470 break;
471 case OPT_DET_MAX_EDGES:
472 max_det_edges_given = true;
473 max_det_states = to_pos_int(arg, "--determinize-max-edges");
474 if (determinize)
475 error(2, 0, "Options --determinize-max-edges and "
476 "--determinize are incompatible.");
477 break;
478 case OPT_DET_MAX_STATES:
479 max_det_states_given = true;
480 max_det_states = to_pos_int(arg, "--determinize-max-states");
481 if (determinize)
482 error(2, 0, "Options --determinize-max-states and "
483 "--determinize are incompatible.");
484 break;
485 case ARGP_KEY_ARG:
486 if (arg[0] == '-' && !arg[1])
487 jobs.emplace_back(arg, true);
488 else
489 tools_push_trans(arg);
490 break;
491 case OPT_AMBIGUOUS:
492 opt_ambiguous = true;
493 break;
494 case OPT_AUTOMATA:
495 opt_automata = true;
496 break;
497 case OPT_BOGUS:
498 {
499 bogus_output = new output_file(arg);
500 bogus_output_filename = arg;
501 break;
502 }
503 case OPT_CSV:
504 want_stats = true;
505 csv_output = arg ? arg : "-";
506 break;
507 case OPT_DENSITY:
508 density = to_probability(arg, "---density");
509 break;
510 case OPT_DUPS:
511 allow_dups = true;
512 break;
513 case OPT_FAIL_ON_TIMEOUT:
514 fail_on_timeout = true;
515 break;
516 case OPT_GRIND:
517 grind_output_filename = arg;
518 grind_output = new output_file(arg);
519 break;
520 case OPT_IGNORE_EXEC_FAIL:
521 ignore_exec_fail = true;
522 break;
523 case OPT_JSON:
524 want_stats = true;
525 json_output = arg ? arg : "-";
526 break;
527 case OPT_NOCHECKS:
528 no_checks = true;
529 no_complement = true;
530 break;
531 case OPT_NOCOMP:
532 no_complement = true;
533 break;
534 case OPT_OMIT:
535 opt_omit = true;
536 break;
537 case OPT_PRODUCTS:
538 if (*arg == '+')
539 {
540 products_avg = false;
541 ++arg;
542 }
543 products = to_pos_int(arg, "--products");
544 if (products == 0)
545 products_avg = false;
546 break;
547 case OPT_REFERENCE:
548 tools_push_trans(arg, true);
549 break;
550 case OPT_SAVE_INCLUSION_PRODUCTS:
551 {
552 saved_inclusion_products = new output_file(arg);
553 saved_inclusion_products_filename = arg;
554 break;
555 }
556 case OPT_SEED:
557 seed = to_pos_int(arg, "--seed");
558 break;
559 case OPT_STATES:
560 states = to_pos_int(arg, "--states");
561 break;
562 case OPT_STOP_ERR:
563 stop_on_error = true;
564 break;
565 case OPT_STRENGTH:
566 opt_strength = true;
567 break;
568 case OPT_VERBOSE:
569 verbose = true;
570 quiet = false;
571 break;
572 default:
573 return ARGP_ERR_UNKNOWN;
574 }
575 END_EXCEPTION_PROTECT;
576 return 0;
577 }
578
579 namespace
580 {
581 class xtranslator_runner final: public translator_runner
582 {
583 public:
xtranslator_runner(spot::bdd_dict_ptr dict)584 xtranslator_runner(spot::bdd_dict_ptr dict)
585 : translator_runner(dict)
586 {
587 }
588
589 spot::twa_graph_ptr
translate(unsigned int translator_num,char l,statistics_formula * fstats,bool & problem)590 translate(unsigned int translator_num, char l, statistics_formula* fstats,
591 bool& problem)
592 {
593 output.reset(translator_num);
594
595 std::ostringstream command;
596 format(command, tools[translator_num].cmd);
597
598 std::string cmd = command.str();
599 auto disp_cmd =
600 [&]() {
601 std::cerr << "Running [" << l << translator_num;
602 const char* name = tools[translator_num].name;
603 if (name != tools[translator_num].spec)
604 std::cerr << ": " << name;
605 std::cerr << "]: " << cmd << '\n';
606 };
607 if (!quiet)
608 disp_cmd();
609 spot::process_timer timer;
610 timer.start();
611 int es = exec_with_timeout(cmd.c_str());
612 timer.stop();
613 const char* status_str = nullptr;
614
615 spot::twa_graph_ptr res = nullptr;
616 if (timed_out)
617 {
618 if (fail_on_timeout)
619 {
620 if (quiet)
621 disp_cmd();
622 global_error() << "error: timeout during execution of command\n";
623 end_error();
624 }
625 else
626 {
627 if (!quiet)
628 std::cerr << "warning: timeout during execution of command\n";
629 ++timeout_count;
630 }
631 status_str = "timeout";
632 problem = fail_on_timeout;
633 es = -1;
634 }
635 else if (WIFSIGNALED(es))
636 {
637 if (quiet)
638 disp_cmd();
639 status_str = "signal";
640 problem = true;
641 es = WTERMSIG(es);
642 global_error() << "error: execution terminated by signal "
643 << es << ".\n";
644 end_error();
645 }
646 else if (WIFEXITED(es) && WEXITSTATUS(es) != 0)
647 {
648 es = WEXITSTATUS(es);
649 status_str = "exit code";
650 if (!ignore_exec_fail)
651 {
652 if (quiet)
653 disp_cmd();
654 problem = true;
655 global_error() << "error: execution returned exit code "
656 << es << ".\n";
657 end_error();
658 }
659 else
660 {
661 problem = false;
662 if (!quiet)
663 std::cerr << "warning: execution returned exit code "
664 << es << ".\n";
665 ++ignored_exec_fail;
666 }
667 }
668 else
669 {
670 status_str = "ok";
671 problem = false;
672 es = 0;
673
674 auto aut = spot::parse_aut(output.val()->name(), dict,
675 spot::default_environment::instance(),
676 opt_parse);
677 if (!aut->errors.empty())
678 {
679 if (quiet)
680 disp_cmd();
681 status_str = "parse error";
682 problem = true;
683 es = -1;
684 std::ostream& err = global_error();
685 err << "error: failed to parse the produced automaton.\n";
686 aut->format_errors(err);
687 end_error();
688 res = nullptr;
689 }
690 else if (aut->aborted)
691 {
692 if (quiet)
693 disp_cmd();
694 status_str = "aborted";
695 problem = true;
696 es = -1;
697 global_error() << "error: aborted HOA file.\n";
698 end_error();
699 res = nullptr;
700 }
701 else
702 {
703 res = aut->aut;
704 }
705 }
706
707 if (want_stats)
708 {
709 statistics* st = &(*fstats)[translator_num];
710 st->status_str = status_str;
711 st->status_code = es;
712 st->time = timer.walltime();
713
714 // Compute statistics.
715 if (res)
716 {
717 if (verbose)
718 std::cerr << "info: getting statistics\n";
719 st->ok = true;
720 st->alternating = !res->is_existential();
721 spot::twa_sub_statistics s = sub_stats_reachable(res);
722 st->states = s.states;
723 st->edges = s.edges;
724 st->transitions = s.transitions;
725 st->acc = res->acc().num_sets();
726 spot::scc_info
727 m(res, (opt_strength
728 ? spot::scc_info_options::TRACK_STATES
729 : spot::scc_info_options::NONE));
730 unsigned c = m.scc_count();
731 st->scc = c;
732 st->nondetstates = spot::count_nondet_states(res);
733 st->nondeterministic = st->nondetstates != 0;
734 if (opt_strength && !st->alternating)
735 {
736 m.determine_unknown_acceptance();
737 for (unsigned n = 0; n < c; ++n)
738 {
739 if (m.is_rejecting_scc(n))
740 ++st->nonacc_scc;
741 else if (is_terminal_scc(m, n))
742 ++st->terminal_scc;
743 else if (is_weak_scc(m, n))
744 ++st->weak_scc;
745 else
746 ++st->strong_scc;
747 }
748 if (st->strong_scc)
749 st->strong_aut = true;
750 else if (st->weak_scc)
751 st->weak_aut = true;
752 else
753 st->terminal_aut = true;
754 }
755 if (opt_ambiguous && !st->alternating)
756 st->ambiguous = !spot::is_unambiguous(res);
757 st->complete = spot::is_complete(res);
758
759 if (opt_automata)
760 {
761 std::ostringstream os;
762 spot::print_hoa(os, res, "l");
763 st->hoa_str = os.str();
764 }
765 }
766 }
767 output.cleanup();
768 return res;
769 }
770 };
771
772 static bool
check_empty_prod(const spot::const_twa_graph_ptr & aut_i,const spot::const_twa_graph_ptr & aut_j,size_t i,size_t j,bool icomp,bool jcomp,const std::string & formula)773 check_empty_prod(const spot::const_twa_graph_ptr& aut_i,
774 const spot::const_twa_graph_ptr& aut_j,
775 size_t i, size_t j, bool icomp, bool jcomp,
776 const std::string& formula)
777 {
778 if (aut_i->num_sets() + aut_j->num_sets() >
779 spot::acc_cond::mark_t::max_accsets())
780 {
781 // Report the skipped test if both automata are not
782 // complemented, or the --verbose option is used,
783 if (!verbose && (icomp || jcomp))
784 return false;
785 if (!quiet)
786 {
787 std::cerr << "info: building ";
788 if (icomp)
789 std::cerr << "Comp(N" << i << ')';
790 else
791 std::cerr << 'P' << i;
792 if (jcomp)
793 std::cerr << "*Comp(P" << j << ')';
794 else
795 std::cerr << "*N" << j;
796 std::cerr << " requires more acceptance sets than supported\n";
797 }
798 return false;
799 }
800
801 auto prod = spot::product(aut_i, aut_j);
802
803 if (saved_inclusion_products)
804 {
805 std::ostringstream os;
806 if (icomp)
807 os << "Comp(N" << i << ')';
808 else
809 os << 'P' << i;
810 if (jcomp)
811 os << "*Comp(P" << j << ')';
812 else
813 os << "*N" << j;
814 os << ", " << formula;
815 prod->set_named_prop("automaton-name", new std::string(os.str()));
816 spot::print_hoa(saved_inclusion_products->ostream(), prod) << std::endl;
817 }
818
819 if (verbose)
820 {
821 std::cerr << "info: check_empty ";
822 if (icomp)
823 std::cerr << "Comp(N" << i << ')';
824 else
825 std::cerr << 'P' << i;
826 if (jcomp)
827 std::cerr << "*Comp(P" << j << ')';
828 else
829 std::cerr << "*N" << j;
830 std::cerr << '\n';
831 }
832
833 auto w = prod->accepting_word();
834 if (w)
835 {
836 std::ostream& err = global_error();
837 err << "error: ";
838 if (icomp)
839 err << "Comp(N" << i << ')';
840 else
841 err << 'P' << i;
842 if (jcomp)
843 err << "*Comp(P" << j << ')';
844 else
845 err << "*N" << j;
846 err << " is nonempty; both automata accept the infinite word:\n"
847 << " ";
848 example() << *w << '\n';
849 end_error();
850 }
851 return !!w;
852 }
853
854 static bool
cross_check(const std::vector<spot::scc_info * > & maps,char l,unsigned p)855 cross_check(const std::vector<spot::scc_info*>& maps, char l, unsigned p)
856 {
857 size_t m = maps.size();
858 if (verbose)
859 {
860 std::cerr << "info: cross_check {";
861 bool first = true;
862 for (size_t i = 0; i < m; ++i)
863 if (maps[i])
864 {
865 if (first)
866 first = false;
867 else
868 std::cerr << ',';
869 std::cerr << l << i;
870 }
871 std::cerr << "}, state-space #" << p << '/' << products << '\n';
872 }
873
874 std::vector<bool> res(m);
875 unsigned verified = 0;
876 unsigned violated = 0;
877 for (size_t i = 0; i < m; ++i)
878 if (spot::scc_info* m = maps[i])
879 {
880 bool i_is_accepting = m->one_accepting_scc() >= 0;
881 res[i] = i_is_accepting;
882 if (i_is_accepting)
883 ++verified;
884 else
885 ++violated;
886 }
887 if (verified != 0 && violated != 0)
888 {
889 std::ostream& err = global_error();
890 err << "error: {";
891 bool first = true;
892 for (size_t i = 0; i < m; ++i)
893 if (maps[i] && res[i])
894 {
895 if (first)
896 first = false;
897 else
898 err << ',';
899 err << l << i;
900 }
901 err << "} disagree with {";
902 std::ostringstream os;
903 first = true;
904 for (size_t i = 0; i < m; ++i)
905 if (maps[i] && !res[i])
906 {
907 if (first)
908 first = false;
909 else
910 os << ',';
911 os << l << i;
912 }
913 err << os.str() << "} when evaluating ";
914 if (products > 1)
915 err << "state-space #" << p << '/' << products << '\n';
916 else
917 err << "the state-space\n";
918 err << " the following word(s) are not accepted by {"
919 << os.str() << "}:\n";
920 for (size_t i = 0; i < m; ++i)
921 if (maps[i] && res[i])
922 {
923 global_error() << " " << l << i << " accepts: ";
924 example() << *maps[i]->get_aut()->accepting_word() << '\n';
925 }
926 end_error();
927 return true;
928 }
929 return false;
930 }
931
932 typedef std::set<unsigned> state_set;
933
934 // Collect all the states of SSPACE that appear in the accepting SCCs
935 // of PROD. (Trivial SCCs are considered accepting.)
936 static void
states_in_acc(const spot::scc_info * m,state_set & s)937 states_in_acc(const spot::scc_info* m, state_set& s)
938 {
939 auto aut = m->get_aut();
940 auto ps = aut->get_named_prop<const spot::product_states>("product-states");
941 for (auto& scc: *m)
942 if (scc.is_accepting() || scc.is_trivial())
943 for (auto i: scc.states())
944 // Get the projection on sspace.
945 s.insert((*ps)[i].second);
946 }
947
948 static bool
consistency_check(const spot::scc_info * pos,const spot::scc_info * neg)949 consistency_check(const spot::scc_info* pos, const spot::scc_info* neg)
950 {
951 // the states of SSPACE should appear in the accepting SCC of at
952 // least one of POS or NEG. Maybe both.
953 state_set s;
954 states_in_acc(pos, s);
955 states_in_acc(neg, s);
956 return s.size() == states;
957 }
958
959 typedef
960 std::unordered_set<spot::formula> fset_t;
961
962 class processor final: public job_processor
963 {
964 spot::bdd_dict_ptr dict = spot::make_bdd_dict();
965 xtranslator_runner runner;
966 fset_t unique_set;
967 public:
processor()968 processor():
969 runner(dict)
970 {
971 }
972
973 int
process_string(const std::string & input,const char * filename,int linenum)974 process_string(const std::string& input,
975 const char* filename,
976 int linenum) override
977 {
978 auto pf = parse_formula(input);
979 if (!pf.f || !pf.errors.empty())
980 {
981 if (filename)
982 error_at_line(0, 0, filename, linenum, "parse error:");
983 pf.format_errors(std::cerr);
984 return 1;
985 }
986 auto f = pf.f;
987
988 int res = process_formula(f, filename, linenum);
989
990 if (res && bogus_output)
991 bogus_output->ostream() << input << std::endl;
992 if (res && grind_output)
993 {
994 std::string bogus = input;
995 std::vector<spot::formula> mutations;
996 unsigned mutation_count;
997 unsigned mutation_max;
998 while (res)
999 {
1000 if (!quiet)
1001 std::cerr << "Trying to find a bogus mutation of " << bold
1002 << bogus << reset_color << "...\n";
1003 mutations = mutate(f);
1004 mutation_count = 1;
1005 mutation_max = mutations.size();
1006 res = 0;
1007 for (auto g: mutations)
1008 {
1009 if (!quiet)
1010 std::cerr << "Mutation " << mutation_count << '/'
1011 << mutation_max << ": ";
1012 f = g;
1013 res = process_formula(g);
1014 if (res)
1015 break;
1016 ++mutation_count;
1017 }
1018 if (res)
1019 {
1020 if (lbt_input)
1021 bogus = spot::str_lbt_ltl(f);
1022 else
1023 bogus = spot::str_psl(f);
1024 if (bogus_output)
1025 bogus_output->ostream() << bogus << std::endl;
1026 }
1027 }
1028 if (!quiet)
1029 std::cerr << "Smallest bogus mutation found for "
1030 << bold << input << reset_color << " is "
1031 << bold << bogus << reset_color << ".\n\n";
1032 grind_output->ostream() << bogus << std::endl;
1033 }
1034 return 0;
1035 }
1036
product_stats(statistics_formula * stats,unsigned i,spot::scc_info * sm)1037 void product_stats(statistics_formula* stats, unsigned i,
1038 spot::scc_info* sm)
1039 {
1040 if (verbose && sm)
1041 std::cerr << "info: " << sm->scc_count()
1042 << " SCCs\n";
1043 // Statistics
1044 if (want_stats)
1045 {
1046 if (sm)
1047 {
1048 (*stats)[i].product_scc.push_back(sm->scc_count());
1049 spot::twa_statistics s = spot::stats_reachable(sm->get_aut());
1050 (*stats)[i].product_states.push_back(s.states);
1051 (*stats)[i].product_transitions.push_back(s.edges);
1052 }
1053 else
1054 {
1055 double n = nan("");
1056 (*stats)[i].product_scc.push_back(n);
1057 (*stats)[i].product_states.push_back(n);
1058 (*stats)[i].product_transitions.push_back(n);
1059 }
1060 }
1061 }
1062
1063 int
process_formula(spot::formula f,const char * filename=nullptr,int linenum=0)1064 process_formula(spot::formula f,
1065 const char* filename = nullptr, int linenum = 0) override
1066 {
1067 static unsigned round = 0;
1068
1069 if (opt_relabel
1070 // If we need LBT atomic proposition in any of the input or
1071 // output, relabel the formula.
1072 || (!f.has_lbt_atomic_props() &&
1073 (runner.has('l') || runner.has('L') || runner.has('T')))
1074 // Likewise for Spin
1075 || (!f.has_spin_atomic_props() &&
1076 (runner.has('s') || runner.has('S'))))
1077 f = spot::relabel(f, spot::Pnn);
1078
1079 // ---------- Positive Formula ----------
1080
1081 runner.round_formula(f, round);
1082
1083 // Call formula() before printing anything else, in case it
1084 // complains.
1085 std::string fstr = runner.formula();
1086 if (!quiet)
1087 {
1088 if (filename)
1089 std::cerr << filename << ':';
1090 if (linenum)
1091 std::cerr << linenum << ':';
1092 if (filename || linenum)
1093 std::cerr << ' ';
1094 std::cerr << bold << fstr << reset_color << '\n';
1095 }
1096
1097 // Make sure we do not translate the same formula twice.
1098 if (!allow_dups)
1099 {
1100 if (!unique_set.insert(f).second)
1101 {
1102 if (!quiet)
1103 std::cerr
1104 << ("warning: This formula or its negation has already"
1105 " been checked.\n Use --allow-dups if it "
1106 "should not be ignored.\n\n");
1107 return 0;
1108 }
1109 }
1110
1111 int problems = 0;
1112
1113 // These store the result of the translation of the positive and
1114 // negative formulas.
1115 size_t m = tools.size();
1116 std::vector<spot::twa_graph_ptr> pos(m);
1117 std::vector<spot::twa_graph_ptr> neg(m);
1118 // These store the complement of the above results, when we can
1119 // compute it easily.
1120 std::vector<spot::twa_graph_ptr> comp_pos(m);
1121 std::vector<spot::twa_graph_ptr> comp_neg(m);
1122
1123
1124 unsigned n = vstats.size();
1125 vstats.resize(n + (no_checks ? 1 : 2));
1126 statistics_formula* pstats = &vstats[n];
1127 statistics_formula* nstats = nullptr;
1128 pstats->resize(m);
1129 formulas.push_back(fstr);
1130
1131 for (size_t n = 0; n < m; ++n)
1132 {
1133 bool prob;
1134 pos[n] = runner.translate(n, 'P', pstats, prob);
1135 problems += prob;
1136 }
1137
1138 // ---------- Negative Formula ----------
1139
1140 // The negative formula is only needed when checks are
1141 // activated.
1142 if (!no_checks)
1143 {
1144 nstats = &vstats[n + 1];
1145 nstats->resize(m);
1146
1147 spot::formula nf = spot::formula::Not(f);
1148
1149 if (!allow_dups)
1150 {
1151 bool res = unique_set.insert(nf).second;
1152 // It is not possible to discover that nf has already been
1153 // translated, otherwise that would mean that f had been
1154 // translated too and we would have caught it before.
1155 assert(res);
1156 (void) res;
1157 }
1158
1159 runner.round_formula(nf, round);
1160 formulas.push_back(runner.formula());
1161
1162 for (size_t n = 0; n < m; ++n)
1163 {
1164 bool prob;
1165 neg[n] = runner.translate(n, 'N', nstats, prob);
1166 problems += prob;
1167 }
1168 }
1169
1170 spot::cleanup_tmpfiles();
1171 ++round;
1172
1173 auto printsize = [](const spot::const_twa_graph_ptr& aut)
1174 {
1175 std::cerr << aut->num_states() << " st.,"
1176 << aut->num_edges() << " ed.,"
1177 << aut->num_sets() << " sets";
1178 };
1179
1180 if (verbose)
1181 {
1182 std::cerr << "info: collected automata:\n";
1183 auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
1184 const char prefix)
1185 {
1186 if (!x[i])
1187 return;
1188 std::cerr << "info: " << prefix << i << "\t(";
1189 printsize(x[i]);
1190 std::cerr << ')';
1191 if (!x[i]->is_existential())
1192 std::cerr << " univ-edges";
1193 if (is_deterministic(x[i]))
1194 std::cerr << " deterministic";
1195 if (is_complete(x[i]))
1196 std::cerr << " complete";
1197 std::cerr << '\n';
1198 };
1199 for (unsigned i = 0; i < m; ++i)
1200 {
1201 tmp(pos, i, 'P');
1202 tmp(neg, i, 'N');
1203 }
1204 }
1205
1206 bool missing_complement = true;
1207
1208 if (!no_checks)
1209 {
1210 if (!quiet)
1211 std::cerr
1212 << "Performing sanity checks and gathering statistics...\n";
1213
1214 // If we have reference tools, pick the smallest of their
1215 // automata for positive and negative references.
1216 auto smallest_ref = [&](std::vector<spot::twa_graph_ptr>& from)
1217 {
1218 typedef std::tuple<bool, unsigned, unsigned, unsigned> aut_size;
1219 int smallest_ref = -1;
1220 aut_size smallest_size(true, -1U, -1U, -1U);
1221 for (unsigned i = 0; i < m; ++i)
1222 if (tools[i].reference && from[i])
1223 {
1224 aut_size pisize(!is_deterministic(from[i]),
1225 from[i]->num_states(),
1226 from[i]->num_edges(),
1227 from[i]->num_sets());
1228 if (pisize < smallest_size)
1229 {
1230 smallest_ref = i;
1231 smallest_size = pisize;
1232 }
1233 }
1234 return smallest_ref;
1235 };
1236
1237 // These are not our definitive choice for reference
1238 // automata, because the sizes might change after we remove
1239 // alternation and Fin acceptance. But we need to know now
1240 // if we will have a pair of reference automata in order to
1241 // skip some of the constructions.
1242 int smallest_pos_ref = smallest_ref(pos);
1243 int smallest_neg_ref = smallest_ref(neg);
1244 if (smallest_pos_ref < 0 || smallest_neg_ref < 0)
1245 smallest_pos_ref = smallest_neg_ref = -1;
1246
1247 bool print_first = verbose;
1248 auto unalt = [&](std::vector<spot::twa_graph_ptr>& x,
1249 unsigned i, char prefix)
1250 {
1251 if (!x[i] || x[i]->is_existential())
1252 return;
1253 if (verbose)
1254 {
1255 if (print_first)
1256 {
1257 std::cerr <<
1258 "info: getting rid of universal edges...\n";
1259 print_first = false;
1260 }
1261 std::cerr << "info: " << prefix << i << "\t(";
1262 printsize(x[i]);
1263 std::cerr << ") ->";
1264 }
1265 x[i] = remove_alternation(x[i]);
1266 if (verbose)
1267 {
1268 std::cerr << " (";
1269 printsize(x[i]);
1270 std::cerr << ")\n";
1271 }
1272 };
1273
1274 // Remove alternation
1275 for (size_t i = 0; i < m; ++i)
1276 {
1277 unalt(pos, i, 'P');
1278 unalt(neg, i, 'N');
1279 }
1280
1281 print_first = verbose;
1282 auto tmp = [&](std::vector<spot::twa_graph_ptr>& x, unsigned i,
1283 const char* prefix, const char* suffix)
1284 {
1285 if (!x[i])
1286 return;
1287 unsigned before = x[i]->num_sets();
1288 cleanup_acceptance_here(x[i]);
1289 unsigned after = x[i]->num_sets();
1290 if (verbose && before != after)
1291 {
1292 if (print_first)
1293 {
1294 std::cerr << "info: removing unused sets...\n";
1295 print_first = false;
1296 }
1297 std::cerr << "info: " << prefix << i
1298 << suffix << '\t' << before << " sets -> "
1299 << after << " sets\n";
1300 }
1301 };
1302 for (size_t i = 0; i < m; ++i)
1303 {
1304 tmp(pos, i, " P", " ");
1305 tmp(neg, i, " N", " ");
1306 }
1307
1308 // Complement
1309 if (!no_complement)
1310 {
1311 spot::output_aborter aborter_(max_det_states,
1312 max_det_edges);
1313 spot::output_aborter* aborter = nullptr;
1314 if (max_det_states != -1U || max_det_edges != -1U)
1315 aborter = &aborter_;
1316
1317 print_first = verbose;
1318 auto comp = [&](std::vector<spot::twa_graph_ptr>& from,
1319 std::vector<spot::twa_graph_ptr>& to, int i,
1320 char prefix)
1321 {
1322 if (from[i] && !to[i])
1323 {
1324 // Do not complement reference automata if we have a
1325 // reference pair.
1326 if (smallest_pos_ref >= 0 && tools[i].reference)
1327 return;
1328 if (print_first)
1329 {
1330 std::cerr << "info: complementing automata...\n";
1331 print_first = false;
1332 }
1333 if (verbose)
1334 std::cerr << "info: " << prefix << i;
1335 if (aborter && aborter->too_large(from[i])
1336 && !spot::is_universal(from[i]))
1337 missing_complement = true;
1338 else
1339 try
1340 {
1341 to[i] = spot::complement(from[i], aborter);
1342 if (verbose)
1343 {
1344 if (to[i])
1345 {
1346 std::cerr << "\t(";
1347 printsize(from[i]);
1348 std::cerr << ") -> (";
1349 printsize(to[i]);
1350 std::cerr << ")\tComp(" << prefix
1351 << i << ")\n";
1352 }
1353 else
1354 {
1355 std::cerr << "\tnot complemented";
1356 if (aborter)
1357 aborter->print_reason(std::cerr
1358 << " (") << ')';
1359 std::cerr << '\n';
1360 }
1361 }
1362 }
1363 catch (const std::runtime_error& re)
1364 {
1365 missing_complement = true;
1366 if (verbose)
1367 std::cerr << "\tnot complemented ("
1368 << re.what() << ")\n";
1369 }
1370 }
1371 };
1372 missing_complement = false;
1373 for (unsigned i = 0; i < m; ++i)
1374 {
1375 comp(pos, comp_pos, i, 'P');
1376 comp(neg, comp_neg, i, 'N');
1377 }
1378 }
1379
1380 if (smallest_pos_ref >= 0)
1381 {
1382 // Recompute the smallest references now, because
1383 // removing alternation and useless acceptance sets
1384 // might have changed the sizes.
1385 smallest_pos_ref = smallest_ref(pos);
1386 smallest_neg_ref = smallest_ref(neg);
1387
1388 if (verbose)
1389 std::cerr << "info: P" << smallest_pos_ref
1390 << " and N" << smallest_neg_ref << " assumed "
1391 << "correct and used as references\n";
1392 }
1393
1394 // intersection test
1395 for (size_t i = 0; i < m; ++i)
1396 if (pos[i])
1397 for (size_t j = 0; j < m; ++j)
1398 if (neg[j])
1399 {
1400 // Do not compare reference translators.
1401 if (tools[i].reference && tools[j].reference)
1402 continue;
1403 // If we have a reference pair, only compare
1404 // against that pair when i != j.
1405 if (i == j ||
1406 !((!tools[i].reference &&
1407 smallest_neg_ref >= 0 &&
1408 (size_t)smallest_neg_ref != j)
1409 || (!tools[j].reference &&
1410 smallest_pos_ref >= 0 &&
1411 (size_t)smallest_pos_ref != i)))
1412 problems +=
1413 check_empty_prod(pos[i], neg[j], i, j, false, false,
1414 fstr);
1415
1416 // Deal with the extra complemented automata if we
1417 // have some.
1418
1419 // If comp_pos[j] and comp_neg[j] exist for the
1420 // same j, it means pos[j] and neg[j] were both
1421 // deterministic. In that case, we will want to
1422 // make sure that comp_pos[j]*comp_neg[j] is empty
1423 // to assert the complementary of pos[j] and
1424 // neg[j]. However using comp_pos[j] and
1425 // comp_neg[j] against other translator will not
1426 // give us any more insight than pos[j] and
1427 // neg[j]. So we only do intersection checks with
1428 // a complement automata when one of the two
1429 // translation was not deterministic.
1430
1431 if (i != j && comp_pos[j] && !comp_neg[j])
1432 if (smallest_pos_ref < 0 || i == (size_t)smallest_pos_ref)
1433 problems +=
1434 check_empty_prod(pos[i], comp_pos[j],
1435 i, j, false, true, fstr);
1436 if (i != j && comp_neg[i] && !comp_pos[i])
1437 if (smallest_neg_ref < 0 || j == (size_t)smallest_neg_ref)
1438 problems +=
1439 check_empty_prod(comp_neg[i], neg[j],
1440 i, j, true, false, fstr);
1441 if (comp_pos[i] && comp_neg[j] &&
1442 (i == j || (!comp_neg[i] && !comp_pos[j])))
1443 problems +=
1444 check_empty_prod(comp_neg[j], comp_pos[i],
1445 j, i, true, true, fstr);
1446 }
1447 }
1448 else
1449 {
1450 std::cerr << "Gathering statistics...\n";
1451 }
1452
1453 spot::atomic_prop_set* ap = spot::atomic_prop_collect(f);
1454
1455 if (want_stats)
1456 for (size_t i = 0; i < m; ++i)
1457 {
1458 (*pstats)[i].product_states.reserve(products);
1459 (*pstats)[i].product_transitions.reserve(products);
1460 (*pstats)[i].product_scc.reserve(products);
1461 if (neg[i])
1462 {
1463 (*nstats)[i].product_states.reserve(products);
1464 (*nstats)[i].product_transitions.reserve(products);
1465 (*nstats)[i].product_scc.reserve(products);
1466 }
1467 }
1468 // Decide if we need products with state-space.
1469 unsigned actual_products = products;
1470 if (actual_products)
1471 {
1472 if (missing_complement)
1473 {
1474 if (verbose)
1475 std::cerr
1476 << ("info: complements not computed for some automata\ninfo: "
1477 "continuing with cross_checks and consistency_checks\n");
1478 }
1479 else if (want_stats)
1480 {
1481 if (verbose)
1482 std::cerr
1483 << ("info: running cross_checks and consistency_checks"
1484 "just for statistics\n");
1485 }
1486 else
1487 {
1488 if (verbose)
1489 std::cerr
1490 << "info: cross_checks and consistency_checks unnecessary\n";
1491 actual_products = 0;
1492 }
1493 }
1494 for (unsigned p = 0; p < actual_products; ++p)
1495 {
1496 // build a random state-space.
1497 spot::srand(seed);
1498
1499 if (verbose)
1500 std::cerr << "info: building state-space #" << (p+1) << '/'
1501 << products << " of " << states
1502 << " states with seed " << seed << '\n';
1503
1504 auto statespace = spot::random_graph(states, density, ap, dict);
1505
1506 if (verbose)
1507 std::cerr << "info: state-space has "
1508 << statespace->num_edges()
1509 << " edges\n";
1510
1511 // Associated SCC maps.
1512 std::vector<spot::scc_info*> pos_map(m);
1513 std::vector<spot::scc_info*> neg_map(m);
1514 for (size_t i = 0; i < m; ++i)
1515 {
1516 spot::scc_info* sm = nullptr;
1517 if (pos[i])
1518 {
1519 if (verbose)
1520 std::cerr << ("info: building product between state-space"
1521 " and P") << i
1522 << " (" << pos[i]->num_states() << " st., "
1523 << pos[i]->num_edges() << " ed.)\n";
1524
1525 try
1526 {
1527 auto p = spot::product(pos[i], statespace);
1528 if (verbose)
1529 std::cerr << "info: product has " << p->num_states()
1530 << " st., " << p->num_edges()
1531 << " ed.\n";
1532 sm = new
1533 spot::scc_info(p, spot::scc_info_options::TRACK_STATES);
1534 sm->determine_unknown_acceptance();
1535 }
1536 catch (const std::bad_alloc&)
1537 {
1538 std::cerr << ("warning: not enough memory to build "
1539 "product of P") << i << " with state-space";
1540 if (products > 1)
1541 std::cerr << " #" << (p+1) << '/' << products << '\n';
1542 std::cerr << '\n';
1543 ++oom_count;
1544 }
1545 pos_map[i] = sm;
1546 }
1547 product_stats(pstats, i, sm);
1548 }
1549
1550 if (!no_checks)
1551 for (size_t i = 0; i < m; ++i)
1552 {
1553 spot::scc_info* sm = nullptr;
1554 if (neg[i])
1555 {
1556 if (verbose)
1557 std::cerr << ("info: building product between state-space"
1558 " and N") << i
1559 << " (" << neg[i]->num_states() << " st., "
1560 << neg[i]->num_edges() << " ed.)\n";
1561
1562 try
1563 {
1564 auto p = spot::product(neg[i], statespace);
1565 if (verbose)
1566 std::cerr << "info: product has " << p->num_states()
1567 << " st., " << p->num_edges()
1568 << " ed.\n";
1569 sm = new
1570 spot::scc_info(p,
1571 spot::scc_info_options::TRACK_STATES);
1572 sm->determine_unknown_acceptance();
1573 }
1574 catch (const std::bad_alloc&)
1575 {
1576 std::cerr << ("warning: not enough memory to build "
1577 "product of N")
1578 << i << " with state-space";
1579 if (products > 1)
1580 std::cerr << " #" << p << '/' << products << '\n';
1581 std::cerr << '\n';
1582 ++oom_count;
1583 }
1584 neg_map[i] = sm;
1585 }
1586 product_stats(nstats, i, sm);
1587 }
1588
1589 if (!no_checks)
1590 {
1591 // cross-comparison test
1592 problems += cross_check(pos_map, 'P', p);
1593 problems += cross_check(neg_map, 'N', p);
1594
1595 // consistency check
1596 for (size_t i = 0; i < m; ++i)
1597 if (pos_map[i] && neg_map[i] && !tools[i].reference)
1598 {
1599 if (verbose)
1600 std::cerr << "info: consistency_check (P" << i
1601 << ",N" << i << "), state-space #"
1602 << p << '/' << products << '\n';
1603 if (!(consistency_check(pos_map[i], neg_map[i])))
1604 {
1605 ++problems;
1606
1607 std::ostream& err = global_error();
1608 err << "error: inconsistency between P" << i
1609 << " and N" << i;
1610 if (products > 1)
1611 err << " for state-space #" << p
1612 << '/' << products << '\n';
1613 else
1614 err << '\n';
1615 end_error();
1616 }
1617 }
1618 }
1619
1620 // Cleanup.
1621 if (!no_checks)
1622 for (size_t i = 0; i < m; ++i)
1623 delete neg_map[i];
1624 for (size_t i = 0; i < m; ++i)
1625 delete pos_map[i];
1626 ++seed;
1627 }
1628 if (problems && quiet)
1629 std::cerr << "input formula was "
1630 << bold << fstr << reset_color << "\n\n";
1631 if (!quiet)
1632 std::cerr << '\n';
1633 delete ap;
1634
1635 // Shall we stop processing formulas now?
1636 abort_run = global_error_flag && stop_on_error;
1637 return problems;
1638 }
1639 };
1640 }
1641
1642 // Output an RFC4180-compatible CSV file.
1643 static void
print_stats_csv(const char * filename)1644 print_stats_csv(const char* filename)
1645 {
1646 if (verbose)
1647 std::cerr << "info: writing CSV to " << filename << '\n';
1648
1649 output_file outf(filename);
1650 std::ostream& out = outf.ostream();
1651
1652 unsigned ntrans = tools.size();
1653 unsigned rounds = vstats.size();
1654 assert(rounds == formulas.size());
1655
1656 if (!outf.append())
1657 {
1658 // Do not output the header line if we append to a file.
1659 // (Even if that file was empty initially.)
1660 out << "\"formula\",\"tool\",";
1661 statistics::fields(out, !opt_omit);
1662 out << '\n';
1663 }
1664 for (unsigned r = 0; r < rounds; ++r)
1665 for (unsigned t = 0; t < ntrans; ++t)
1666 if (!opt_omit || vstats[r][t].ok)
1667 {
1668 out << '"';
1669 spot::escape_rfc4180(out, formulas[r]);
1670 out << "\",\"";
1671 spot::escape_rfc4180(out, tools[t].name);
1672 out << "\",";
1673 vstats[r][t].to_csv(out, !opt_omit);
1674 out << '\n';
1675 }
1676 outf.close(filename);
1677 }
1678
1679 static void
print_stats_json(const char * filename)1680 print_stats_json(const char* filename)
1681 {
1682 if (verbose)
1683 std::cerr << "info: writing JSON to " << filename << '\n';
1684
1685 output_file outf(filename);
1686 std::ostream& out = outf.ostream();
1687
1688 unsigned ntrans = tools.size();
1689 unsigned rounds = vstats.size();
1690 assert(rounds == formulas.size());
1691
1692 out << "{\n \"tool\": [\n \"";
1693 spot::escape_str(out, tools[0].name);
1694 for (unsigned t = 1; t < ntrans; ++t)
1695 {
1696 out << "\",\n \"";
1697 spot::escape_str(out, tools[t].name);
1698 }
1699 out << "\"\n ],\n \"formula\": [\n \"";
1700 spot::escape_str(out, formulas[0]);
1701 for (unsigned r = 1; r < rounds; ++r)
1702 {
1703 out << "\",\n \"";
1704 spot::escape_str(out, formulas[r]);
1705 }
1706 out << ("\"\n ],\n \"fields\": [\n \"formula\",\"tool\",");
1707 statistics::fields(out, !opt_omit);
1708 out << "\n ],\n \"inputs\": [ 0, 1 ],";
1709 out << "\n \"results\": [";
1710 bool notfirst = false;
1711 for (unsigned r = 0; r < rounds; ++r)
1712 for (unsigned t = 0; t < ntrans; ++t)
1713 if (!opt_omit || vstats[r][t].ok)
1714 {
1715 if (notfirst)
1716 out << ',';
1717 notfirst = true;
1718 out << "\n [ " << r << ',' << t << ',';
1719 vstats[r][t].to_csv(out, !opt_omit, "null", false);
1720 out << " ]";
1721 }
1722 out << "\n ]\n}\n";
1723 outf.close(filename);
1724 }
1725
1726 int
main(int argc,char ** argv)1727 main(int argc, char** argv)
1728 {
1729 return protected_main(argv, [&]() -> unsigned {
1730 const argp ap = { options, parse_opt, "[COMMANDFMT...]",
1731 argp_program_doc, children, nullptr, nullptr };
1732
1733 if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
1734 exit(err);
1735
1736 check_no_formula();
1737
1738 if (tools.empty())
1739 error(2, 0, "No translator to run? Run '%s --help' for usage.",
1740 program_name);
1741
1742 setup_color();
1743 setup_sig_handler();
1744
1745 processor p;
1746 if (p.run())
1747 return 2;
1748
1749 if (formulas.empty())
1750 {
1751 error(2, 0, "no formula to translate");
1752 }
1753 else if (!quiet)
1754 {
1755 if (global_error_flag)
1756 {
1757 std::ostream& err = global_error();
1758 if (bogus_output)
1759 err << ("error: some error was detected during the above "
1760 "runs.\n Check file ")
1761 << bogus_output_filename
1762 << " for problematic formulas.";
1763 else
1764 err << ("error: some error was detected during the above "
1765 "runs,\n please search for 'error:' messages"
1766 " in the above trace.");
1767 err << '\n';
1768 end_error();
1769 }
1770 else if (timeout_count == 0
1771 && ignored_exec_fail == 0 && oom_count == 0)
1772 {
1773 std::cerr << "No problem detected.\n";
1774 }
1775 else
1776 {
1777 std::cerr << "No major problem detected.\n";
1778 }
1779
1780 unsigned additional_errors = 0U;
1781 additional_errors += timeout_count > 0;
1782 additional_errors += ignored_exec_fail > 0;
1783 additional_errors += oom_count > 0;
1784 if (additional_errors)
1785 {
1786 std::cerr << (global_error_flag ? "Additionally, " : "However, ");
1787 if (timeout_count)
1788 {
1789 if (additional_errors > 1)
1790 std::cerr << "\n - ";
1791 if (timeout_count == 1)
1792 std::cerr << "1 timeout occurred";
1793 else
1794 std::cerr << timeout_count << " timeouts occurred";
1795 }
1796
1797 if (oom_count)
1798 {
1799 if (additional_errors > 1)
1800 std::cerr << "\n - ";
1801 if (oom_count == 1)
1802 std::cerr << "1 state-space product was";
1803 else
1804 std::cerr << oom_count << "state-space products were";
1805 std::cerr << " skipped by lack of memory";
1806 }
1807
1808 if (ignored_exec_fail)
1809 {
1810 if (additional_errors > 1)
1811 std::cerr << "\n - ";
1812 if (ignored_exec_fail == 1)
1813 std::cerr << "1 non-zero exit status was ignored";
1814 else
1815 std::cerr << ignored_exec_fail
1816 << " non-zero exit statuses were ignored";
1817 }
1818 if (additional_errors == 1)
1819 std::cerr << '.';
1820 std::cerr << '\n';
1821 }
1822 }
1823
1824 if (bogus_output)
1825 {
1826 bogus_output->close(bogus_output_filename);
1827 delete bogus_output;
1828 }
1829 if (grind_output)
1830 {
1831 grind_output->close(grind_output_filename);
1832 delete grind_output;
1833 }
1834 if (saved_inclusion_products)
1835 {
1836 saved_inclusion_products->close(saved_inclusion_products_filename);
1837 delete saved_inclusion_products;
1838 }
1839
1840 if (json_output)
1841 print_stats_json(json_output);
1842 if (csv_output)
1843 print_stats_csv(csv_output);
1844
1845 return global_error_flag;
1846 });
1847 }
1848