bin: abort autcross on input parse error
* bin/common_hoaread.hh (hoa_processor): Add a abort_on_error option. * bin/autcross.cc: Use it. * tests/core/autcross4.test: Add many more error cases to improve coverage.
This commit is contained in:
parent
faca835a5e
commit
1f9f3c77ea
4 changed files with 42 additions and 11 deletions
4
NEWS
4
NEWS
|
|
@ -5,6 +5,10 @@ New in spot 2.5.3.dev (not yet released)
|
||||||
- autcross' tool specifications now have %M replaced by the name of
|
- autcross' tool specifications now have %M replaced by the name of
|
||||||
the input automaton.
|
the input automaton.
|
||||||
|
|
||||||
|
- autcross now aborts if there is any parser diagnostic for the
|
||||||
|
input automata (previous versions would use the input automaton
|
||||||
|
whenever the parser would manage to read something).
|
||||||
|
|
||||||
- autfilt learned --is-colored to filter automata that use
|
- autfilt learned --is-colored to filter automata that use
|
||||||
exactly one acceptance set per mark or transition.
|
exactly one acceptance set per mark or transition.
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -542,7 +542,7 @@ namespace
|
||||||
autcross_runner runner;
|
autcross_runner runner;
|
||||||
public:
|
public:
|
||||||
autcross_processor()
|
autcross_processor()
|
||||||
: hoa_processor(spot::make_bdd_dict()), runner(dict_)
|
: hoa_processor(spot::make_bdd_dict(), true), runner(dict_)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -829,13 +829,13 @@ main(int argc, char** argv)
|
||||||
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
|
||||||
exit(err);
|
exit(err);
|
||||||
|
|
||||||
check_no_automaton();
|
|
||||||
|
|
||||||
auto s = tools.size();
|
auto s = tools.size();
|
||||||
if (s == 0)
|
if (s == 0)
|
||||||
error(2, 0, "No tool to run? Run '%s --help' for usage.",
|
error(2, 0, "No tool to run? Run '%s --help' for usage.",
|
||||||
program_name);
|
program_name);
|
||||||
|
|
||||||
|
check_no_automaton();
|
||||||
|
|
||||||
if (s == 1 && !opt_language_preserved && !no_checks)
|
if (s == 1 && !opt_language_preserved && !no_checks)
|
||||||
error(2, 0, "Since --language-preserved is not used, you need "
|
error(2, 0, "Since --language-preserved is not used, you need "
|
||||||
"at least two tools to compare.");
|
"at least two tools to compare.");
|
||||||
|
|
@ -845,8 +845,7 @@ main(int argc, char** argv)
|
||||||
setup_sig_handler();
|
setup_sig_handler();
|
||||||
|
|
||||||
autcross_processor p;
|
autcross_processor p;
|
||||||
if (p.run())
|
p.run();
|
||||||
return 2;
|
|
||||||
|
|
||||||
if (round_num == 0)
|
if (round_num == 0)
|
||||||
{
|
{
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement de
|
||||||
// l'Epita (LRDE).
|
// l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -45,10 +45,11 @@ class hoa_processor: public job_processor
|
||||||
{
|
{
|
||||||
protected:
|
protected:
|
||||||
spot::bdd_dict_ptr dict_;
|
spot::bdd_dict_ptr dict_;
|
||||||
|
bool abort_on_error_;
|
||||||
public:
|
public:
|
||||||
|
|
||||||
hoa_processor(spot::bdd_dict_ptr dict)
|
hoa_processor(spot::bdd_dict_ptr dict, bool abort_on_error = false)
|
||||||
: dict_(dict)
|
: dict_(dict), abort_on_error_(abort_on_error)
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -131,7 +132,7 @@ public:
|
||||||
break;
|
break;
|
||||||
if (haut->format_errors(std::cerr))
|
if (haut->format_errors(std::cerr))
|
||||||
err = 2;
|
err = 2;
|
||||||
if (!haut->aut)
|
if (!haut->aut || (err && abort_on_error_))
|
||||||
error(2, 0, "failed to read automaton from %s",
|
error(2, 0, "failed to read automaton from %s",
|
||||||
haut->filename.c_str());
|
haut->filename.c_str());
|
||||||
else if (haut->aborted)
|
else if (haut->aborted)
|
||||||
|
|
|
||||||
31
tests/core/autcross4.test
Normal file → Executable file
31
tests/core/autcross4.test
Normal file → Executable file
|
|
@ -18,7 +18,6 @@
|
||||||
# You should have received a copy of the GNU General Public License
|
# You should have received a copy of the GNU General Public License
|
||||||
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
# along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
# Test the timeout handling of autcross.
|
|
||||||
. ./defs
|
. ./defs
|
||||||
set -e
|
set -e
|
||||||
|
|
||||||
|
|
@ -48,6 +47,34 @@ State: 0
|
||||||
--END--
|
--END--
|
||||||
EOF
|
EOF
|
||||||
|
|
||||||
autcross -Fin 'ltl2tgba %[no]M>%O' 'ltl2tgba %M>%O' --csv=out.csv && exit 1
|
autcross --verbose \
|
||||||
|
-Fin 'ltl2tgba %[no]M>%O' 'ltl2tgba %M>%O' --csv=out.csv && exit 1
|
||||||
test 3 = `grep -c '"ok"' out.csv`
|
test 3 = `grep -c '"ok"' out.csv`
|
||||||
|
|
||||||
|
sed 's/AP: 0/AP: 0 "a"/g' in |
|
||||||
|
autcross --language-preserved autfilt 2>err && exit 1
|
||||||
|
grep 'autcross: failed to read automaton from -' err
|
||||||
|
|
||||||
|
autcross -T3 --verbose --language-preserved --ignore-execution-failures \
|
||||||
|
--csv=out.csv --omit-missing --low --medium --high --stop-on-error \
|
||||||
|
'sleep 10; autfilt %H>%O' 'false %H %O' 2>err -Fin
|
||||||
|
cat err
|
||||||
|
grep 'some error was detected' err && exit 1
|
||||||
|
grep 'No major problem' err
|
||||||
|
grep '2 timeouts occurred' err
|
||||||
|
grep '2 non-zero exit statuses were ignored' err
|
||||||
|
test 1 = `wc -l < out.csv`
|
||||||
|
|
||||||
|
autcross -T3 --verbose --language-preserved --ignore-execution-failures \
|
||||||
|
--csv=out.csv --omit-missing --low --medium --high --stop-on-error \
|
||||||
|
--fail-on-timeout \
|
||||||
|
'sleep 10; autfilt %H>%O' 'false %H %O' 2>err -Fin && exit 1
|
||||||
|
cat err
|
||||||
|
grep 'No major problem' err && exit 1
|
||||||
|
grep 'some error was detected ' err
|
||||||
|
grep '1 non-zero exit status was ignored' err
|
||||||
|
test 1 = `wc -l < out.csv`
|
||||||
|
|
||||||
|
autcross - 2> err && exit 1
|
||||||
|
cat err
|
||||||
|
grep 'autcross: No tool to run' err
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue