Commit 183ec1fb authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

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.
parent 0a2bca13
...@@ -36,6 +36,8 @@ New in spot 2.4.1.dev (not yet released) ...@@ -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. - 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 - The new -x tls-impl=N option allows to fine-tune the
implication-based simplification rules of ltl2tgba. See the implication-based simplification rules of ltl2tgba. See the
spot-x man-page for details. spot-x man-page for details.
......
...@@ -35,6 +35,7 @@ Rüdiger Ehlers ...@@ -35,6 +35,7 @@ Rüdiger Ehlers
Silien Hong Silien Hong
Shufang Zhu Shufang Zhu
Sonali Dutta Sonali Dutta
Tobias Meggendorfer.
Tomáš Babiak Tomáš Babiak
Valentin Iovene Valentin Iovene
Vitus Lam Vitus Lam
......
...@@ -59,7 +59,7 @@ Call several tools that process automata and cross-compare their output \ ...@@ -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 \ 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\ should be supplied on standard input, or using the -F option.\v\
Exit status:\n\ 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\ 1 some tools failed to output something we understand, or failed\n\
sanity checks (statistics were output nonetheless)\n\ sanity checks (statistics were output nonetheless)\n\
2 autcross aborted on error\n\ 2 autcross aborted on error\n\
...@@ -69,6 +69,7 @@ enum { ...@@ -69,6 +69,7 @@ enum {
OPT_BOGUS = 256, OPT_BOGUS = 256,
OPT_CSV, OPT_CSV,
OPT_HIGH, OPT_HIGH,
OPT_FAIL_ON_TIMEOUT,
OPT_IGNORE_EXEC_FAIL, OPT_IGNORE_EXEC_FAIL,
OPT_LANG, OPT_LANG,
OPT_LOW, OPT_LOW,
...@@ -92,6 +93,8 @@ static const argp_option options[] = ...@@ -92,6 +93,8 @@ static const argp_option options[] =
{ "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0, { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0,
"ignore automata from translators that return with a non-zero exit code," "ignore automata from translators that return with a non-zero exit code,"
" but do not flag this as an error", 0 }, " 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, { "language-preserved", OPT_LANG, nullptr, 0,
"expect that each tool preserves the input language", 0 }, "expect that each tool preserves the input language", 0 },
{ "no-checks", OPT_NOCHECKS, nullptr, 0, { "no-checks", OPT_NOCHECKS, nullptr, 0,
...@@ -137,6 +140,7 @@ const struct argp_child children[] = ...@@ -137,6 +140,7 @@ const struct argp_child children[] =
static bool verbose = false; static bool verbose = false;
static bool ignore_exec_fail = false; static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0; static unsigned ignored_exec_fail = 0;
static bool fail_on_timeout = false;
static bool stop_on_error = false; static bool stop_on_error = false;
static bool no_checks = false; static bool no_checks = false;
static bool opt_language_preserved = false; static bool opt_language_preserved = false;
...@@ -163,6 +167,9 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -163,6 +167,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_CSV: case OPT_CSV:
csv_output = arg ? arg : "-"; csv_output = arg ? arg : "-";
break; break;
case OPT_FAIL_ON_TIMEOUT:
fail_on_timeout = true;
break;
case OPT_HIGH: case OPT_HIGH:
level = spot::postprocessor::High; level = spot::postprocessor::High;
level_set = true; level_set = true;
...@@ -392,11 +399,18 @@ namespace ...@@ -392,11 +399,18 @@ namespace
spot::twa_graph_ptr res = nullptr; spot::twa_graph_ptr res = nullptr;
if (timed_out) if (timed_out)
{ {
// This is not considered to be a global error. if (fail_on_timeout)
std::cerr << "warning: timeout during execution of command\n"; {
++timeout_count; 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"; status_str = "timeout";
problem = false; // A timeout is not a sign of a bug problem = fail_on_timeout;
es = -1; es = -1;
} }
else if (WIFSIGNALED(es)) else if (WIFSIGNALED(es))
......
...@@ -74,7 +74,7 @@ Call several LTL/PSL translators and cross-compare their output to detect \ ...@@ -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 \ 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\ supplied on standard input, or using the -f or -F options.\v\
Exit status:\n\ 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\ 1 some translator failed to output something we understand, or failed\n\
sanity checks (statistics were output nonetheless)\n\ sanity checks (statistics were output nonetheless)\n\
2 ltlcross aborted on error\n\ 2 ltlcross aborted on error\n\
...@@ -87,6 +87,7 @@ enum { ...@@ -87,6 +87,7 @@ enum {
OPT_CSV, OPT_CSV,
OPT_DENSITY, OPT_DENSITY,
OPT_DUPS, OPT_DUPS,
OPT_FAIL_ON_TIMEOUT,
OPT_GRIND, OPT_GRIND,
OPT_IGNORE_EXEC_FAIL, OPT_IGNORE_EXEC_FAIL,
OPT_JSON, OPT_JSON,
...@@ -121,6 +122,8 @@ static const argp_option options[] = ...@@ -121,6 +122,8 @@ static const argp_option options[] =
{ "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0, { "ignore-execution-failures", OPT_IGNORE_EXEC_FAIL, nullptr, 0,
"ignore automata from translators that return with a non-zero exit code," "ignore automata from translators that return with a non-zero exit code,"
" but do not flag this as an error", 0 }, " 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 }, { nullptr, 0, nullptr, 0, "State-space generation:", 6 },
{ "states", OPT_STATES, "INT", 0, { "states", OPT_STATES, "INT", 0,
...@@ -199,6 +202,7 @@ static output_file* grind_output = nullptr; ...@@ -199,6 +202,7 @@ static output_file* grind_output = nullptr;
static bool verbose = false; static bool verbose = false;
static bool ignore_exec_fail = false; static bool ignore_exec_fail = false;
static unsigned ignored_exec_fail = 0; static unsigned ignored_exec_fail = 0;
static bool fail_on_timeout = false;
static bool opt_automata = false; static bool opt_automata = false;
static bool opt_strength = false; static bool opt_strength = false;
static bool opt_ambiguous = false; static bool opt_ambiguous = false;
...@@ -445,6 +449,9 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -445,6 +449,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_DUPS: case OPT_DUPS:
allow_dups = true; allow_dups = true;
break; break;
case OPT_FAIL_ON_TIMEOUT:
fail_on_timeout = true;
break;
case OPT_GRIND: case OPT_GRIND:
grind_output = new output_file(arg); grind_output = new output_file(arg);
break; break;
...@@ -530,11 +537,18 @@ namespace ...@@ -530,11 +537,18 @@ namespace
spot::twa_graph_ptr res = nullptr; spot::twa_graph_ptr res = nullptr;
if (timed_out) if (timed_out)
{ {
// This is not considered to be a global error. if (fail_on_timeout)
std::cerr << "warning: timeout during execution of command\n"; {
++timeout_count; 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"; status_str = "timeout";
problem = false; // A timeout is not a sign of a bug problem = fail_on_timeout;
es = -1; es = -1;
} }
else if (WIFSIGNALED(es)) else if (WIFSIGNALED(es))
......
...@@ -53,6 +53,7 @@ enum { ...@@ -53,6 +53,7 @@ enum {
OPT_ERRORS = 256, OPT_ERRORS = 256,
OPT_SMALLEST, OPT_SMALLEST,
OPT_GREATEST, OPT_GREATEST,
OPT_FAIL_ON_TIMEOUT,
}; };
static const argp_option options[] = static const argp_option options[] =
...@@ -62,6 +63,8 @@ static const argp_option options[] = ...@@ -62,6 +63,8 @@ static const argp_option options[] =
{ "errors", OPT_ERRORS, "abort|warn|ignore", 0, { "errors", OPT_ERRORS, "abort|warn|ignore", 0,
"how to deal with tools returning with non-zero exit codes or " "how to deal with tools returning with non-zero exit codes or "
"automata that ltldo cannot parse (default: abort)", 0 }, "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 }, { nullptr, 0, nullptr, 0, "Output selection:", 5 },
{ "smallest", OPT_SMALLEST, "FORMAT", OPTION_ARG_OPTIONAL, { "smallest", OPT_SMALLEST, "FORMAT", OPTION_ARG_OPTIONAL,
...@@ -122,7 +125,7 @@ build_percent_list() ...@@ -122,7 +125,7 @@ build_percent_list()
enum errors_type { errors_abort, errors_warn, errors_ignore }; enum errors_type { errors_abort, errors_warn, errors_ignore };
static errors_type errors_opt; static errors_type errors_opt;
static bool fail_on_timeout = false;
static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection static int best_type = 0; // -1 smallest, 1 greatest, 0 no selection
static const char* best_format = "%s,%e"; static const char* best_format = "%s,%e";
static int opt_max_count = -1; static int opt_max_count = -1;
...@@ -162,6 +165,9 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -162,6 +165,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_ERRORS: case OPT_ERRORS:
errors_opt = XARGMATCH("--errors", arg, errors_args, errors_types); errors_opt = XARGMATCH("--errors", arg, errors_args, errors_types);
break; break;
case OPT_FAIL_ON_TIMEOUT:
fail_on_timeout = true;
break;
case OPT_GREATEST: case OPT_GREATEST:
best_type = 1; best_type = 1;
if (arg) if (arg)
...@@ -218,9 +224,18 @@ namespace ...@@ -218,9 +224,18 @@ namespace
if (timed_out) if (timed_out)
{ {
// A timeout is considered benign // 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"; << cmd << "\"\n";
++timeout_count;
} }
else if (WIFSIGNALED(es)) else if (WIFSIGNALED(es))
{ {
......
...@@ -319,7 +319,7 @@ Incoherence between the output of several tools (even with ...@@ -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 The =--stop-on-error= option will cause =autcross= to abort on the
first detected error. This include failure to start some tool, first detected error. This include failure to start some tool,
read its output, or failure to passe the sanity checks. Timeouts are 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 One use for this option is when =autcross= is used in combination with
=randaut= to check tools on an infinite stream of formulas. =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 ...@@ -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 The =--save-bogus=FILENAME= will save any automaton for which an error
was detected (either some tool failed, or some problem was was detected (either some tool failed, or some problem was
detected using the resulting automata) in =FILENAME=. Again, timeouts detected using the resulting automata) in =FILENAME=. Again, timeouts
are not considered to be errors, and therefore not reported in this are not considered to be errors and therefore not reported in this
file. file, unless =--fail-on-timeout= is given.
The main use for this feature is in conjunction with =randaut='s The main use for this feature is in conjunction with =randaut='s
generation of random formulas. For instance the following command generation of random formulas. For instance the following command
......
...@@ -733,7 +733,7 @@ automaton as well. ...@@ -733,7 +733,7 @@ automaton as well.
The =--stop-on-error= option will cause =ltlcross= to abort on the The =--stop-on-error= option will cause =ltlcross= to abort on the
first detected error. This include failure to start some translator, first detected error. This include failure to start some translator,
read its output, or failure to passe the sanity checks. Timeouts are 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 One use for this option is when =ltlcross= is used in combination with
=randltl= to check translators on an infinite stream of formulas. =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 ...@@ -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 The =--save-bogus=FILENAME= will save any formula for which an error
was detected (either some translation failed, or some problem was was detected (either some translation failed, or some problem was
detected using the resulting automata) in =FILENAME=. Again, timeouts detected using the resulting automata) in =FILENAME=. Again, timeouts
are not considered to be errors, and therefore not reported in this are not considered to be errors and therefore not reported in this
file. file, unless =--fail-on-timeout= is given.
The main use for this feature is in conjunction with =randltl='s The main use for this feature is in conjunction with =randltl='s
generation of random formulas. For instance the following command generation of random formulas. For instance the following command
......
...@@ -626,7 +626,9 @@ When a timeout occurs a warning is printed on stderr, and no automaton ...@@ -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 (or statistic) is output by =ltdo= for this specific pair of
command/formula. The processing then continue with other formulas and command/formula. The processing then continue with other formulas and
tools. Timeouts are not considered as errors, so they have no effect 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 For each command (that does not terminate with a timeout) the runtime
can be printed using the =%r= escape sequence. This makes =ltldo= an can be printed using the =%r= escape sequence. This makes =ltldo= an
......
...@@ -299,6 +299,7 @@ TESTS_twa = \ ...@@ -299,6 +299,7 @@ TESTS_twa = \
core/ltlcross2.test \ core/ltlcross2.test \
core/autcross.test \ core/autcross.test \
core/autcross2.test \ core/autcross2.test \
core/autcross3.test \
core/complementation.test \ core/complementation.test \
core/randpsl.test \ core/randpsl.test \
core/cycles.test \ core/cycles.test \
......
#!/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 <http://www.gnu.org/licenses/>.
# 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
...@@ -124,6 +124,20 @@ test `grep 'warning:.*timeout' stderr | wc -l` -eq 2 ...@@ -124,6 +124,20 @@ test `grep 'warning:.*timeout' stderr | wc -l` -eq 2
test `wc -l < out.csv` -eq 1 test `wc -l < out.csv` -eq 1
check_csv out.csv 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 # Check with --products=5 --automata
run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \ run 1 ltlcross "$ltl2tgba -s %f >%N" 'false %f >%N' \
-f a --csv=out.csv --products=5 --automata 2>stderr -f a --csv=out.csv --products=5 --automata 2>stderr
......
...@@ -42,13 +42,27 @@ EOF ...@@ -42,13 +42,27 @@ EOF
diff output expected 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 | $genltl --or-g=1..2 |
run 0 $ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \ run 0 $ltldo -t 'sleep 10; echo %f' -T1 -t 'sleep 10; echo %f' \
>output 2>stderr >output 2>stderr
test -z "`cat output`" test -z "`cat output`"
test 4 = `grep -c warning: stderr` 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' test "`echo 1,a,3,4 | ltldo -F-/2 ltl2tgba --stats='%<,%s,%>'`" = '1,2,3,4'
$genltl --and-gf=1..3 | $genltl --and-gf=1..3 |
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment