alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlcross: Add --ignore-execution-failures.

Browse source 
Suggested by Joachim Klein.

* src/bin/ltlcross.cc: Add --ignore-execution-failures.
* src/tgbatest/ltlcross3.test: Test it.
* NEWS: Mention it.
This commit is contained in:
Alexandre Duret-Lutz 2015-02-10 11:14:56 +01:00
parent 2786d0c652
commit afc8773de1
3 changed files with 90 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

4
NEWS
View file

@ -15,6 +15,10 @@ New in spot 1.99a (not yet released)
size of any bogus formula it discovers, while still exhibiting size of any bogus formula it discovers, while still exhibiting
the bug. the bug.
- ltlcross has a new option --ignore-execution-failures that
ignore translator returning non-zero exist status instead of
returning an error.
- randaut is a new tool that generates random automata. - randaut is a new tool that generates random automata.
- autfilt is a new tool that converts/filters/transforms a - autfilt is a new tool that converts/filters/transforms a

121
src/bin/ltlcross.cc
View file

@ -90,6 +90,7 @@ Exit status:\n\
#define OPT_BOGUS 13 #define OPT_BOGUS 13
#define OPT_VERBOSE 14 #define OPT_VERBOSE 14
#define OPT_GRIND 15 #define OPT_GRIND 15
#define OPT_IGNORE_EXEC_FAIL 16
static const argp_option options[] = static const argp_option options[] =
{ {
@ -105,6 +106,9 @@ static const argp_option options[] =
{ "stop-on-error", OPT_STOP_ERR, 0, 0, { "stop-on-error", OPT_STOP_ERR, 0, 0,
"stop on first execution error or failure to pass" "stop on first execution error or failure to pass"
" sanity checks (timeouts are OK)", 0 }, " sanity checks (timeouts are OK)", 0 },
{ "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, 0, 0,
"ignore automata from translators that return with a non-zero exit code,"
" but do not flag this as an error", 0 },
/**************************************************/ /**************************************************/
{ 0, 0, 0, 0, "State-space generation:", 6 }, { 0, 0, 0, 0, "State-space generation:", 6 },
{ "states", OPT_STATES, "INT", 0, { "states", OPT_STATES, "INT", 0,
@ -165,33 +169,34 @@ static color_type const color_types[] =
}; };
ARGMATCH_VERIFY(color_args, color_types); ARGMATCH_VERIFY(color_args, color_types);
color_type color_opt = color_if_tty; static color_type color_opt = color_if_tty;
const char* bright_red = "\033[01;31m"; static const char* bright_red = "\033[01;31m";
const char* bright_blue = "\033[01;34m"; static const char* bright_blue = "\033[01;34m";
const char* bright_yellow = "\033[01;33m"; static const char* bright_yellow = "\033[01;33m";
const char* reset_color = "\033[m"; static const char* reset_color = "\033[m";
unsigned states = 200; static unsigned states = 200;
float density = 0.1; static float density = 0.1;
const char* json_output = 0; static const char* json_output = 0;
const char* csv_output = 0; static const char* csv_output = 0;
bool want_stats = false; static bool want_stats = false;
bool allow_dups = false; static bool allow_dups = false;
bool no_checks = false; static bool no_checks = false;
bool no_complement = false; static bool no_complement = false;
bool stop_on_error = false; static bool stop_on_error = false;
int seed = 0; static int seed = 0;
unsigned products = 1; static unsigned products = 1;
bool products_avg = true; static bool products_avg = true;
bool opt_omit = false; static bool opt_omit = false;
bool has_sr = false; // Has Streett or Rabin automata to process. static bool has_sr = false; // Has Streett or Rabin automata to process.
const char* bogus_output_filename = 0; static const char* bogus_output_filename = 0;
std::ofstream* bogus_output = 0; static std::ofstream* bogus_output = 0;
std::ofstream* grind_output = 0; static std::ofstream* grind_output = 0;
bool verbose = false; static bool verbose = false;
static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0;
static bool global_error_flag = false;
bool global_error_flag = false;
static std::ostream& static std::ostream&
global_error() global_error()
@ -422,6 +427,9 @@ parse_opt(int key, char* arg, struct argp_state*)
if (!*grind_output) if (!*grind_output)
error(2, errno, "cannot open '%s'", arg); error(2, errno, "cannot open '%s'", arg);
break; break;
case OPT_IGNORE_EXEC_FAIL:
ignore_exec_fail = true;
break;
case OPT_JSON: case OPT_JSON:
want_stats = true; want_stats = true;
json_output = arg ? arg : "-"; json_output = arg ? arg : "-";
@ -517,10 +525,20 @@ namespace
{ {
es = WEXITSTATUS(es); es = WEXITSTATUS(es);
status_str = "exit code"; status_str = "exit code";
problem = true; if (!ignore_exec_fail)
global_error() << "error: execution returned exit code " {
<< es << ".\n"; problem = true;
end_error(); global_error() << "error: execution returned exit code "
<< es << ".\n";
end_error();
}
else
{
problem = false;
std::cerr << "warning: execution returned exit code "
<< es << ".\n";
++ignored_exec_fail;
}
} }
else else
{ {
@ -1393,20 +1411,43 @@ main(int argc, char** argv)
" please search for 'error:' messages in the above" " please search for 'error:' messages in the above"
" trace."); " trace.");
err << std::endl; err << std::endl;
if (timeout_count == 1) if (timeout_count > 0 || ignored_exec_fail > 0)
err << "Additionally, 1 timeout occurred." << std::endl; {
else if (timeout_count > 1) err << "Additionally, ";
err << "Additionally, " if (timeout_count == 1)
<< timeout_count << " timeouts occurred." << std::endl; err << "1 timeout occurred";
else if (timeout_count > 1)
err << timeout_count << " timeouts occurred";
if (timeout_count > 0 && ignored_exec_fail > 0)
err << " and ";
if (ignored_exec_fail == 1)
err << "1 non-zero exit status was ignored";
if (ignored_exec_fail > 1)
err << ignored_exec_fail
<< " non-zero exit statuses were ignored";
err << '.' << std::endl;
}
end_error(); end_error();
} }
else if (timeout_count == 0) else if (timeout_count == 0 && ignored_exec_fail == 0)
std::cerr << "No problem detected." << std::endl; {
else if (timeout_count == 1) std::cerr << "No problem detected." << std::endl;
std::cerr << "1 timeout, but no other problem detected." << std::endl; }
else else
std::cerr << timeout_count {
<< " timeouts, but no other problem detected." << std::endl; if (timeout_count == 1)
std::cerr << "1 timeout";
if (timeout_count > 1)
std::cerr << timeout_count << " timeouts";
if (timeout_count > 0 && ignored_exec_fail > 0)
std::cerr << " and ";
if (ignored_exec_fail == 1)
std::cerr << "1 non-zero exit status";
if (ignored_exec_fail > 1)
std::cerr << ignored_exec_fail
<< " non-zero exit statuses";
std::cerr << ", but no other problem detected." << std::endl;
}
} }
delete bogus_output; delete bogus_output;

