From 183ec1fb4e7e97afad03f8016ca00a3100a3218a Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 15 Oct 2017 10:44:26 +0200 Subject: [PATCH] ltlcross, autcross, ltldo: support --fail-on-timeout Suggested by Tobias Meggendorfer. Fixes #294. * bin/autcross.cc, bin/ltlcross.cc, bin/ltldo.cc: Add the option. * tests/core/autcross3.test, tests/core/ltlcross3.test, tests/core/ltldo.test: Test it. * tests/Makefile.am: Add autcross3.test. * NEWS, doc/org/autcross.org, doc/org/ltlcross.org, doc/org/ltldo.org: Mention the option. * THANKS: Add Tobias. --- NEWS | 2 ++ THANKS | 1 + bin/autcross.cc | 24 +++++++++++++++---- bin/ltlcross.cc | 24 +++++++++++++++---- bin/ltldo.cc | 21 ++++++++++++++--- doc/org/autcross.org | 6 ++--- doc/org/ltlcross.org | 6 ++--- doc/org/ltldo.org | 4 +++- tests/Makefile.am | 1 + tests/core/autcross3.test | 49 +++++++++++++++++++++++++++++++++++++++ tests/core/ltlcross3.test | 14 +++++++++++ tests/core/ltldo.test | 16 ++++++++++++- 12 files changed, 147 insertions(+), 21 deletions(-) create mode 100755 tests/core/autcross3.test diff --git a/NEWS b/NEWS index c7e5e1136..d4e0ce65e 100644 --- a/NEWS +++ b/NEWS @@ -36,6 +36,8 @@ New in spot 2.4.1.dev (not yet released) - ltldo learned to limit the number of automata it outputs using -n. + - autcross, ltlcross, and ltldo learned --fail-on-timeout. + - The new -x tls-impl=N option allows to fine-tune the implication-based simplification rules of ltl2tgba. See the spot-x man-page for details. diff --git a/THANKS b/THANKS index 7a235bdc6..9001306dc 100644 --- a/THANKS +++ b/THANKS @@ -35,6 +35,7 @@ Rüdiger Ehlers Silien Hong Shufang Zhu Sonali Dutta +Tobias Meggendorfer. Tomáš Babiak Valentin Iovene Vitus Lam diff --git a/bin/autcross.cc b/bin/autcross.cc index 15a12ed09..e7defaa89 100644 --- a/bin/autcross.cc +++ b/bin/autcross.cc @@ -59,7 +59,7 @@ Call several tools that process automata and cross-compare their output \ to detect bugs, or to gather statistics. The list of automata to use \ should be supplied on standard input, or using the -F option.\v\ Exit status:\n\ - 0 everything went fine (timeouts are OK too)\n\ + 0 everything went fine (without --fail-on-timeout, timeouts are OK)\n\ 1 some tools failed to output something we understand, or failed\n\ sanity checks (statistics were output nonetheless)\n\ 2 autcross aborted on error\n\ @@ -69,6 +69,7 @@ enum { OPT_BOGUS = 256, OPT_CSV, OPT_HIGH, + OPT_FAIL_ON_TIMEOUT, OPT_IGNORE_EXEC_FAIL, OPT_LANG, OPT_LOW, @@ -92,6 +93,8 @@ static const argp_option options[] = { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0, "ignore automata from translators that return with a non-zero exit code," " but do not flag this as an error", 0 }, + { "fail-on-timeout", OPT_FAIL_ON_TIMEOUT, nullptr, 0, + "consider timeouts as errors", 0 }, { "language-preserved", OPT_LANG, nullptr, 0, "expect that each tool preserves the input language", 0 }, { "no-checks", OPT_NOCHECKS, nullptr, 0, @@ -137,6 +140,7 @@ const struct argp_child children[] = static bool verbose = false; static bool ignore_exec_fail = false; static unsigned ignored_exec_fail = 0; +static bool fail_on_timeout = false; static bool stop_on_error = false; static bool no_checks = false; static bool opt_language_preserved = false; @@ -163,6 +167,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_CSV: csv_output = arg ? arg : "-"; break; + case OPT_FAIL_ON_TIMEOUT: + fail_on_timeout = true; + break; case OPT_HIGH: level = spot::postprocessor::High; level_set = true; @@ -392,11 +399,18 @@ namespace spot::twa_graph_ptr res = nullptr; if (timed_out) { - // This is not considered to be a global error. - std::cerr << "warning: timeout during execution of command\n"; - ++timeout_count; + if (fail_on_timeout) + { + global_error() << "error: timeout during execution of command\n"; + end_error(); + } + else + { + 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 + problem = fail_on_timeout; es = -1; } else if (WIFSIGNALED(es)) diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index 7410140a1..47cd9e749 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -74,7 +74,7 @@ Call several LTL/PSL translators and cross-compare their output to detect \ bugs, or to gather statistics. The list of formulas to use should be \ supplied on standard input, or using the -f or -F options.\v\ Exit status:\n\ - 0 everything went fine (timeouts are OK too)\n\ + 0 everything went fine (without --fail-on-timeout, timeouts are OK)\n\ 1 some translator failed to output something we understand, or failed\n\ sanity checks (statistics were output nonetheless)\n\ 2 ltlcross aborted on error\n\ @@ -87,6 +87,7 @@ enum { OPT_CSV, OPT_DENSITY, OPT_DUPS, + OPT_FAIL_ON_TIMEOUT, OPT_GRIND, OPT_IGNORE_EXEC_FAIL, OPT_JSON, @@ -121,6 +122,8 @@ static const argp_option options[] = { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0, "ignore automata from translators that return with a non-zero exit code," " but do not flag this as an error", 0 }, + { "fail-on-timeout", OPT_FAIL_ON_TIMEOUT, nullptr, 0, + "consider timeouts as errors", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "State-space generation:", 6 }, { "states", OPT_STATES, "INT", 0, @@ -199,6 +202,7 @@ static output_file* grind_output = nullptr; static bool verbose = false; static bool ignore_exec_fail = false; static unsigned ignored_exec_fail = 0; +static bool fail_on_timeout = false; static bool opt_automata = false; static bool opt_strength = false; static bool opt_ambiguous = false; @@ -445,6 +449,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_DUPS: allow_dups = true; break; + case OPT_FAIL_ON_TIMEOUT: + fail_on_timeout = true; + break; case OPT_GRIND: grind_output = new output_file(arg); break; @@ -530,11 +537,18 @@ namespace spot::twa_graph_ptr res = nullptr; if (timed_out) { - // This is not considered to be a global error. - std::cerr << "warning: timeout during execution of command\n"; - ++timeout_count; + if (fail_on_timeout) + { + global_error() << "error: timeout during execution of command\n"; + end_error(); + } + else + { + 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 + problem = fail_on_timeout; es = -1; } else if (WIFSIGNALED(es)) diff --git a/bin/ltldo.cc b/bin/ltldo.cc index e99d7d29c..b28203ec9 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -53,6 +53,7 @@ enum { OPT_ERRORS = 256, OPT_SMALLEST, OPT_GREATEST, + OPT_FAIL_ON_TIMEOUT, }; static const argp_option options[] = @@ -62,6 +63,8 @@ static const argp_option options[] = { "errors", OPT_ERRORS, "abort|warn|ignore", 0, "how to deal with tools returning with non-zero exit codes or " "automata that ltldo cannot parse (default: abort)", 0 }, + { "fail-on-timeout", OPT_FAIL_ON_TIMEOUT, nullptr, 0, + "consider timeouts as errors", 0 }, /**************************************************/ { nullptr, 0, nullptr, 0, "Output selection:", 5 }, { "smallest", OPT_SMALLEST, "FORMAT", OPTION_ARG_OPTIONAL, @@ -122,7 +125,7 @@ build_percent_list() enum errors_type { errors_abort, errors_warn, errors_ignore }; static errors_type errors_opt; - +static bool fail_on_timeout = false; static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection static const char* best_format = "%s,%e"; static int opt_max_count = -1; @@ -162,6 +165,9 @@ parse_opt(int key, char* arg, struct argp_state*) case OPT_ERRORS: errors_opt = XARGMATCH("--errors", arg, errors_args, errors_types); break; + case OPT_FAIL_ON_TIMEOUT: + fail_on_timeout = true; + break; case OPT_GREATEST: best_type = 1; if (arg) @@ -218,9 +224,18 @@ namespace if (timed_out) { // A timeout is considered benign - std::cerr << "warning: timeout during execution of command \"" + if (fail_on_timeout) + { + std::cerr << "error:"; + problem = true; + } + else + { + std::cerr << "warning:"; + ++timeout_count; + } + std::cerr << " timeout during execution of command \"" << cmd << "\"\n"; - ++timeout_count; } else if (WIFSIGNALED(es)) { diff --git a/doc/org/autcross.org b/doc/org/autcross.org index c0f04a6c5..1b4dc96f7 100644 --- a/doc/org/autcross.org +++ b/doc/org/autcross.org @@ -319,7 +319,7 @@ Incoherence between the output of several tools (even with The =--stop-on-error= option will cause =autcross= to abort on the first detected error. This include failure to start some tool, read its output, or failure to passe the sanity checks. Timeouts are -allowed. +allowed unless =--fail-on-timeout= is also given. One use for this option is when =autcross= is used in combination with =randaut= to check tools on an infinite stream of formulas. @@ -329,8 +329,8 @@ One use for this option is when =autcross= is used in combination with The =--save-bogus=FILENAME= will save any automaton for which an error was detected (either some tool 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. +are not considered to be errors and therefore not reported in this +file, unless =--fail-on-timeout= is given. The main use for this feature is in conjunction with =randaut='s generation of random formulas. For instance the following command diff --git a/doc/org/ltlcross.org b/doc/org/ltlcross.org index 64c98e0a5..669658376 100644 --- a/doc/org/ltlcross.org +++ b/doc/org/ltlcross.org @@ -733,7 +733,7 @@ automaton as well. 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. +allowed unless =--fail-on-time= is also given. One use for this option is when =ltlcross= is used in combination with =randltl= to check translators on an infinite stream of formulas. @@ -752,8 +752,8 @@ randltl -n -1 --tree-size 10..25 a b c | ltlcross --stop-on-error 'ltl2tgba --lb 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. +are not considered to be errors and therefore not reported in this +file, unless =--fail-on-timeout= is given. The main use for this feature is in conjunction with =randltl='s generation of random formulas. For instance the following command diff --git a/doc/org/ltldo.org b/doc/org/ltldo.org index 1c20622ab..09b31d06d 100644 --- a/doc/org/ltldo.org +++ b/doc/org/ltldo.org @@ -626,7 +626,9 @@ When a timeout occurs a warning is printed on stderr, and no automaton (or statistic) is output by =ltdo= for this specific pair of command/formula. The processing then continue with other formulas and tools. Timeouts are not considered as errors, so they have no effect -on the exit status of =ltldo=. +on the exit status of =ltldo=. This behavior can be changed with +option =--fail-on-timeout=, in which case timeouts are considered +as errors. For each command (that does not terminate with a timeout) the runtime can be printed using the =%r= escape sequence. This makes =ltldo= an diff --git a/tests/Makefile.am b/tests/Makefile.am index 42dc36dfe..017decc34 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -299,6 +299,7 @@ TESTS_twa = \ core/ltlcross2.test \ core/autcross.test \ core/autcross2.test \ + core/autcross3.test \ core/complementation.test \ core/randpsl.test \ core/cycles.test \ diff --git a/tests/core/autcross3.test b/tests/core/autcross3.test new file mode 100755 index 000000000..9afc50fe8 --- /dev/null +++ b/tests/core/autcross3.test @@ -0,0 +1,49 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2017 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# Test the timeout handling of autcross. +. ./defs +set -e + +check_csv() +{ + # Make sure all lines in $1 have the same number of comas + sed 's/[^,]//g' < "$1" | + ( read first + while read l; do + test "x$first" = "x$l" || exit 1 + done) +} + +randaut -Q4 2 | +autcross --language-preserve 'autfilt' 'sleep 5; autfilt %H > %O' \ + --timeout=2 --csv=out.csv 2>stderr +cat stderr +test `grep 'warning:.*timeout' stderr | wc -l` -eq 1 +test `wc -l < out.csv` -eq 3 +check_csv out.csv + +randaut -Q4 2 | +autcross --language-preserve 'autfilt' 'sleep 5; autfilt %H > %O' \ + --timeout=2 --fail-on-timeout --csv=out.csv 2>stderr && exit 1 +cat stderr +test `grep 'error:.*timeout' stderr | wc -l` -eq 1 +test `wc -l < out.csv` -eq 3 +check_csv out.csv diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index f4d23b9f5..625033dbe 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -124,6 +124,20 @@ test `grep 'warning:.*timeout' stderr | wc -l` -eq 2 test `wc -l < out.csv` -eq 1 check_csv out.csv +run 1 ltlcross 'sleep 5; false %f >%N' --fail-on-timeout \ + --timeout 2 -f a --csv=out.csv 2>stderr +test `grep 'error:.*timeout' stderr | wc -l` -eq 2 +test `wc -l < out.csv` -eq 3 +check_csv out.csv + +run 1 ltlcross 'sleep 5; false %f >%N' --fail-on-timeout \ + --stop-on-error --timeout 2 -f a -f b --csv=out.csv \ + --save-bogus=bogous 2>stderr +test `grep 'error:.*timeout' stderr | wc -l` -eq 2 +test `wc -l < out.csv` -eq 3 +test `wc -l < bogous` -eq 1 +check_csv out.csv + # Check with --products=5 --automata run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ -f a --csv=out.csv --products=5 --automata 2>stderr diff --git a/tests/core/ltldo.test b/tests/core/ltldo.test index 36e5e45d2..653bef6c9 100755 --- a/tests/core/ltldo.test +++ b/tests/core/ltldo.test @@ -42,13 +42,27 @@ EOF diff output expected -# Test timeouts. This test should take 2*2 seconds. +# Test timeouts. Each of these runs should take 2*2 seconds. $genltl --or-g=1..2 | run 0 $ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ >output 2>stderr test -z "`cat output`" test 4 = `grep -c warning: stderr` +genltl --or-g=1..2 | +run 0 ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ + --fail-on-timeout --error=warn >output 2>stderr +test -z "`cat output`" +test 4 = `grep -c error: stderr` +grep -q 'aborting here' stderr && exit 1 + +genltl --or-g=1..2 | +run 2 ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ + --fail-on-timeout >output 2>stderr +test -z "`cat output`" +test 1 = `grep -c error: stderr` +grep -q 'aborting here' stderr + test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4' $genltl --and-gf=1..3 | -- GitLab