diff --git a/NEWS b/NEWS index 423a16e95..85610c261 100644 --- a/NEWS +++ b/NEWS @@ -34,6 +34,11 @@ New in spot 2.6.0.dev (not yet released) - "ltlfilt --suspendable" is now a synonym for "ltlfilt --universal --eventual". + Bugs fixed: + + - scc_info::split_on_sets() did not correctly register the + atomic propositions of the returned automata. + New in spot 2.6 (2018-07-04) Command-line tools: diff --git a/spot/twaalgos/sccinfo.cc b/spot/twaalgos/sccinfo.cc index 16dbd1c7e..9f7097d92 100644 --- a/spot/twaalgos/sccinfo.cc +++ b/spot/twaalgos/sccinfo.cc @@ -528,6 +528,7 @@ namespace spot cur.assign(aut_->num_states(), false); auto copy = make_twa_graph(aut_->get_dict()); + copy->copy_ap_of(aut_); copy->copy_acceptance_of(aut_); copy->prop_state_acc(aut_->prop_state_acc()); transform_accessible(aut_, copy, [&](unsigned src, diff --git a/tests/Makefile.am b/tests/Makefile.am index c331d1a1e..6e2fadc28 100644 --- a/tests/Makefile.am +++ b/tests/Makefile.am @@ -400,6 +400,7 @@ TESTS_python = \ python/sbacc.py \ python/sccfilter.py \ python/sccinfo.py \ + python/sccsplit.py \ python/semidet.py \ python/setacc.py \ python/setxor.py \ diff --git a/tests/python/sccsplit.py b/tests/python/sccsplit.py new file mode 100644 index 000000000..cf8c0e33d --- /dev/null +++ b/tests/python/sccsplit.py @@ -0,0 +1,30 @@ +#!/usr/bin/python3 +# -*- mode: python; coding: utf-8 -*- +# Copyright (C) 2018 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 . + +import spot + +aut = spot.translate('GF(a <-> Xa) & GF(b <-> XXb)') +si = spot.scc_info(aut) +s = "" +for aut2 in si.split_on_sets(0, [0]): + # This call to to_str() used to fail because split_on_sets had not + # registered the atomic propositions of aut + s += aut2.to_str(); +assert spot.automaton(s).num_states() == 8