diff --git a/NEWS b/NEWS index 2f66c8270..8622f8312 100644 --- a/NEWS +++ b/NEWS @@ -1,10 +1,13 @@ New in spot 2.9.6.dev (not yet released) - Nothing yet. + Bugs fixed: - Some formulas using ->, <->, or xor were not properly detected as purely universal or pure eventualities. + - autfilt --keep-states=... could incorrectly mention --mask-acc + when diagnosing errors. + New in spot 2.9.6 (2021-01-18) Build: diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 5cc3bda7e..49fcb04d5 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -1,5 +1,5 @@ // -*- 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). // // 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) 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. if (opt_keep_states.size() <= static_cast(res)) opt_keep_states.resize(res + 1, false); diff --git a/tests/core/maskkeep.test b/tests/core/maskkeep.test index 4fe4dbcf1..1188c1b67 100755 --- a/tests/core/maskkeep.test +++ b/tests/core/maskkeep.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- 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). # # 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 # Errors -run 2 autfilt --keep-states=a3 input1 -run 2 autfilt --keep-states=3-2 input1 +run 2 autfilt --keep-states=a3 input1 2> error +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