diff --git a/NEWS b/NEWS index 8148db94303cf02f1e385b1e478986b4d1f5d0ff..a23c3589e275a5245f80bffb19905ffc05b6651d 100644 --- a/NEWS +++ b/NEWS @@ -66,6 +66,10 @@ New in spot 2.1.2.dev (not yet released) * remove_fin() could produce incorrect result on incomplete automata tagged as weak and deterministic. + * calling set_acceptance() several time on an automaton could result + in unexpected behaviors, because set_acceptance(0,...) used to + set the state-based acceptance flag automatically. + New in spot 2.1.2 (2016-10-14) Command-line tools: diff --git a/THANKS b/THANKS index 1cb44319e8d544592d6872e5f7577e2985b78032..99800934b182554be18994c0066184c69d3d6dbe 100644 --- a/THANKS +++ b/THANKS @@ -18,6 +18,7 @@ Jan Strejček Jean-Michel Couvreur Jean-Michel Ilié Joachim Klein +Juraj Major Kristin Y. Rozier Martin Dieguez Lodeiro Matthias Heizmann diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 02a3f3a8e3cd8f41b5166803b804fdba2da4f507..06bbfea8edbb43542f5dd1dcd059c526ebe71468 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -879,17 +879,12 @@ namespace spot { set_num_sets_(num); acc_.set_acceptance(c); - if (num == 0) - prop_state_acc(true); } /// Copy the acceptance condition of another TωA. void copy_acceptance_of(const const_twa_ptr& a) { acc_ = a->acc(); - unsigned num = acc_.num_sets(); - if (num == 0) - prop_state_acc(true); } /// Copy the atomic propositions of another TωA @@ -915,8 +910,6 @@ namespace spot { set_num_sets_(num); acc_.set_generalized_buchi(); - if (num == 0) - prop_state_acc(true); } /// \brief Set Büchi acceptance. @@ -1092,6 +1085,8 @@ namespace spot /// the acceptance set. trival prop_state_acc() const { + if (num_sets() == 0) + return true; return is.state_based_acc; } diff --git a/tests/Makefile.am b/tests/Makefile.am index adf25ae451d0ac9230dbc937db62251453aa8082..bf8dd110dbe141657d0f97a1d0f4241700a270c8 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -341,6 +341,7 @@ TESTS_python = \ python/relabel.py \ python/remfin.py \ python/satmin.py \ + python/setacc.py \ python/setxor.py \ python/trival.py \ $(TESTS_ipython) diff --git a/tests/python/setacc.py b/tests/python/setacc.py new file mode 100644 index 0000000000000000000000000000000000000000..58f0feedd8143c847e4a27ecc5508a997efcbc7a --- /dev/null +++ b/tests/python/setacc.py @@ -0,0 +1,26 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2016 Laboratoire de Recherche et Développement de +# l'EPITA. +# +# 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 case reduced from a report from Juraj Major . +import spot +a = spot.make_twa_graph(spot._bdd_dict) +a.set_acceptance(0, spot.acc_code("t")) +a.set_acceptance(1, spot.acc_code("Fin(0)")) +assert(a.prop_state_acc() == 0);