From 829012fe43dd4af38b655db4a8b88c14d30fd6a8 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 21 Aug 2014 14:54:29 +0200 Subject: [PATCH] ltlcross: implement a --save-bogus=FILENAME option Suggested by Joachim Klein. * src/bin/ltlcross.cc: Implement it. * src/tgbatest/ltlcross3.test: Test it. * doc/org/ltlcross.org, NEWS: Document it. --- NEWS | 4 ++ doc/org/ltlcross.org | 30 +++++++++- src/bin/ltlcross.cc | 115 +++++++++++++++++++++++++++++------- src/tgbatest/ltlcross3.test | 12 +++- 4 files changed, 134 insertions(+), 27 deletions(-) diff --git a/NEWS b/NEWS index d061cb4e9..e6b10c458 100644 --- a/NEWS +++ b/NEWS @@ -14,6 +14,10 @@ New in spot 1.2.4a (not yet released) - 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'. + - ltlcross has a new option --save-bogus=FILENAME to save any + formula for which a problem (other than timeout) was detected + during translation or using the resulting automatas. + * Documentation: - The man page for ltl2tgba has some new notes and references diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 34762984d..aff718f97 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -610,9 +610,9 @@ automaton as well. ** =--stop-on-error= -The =--stop-on-error= will cause =ltlcross= to abort on the first -detected error. This include failure to start some translator, read -its output, or failure to passe the sanity checks. Timeouts are +The =--stop-on-error= option will cause =ltlcross= to abort on the +first detected error. This include failure to start some translator, +read its output, or failure to passe the sanity checks. Timeouts are allowed. One use for this option is when =ltlcross= is used in combination with @@ -627,6 +627,30 @@ to remove duplicate formulas will keep growing). randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' #+END_SRC +** =--save-bogus=FILENAME= + +The =--save-bogus=FILENAME= will save any formula for which an error +was detected (either some translation failed, or some problem was +detected using the resulting automata) in =FILENAME=. Again, timeouts +are not considered to be errors, and therefore not reported in this +file. + +The main use for this feature is in conjunction with =randltl='s +generation of random formulas. For instance the following command +will run the translators on an infinite number of formulas, saving +any problematic formula in =bugs.ltl=. + +#+BEGIN_SRC sh :export code :eval no +randltl -n -1 --tree-size 10..25 a b c | ltlcross --save-bogus=bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' +#+END_SRC + +You can periodically check the contents of =bugs.ltl=, and then run +=ltlcross= only on those formulas to look at the problems: + +#+BEGIN_SRC sh :export code :eval no +ltlcross -F bugs.ltl 'ltl2tgba --lbtt %f >%T' 'ltl3ba -f %s >%N' +#+END_SRC + ** =--no-check= The =--no-check= option disables all sanity checks, and only use the supplied diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index b776d02e9..be5f577fc 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -94,6 +94,7 @@ Exit status:\n\ #define OPT_COLOR 10 #define OPT_NOCOMP 11 #define OPT_OMIT 12 +#define OPT_BOGUS 13 static const argp_option options[] = { @@ -159,6 +160,8 @@ static const argp_option options[] = "colorize output; WHEN can be 'never', 'always' (the default if " "--color is used without argument), or " "'auto' (the default if --color is not used)", 0 }, + { "save-bogus", OPT_BOGUS, "FILENAME", 0, + "save formulas for which problems were detected in FILENAME", 0 }, { 0, 0, 0, 0, 0, 0 } }; @@ -206,6 +209,8 @@ unsigned products = 1; bool products_avg = true; bool opt_omit = false; bool has_sr = false; // Has Streett or Rabin automata to process. +const char* bogus_output_filename = 0; +std::ofstream* bogus_output = 0; struct translator_spec { @@ -509,6 +514,14 @@ parse_opt(int key, char* arg, struct argp_state*) << "on your platform" << std::endl; #endif break; + case OPT_BOGUS: + { + bogus_output = new std::ofstream(arg); + if (!*bogus_output) + error(2, errno, "cannot open '%s'", arg); + bogus_output_filename = arg; + break; + } case OPT_COLOR: { if (arg) @@ -849,7 +862,8 @@ namespace } const spot::tgba* - translate(unsigned int translator_num, char l, statistics_formula* fstats) + translate(unsigned int translator_num, char l, statistics_formula* fstats, + bool& problem) { output.reset(translator_num); @@ -874,11 +888,13 @@ namespace std::cerr << "warning: timeout during execution of command\n"; ++timeout_count; status_str = "timeout"; + problem = false; // A timeout is not a sign of a bug es = -1; } else if (WIFSIGNALED(es)) { status_str = "signal"; + problem = true; es = WTERMSIG(es); global_error() << "error: execution terminated by signal " << es << ".\n"; @@ -888,6 +904,7 @@ namespace { es = WEXITSTATUS(es); status_str = "exit code"; + problem = true; global_error() << "error: execution returned exit code " << es << ".\n"; end_error(); @@ -895,6 +912,7 @@ namespace else { status_str = "ok"; + problem = false; es = 0; switch (output.format) { @@ -906,6 +924,7 @@ namespace if (!pel.empty()) { status_str = "parse error"; + problem = true; es = -1; std::ostream& err = global_error(); err << "error: failed to parse the produced neverclaim.\n"; @@ -923,6 +942,7 @@ namespace if (!f) { status_str = "no output"; + problem = true; es = -1; global_error() << "Cannot open " << output.val() << std::endl; @@ -934,6 +954,7 @@ namespace if (!res) { status_str = "parse error"; + problem = true; es = -1; global_error() << ("error: failed to parse output in " "LBTT format: ") @@ -952,6 +973,7 @@ namespace if (!pel.empty()) { status_str = "parse error"; + problem = true; es = -1; std::ostream& err = global_error(); err << "error: failed to parse the produced DSTAR" @@ -1048,7 +1070,7 @@ namespace } }; - static void + static bool check_empty_prod(const spot::tgba* aut_i, const spot::tgba* aut_j, size_t i, size_t j, bool icomp, bool jcomp) { @@ -1091,9 +1113,10 @@ namespace delete res; delete ec; delete prod; + return res; } - static void + static bool cross_check(const std::vector& maps, char l, unsigned p) { size_t m = maps.size(); @@ -1146,7 +1169,9 @@ namespace else err << "the state-space\n"; end_error(); + return true; } + return false; } typedef std::set state_set; @@ -1212,12 +1237,35 @@ namespace (*i++)->destroy(); } + int + process_string(const std::string& input, + const char* filename, + int linenum) + { + spot::ltl::parse_error_list pel; + const spot::ltl::formula* f = parse_formula(input, pel); + + if (!f || !pel.empty()) + { + if (filename) + error_at_line(0, 0, filename, linenum, "parse error:"); + spot::ltl::format_parse_errors(std::cerr, input, pel); + if (f) + f->destroy(); + return 1; + } + int res = process_formula(f, filename, linenum); + + if (res && bogus_output) + *bogus_output << input << std::endl; + return 0; + } + + int process_formula(const spot::ltl::formula* f, const char* filename = 0, int linenum = 0) { - (void) filename; - (void) linenum; static unsigned round = 0; // If we need LBT atomic proposition in any of the input or @@ -1268,6 +1316,9 @@ namespace } } + + int problems = 0; + // These store the result of the translation of the positive and // negative formulas. size_t m = translators.size(); @@ -1288,7 +1339,10 @@ namespace for (size_t n = 0; n < m; ++n) { - pos[n] = runner.translate(n, 'P', pstats); + bool prob; + pos[n] = runner.translate(n, 'P', pstats, prob); + problems += prob; + // If the automaton is deterministic, compute its complement // as well. Note that if we have computed statistics // already, there is no need to call is_deterministic() @@ -1326,7 +1380,10 @@ namespace for (size_t n = 0; n < m; ++n) { - neg[n] = runner.translate(n, 'N', nstats); + bool prob; + neg[n] = runner.translate(n, 'N', nstats, prob); + problems += prob; + // If the automaton is deterministic, compute its // complement as well. Note that if we have computed // statistics already, there is no need to call @@ -1353,7 +1410,8 @@ namespace for (size_t j = 0; j < m; ++j) if (neg[j]) { - check_empty_prod(pos[i], neg[j], i, j, false, false); + problems += + check_empty_prod(pos[i], neg[j], i, j, false, false); // Deal with the extra complemented automata if we // have some. @@ -1371,13 +1429,18 @@ namespace // translation was not deterministic. if (i != j && comp_pos[j] && !comp_neg[j]) - check_empty_prod(pos[i], comp_pos[j], i, j, false, true); + problems += + check_empty_prod(pos[i], comp_pos[j], + i, j, false, true); if (i != j && comp_neg[i] && !comp_neg[i]) - check_empty_prod(comp_neg[i], neg[j], i, j, true, false); + problems += + check_empty_prod(comp_neg[i], neg[j], + i, j, true, false); if (comp_pos[i] && comp_neg[j] && (i == j || (!comp_neg[i] && !comp_pos[j]))) - check_empty_prod(comp_pos[i], comp_neg[j], - i, j, true, true); + problems += + check_empty_prod(comp_pos[i], comp_neg[j], + i, j, true, true); } } else @@ -1457,14 +1520,16 @@ namespace if (!no_checks) { // cross-comparison test - cross_check(pos_map, 'P', p); - cross_check(neg_map, 'N', p); + problems += cross_check(pos_map, 'P', p); + problems += cross_check(neg_map, 'N', p); // consistency check for (size_t i = 0; i < m; ++i) if (pos_map[i] && neg_map[i] && !(consistency_check(pos_map[i], neg_map[i], statespace))) { + ++problems; + std::ostream& err = global_error(); err << "error: inconsistency between P" << i << " and N" << i; @@ -1507,7 +1572,7 @@ namespace // Shall we stop processing formulas now? abort_run = global_error_flag && stop_on_error; - return 0; + return problems; } }; } @@ -1525,7 +1590,7 @@ print_stats_csv(const char* filename) else { out = outfile = new std::ofstream(filename); - if (!outfile) + if (!*outfile) error(2, errno, "cannot open '%s'", filename); } @@ -1563,7 +1628,7 @@ print_stats_json(const char* filename) else { out = outfile = new std::ofstream(filename); - if (!outfile) + if (!*outfile) error(2, errno, "cannot open '%s'", filename); } @@ -1642,10 +1707,16 @@ main(int argc, char** argv) if (global_error_flag) { std::ostream& err = global_error(); - err << ("error: some error was detected during the above runs,\n" - " please search for 'error:' messages in the above " - "trace.") - << std::endl; + if (bogus_output) + err << ("error: some error was detected during the above runs.\n" + " Check file ") + << bogus_output_filename + << " for problematic formulas."; + else + err << ("error: some error was detected during the above runs,\n" + " please search for 'error:' messages in the above" + " trace."); + err << std::endl; if (timeout_count == 1) err << "Additionally, 1 timeout occurred." << std::endl; else if (timeout_count > 1) @@ -1662,6 +1733,8 @@ main(int argc, char** argv) << " timeouts, but no other problem detected." << std::endl; } + delete bogus_output; + if (json_output) print_stats_json(json_output); if (csv_output) diff --git a/src/tgbatest/ltlcross3.test b/src/tgbatest/ltlcross3.test index 386afbe25..2ecfe25fb 100755 --- a/src/tgbatest/ltlcross3.test +++ b/src/tgbatest/ltlcross3.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2012, 2013 Laboratoire de Recherche et +# Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -55,13 +55,18 @@ test `grep '"exit code",1' out.csv | wc -l` -eq 0 check_csv out.csv # Likewise for timeouts +echo foo >bug run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \ - --timeout 2 -f a --csv=out.csv 2>stderr + --timeout 2 -f a --csv=out.csv \ + --save-bogus=bug 2>stderr grep '"exit_status"' out.csv grep '"exit_code"' out.csv test `grep 'warning:.*timeout' stderr | wc -l` -eq 2 test `grep '"timeout",-1' out.csv | wc -l` -eq 2 check_csv out.csv +# 'bug' should exist but be empty +test -f bug +test -s bug && exit 1 run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \ --timeout 2 --omit-missing -f a --csv=out.csv 2>stderr @@ -115,12 +120,13 @@ test $q -eq `expr $p + 12` # Check with Rabin/Streett output run 1 ../../bin/ltlcross "$ltl2tgba -s %f >%N" 'false %f >%D' \ - -f a --csv=out.csv 2>stderr + -f 'X a' --csv=out.csv --save-bogus=bug.txt 2>stderr q=`sed 's/[^,]//g;q' out.csv | wc -c` grep '"exit_status"' out.csv grep '"exit_code"' out.csv test `grep 'error:.*returned exit code 1' stderr | wc -l` -eq 2 test `grep '"exit code",1' out.csv | wc -l` -eq 2 check_csv out.csv +grep 'X a' bug.txt test $q -eq `expr $p + 6`