6
src/tgbatest/ltlcross3.test
View file

@ -56,13 +56,17 @@ check_csv out.csv
# Likewise for timeouts # Likewise for timeouts
echo foo >bug echo foo >bug
run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' \ run 0 ../../bin/ltlcross 'sleep 5; false %f >%N' 'false %f >%N' \
--timeout 2 -f a --csv=out.csv \ --timeout 2 -f a --csv=out.csv \
--ignore-execution-failures \
--save-bogus=bug 2>stderr --save-bogus=bug 2>stderr
grep '"exit_status"' out.csv grep '"exit_status"' out.csv
grep '"exit_code"' out.csv grep '"exit_code"' out.csv
test `grep 'warning:.*timeout' stderr | wc -l` -eq 2 test `grep 'warning:.*timeout' stderr | wc -l` -eq 2
test `grep 'warning:.*exit code 1' stderr | wc -l` -eq 2
test `grep '"timeout",-1' out.csv | wc -l` -eq 2 test `grep '"timeout",-1' out.csv | wc -l` -eq 2
test `grep '"exit code",1' out.csv | wc -l` -eq 2
grep '2 timeouts and 2 non-zero exit statuses, but no other problem' stderr
check_csv out.csv check_csv out.csv
# 'bug' should exist but be empty # 'bug' should exist but be empty
test -f bug test -f bug