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

autfilt: fix incorrect diagnostic

Browse source 
* bin/autfilt.cc (OPT_KEEP_STATES): Mention the correct option.
* tests/core/maskkeep.test: Test for it.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2021-02-19 15:58:49 +01:00
parent 7a56ae958e
commit da0dd4c534
3 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -189,6 +189,9 @@ New in spot 2.9.6.dev (not yet released)
- Some formulas using ->, <->, or xor were not properly detected as - Some formulas using ->, <->, or xor were not properly detected as
purely universal or pure eventualities. purely universal or pure eventualities.
- autfilt --keep-states=... could incorrectly mention --mask-acc
when diagnosing errors.
Deprecation notices: Deprecation notices:
- twa_graph::defrag_states() and digraph::defrag_states() now take - twa_graph::defrag_states() and digraph::defrag_states() now take

4
bin/autfilt.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2013-2020 Laboratoire de Recherche et Développement // Copyright (C) 2013-2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -1011,7 +1011,7 @@ parse_opt(int key, char* arg, struct argp_state*)
{ {
if (res < 0) if (res < 0)
error(2, 0, "state ids should be non-negative:" error(2, 0, "state ids should be non-negative:"
" --mask-acc=%ld", res); " --keep-states=%ld", res);
// We don't know yet how many states the automata contain. // We don't know yet how many states the automata contain.
if (opt_keep_states.size() <= static_cast<unsigned long>(res)) if (opt_keep_states.size() <= static_cast<unsigned long>(res))
opt_keep_states.resize(res + 1, false); opt_keep_states.resize(res + 1, false);

10
tests/core/maskkeep.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement # Copyright (C) 2015, 2016, 2021 Laboratoire de Recherche et Développement
# de l'Epita (LRDE). # de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -109,5 +109,9 @@ run 0 autfilt --keep-states=1,2,0 input1 -H >output
diff output expect4 diff output expect4
# Errors # Errors
run 2 autfilt --keep-states=a3 input1 run 2 autfilt --keep-states=a3 input1 2> error
run 2 autfilt --keep-states=3-2 input1 cat error
grep 'failed to parse' error
run 2 autfilt --keep-states=3-2 input1 2> error
cat error
grep 'non-negative: --keep-states' error