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

simplify_acceptance: fix handling of first edge

Browse source 
Fixes #315.

* spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Do not
compare the first edge against previous_a.
* tests/core/accsimpl.test: New file.
* tests/Makefile.am: Add it.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2018-01-06 09:13:52 +01:00
parent 17b295e10f
commit 2feba6ad5e
4 changed files with 67 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

7
NEWS
View file

@ -256,6 +256,13 @@ New in spot 2.4.4.dev (net yet released)
been removed. It's a low-level function was not used anywhere in
Spot anymore, since it's better to use spot::twa::copy_ap_of().
Bugs fixed:
- spot::simplify_acceptance() could produce incorrect output
if the first edge of the automaton was the only one with no
acceptance set. In spot 2.4.x this function was only used
by autfilt --simplify-acceptance.
New in spot 2.4.4 (2017-12-25)
Bugs fixed:

39
spot/twaalgos/cleanacc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2017 Laboratoire de Recherche et Développement
// Copyright (C) 2015, 2017, 2018 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -273,26 +273,45 @@ namespace spot
if (!used_in_cond)
return aut;
// complement[i] holds sets that appear when set #i does not.
unsigned num_sets = acc.num_sets();
std::vector<acc_cond::mark_t> complement(num_sets);
for (unsigned i = 0; i < num_sets; ++i)
if (used_in_cond.has(i))
complement[i] = used_in_cond - acc_cond::mark_t({i});
acc_cond::mark_t previous_a = 0U;
for (auto& t: aut->edges())
// Let's visit all edges to update complement[i]. To skip some
// duplicated work, prev_acc remember the "acc" sets of the
// previous edge, so we can skip consecutive edges with
// identical "acc" sets. Note that there is no value of
// prev_acc that would allow us to fail the comparison on the
// first edge (this was issue #315), so we have to deal with
// that first edge specifically.
acc_cond::mark_t prev_acc = 0U;
const auto& edges = aut->edges();
auto b = edges.begin();
auto e = edges.end();
auto update = [&](acc_cond::mark_t tacc)
{
if (t.acc == previous_a)
continue;
previous_a = t.acc;
prev_acc = tacc;
for (unsigned m: used_in_cond.sets())
{
if (t.acc.has(m))
complement[m] -= t.acc;
if (tacc.has(m))
complement[m] -= tacc;
else
complement[m] &= t.acc;
complement[m] &= tacc;
}
};
if (b != e)
{
update(b->acc);
++b;
while (b != e)
{
if (b->acc != prev_acc)
update(b->acc);
++b;
}
}
aut->set_acceptance(num_sets,

1
tests/Makefile.am
View file

@ -242,6 +242,7 @@ TESTS_twa = \
core/explpro4.test \
core/explsum.test \
core/dualize.test \
core/accsimpl.test \
core/tripprod.test \
core/dupexp.test \
core/exclusive-tgba.test \

30
tests/core/accsimpl.test Executable file
View file

@ -0,0 +1,30 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2018 Laboratoire de Recherche et Développement de
# l'Epita (LRDE).
#
# 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 <http://www.gnu.org/licenses/>.
. ./defs
set -e
# Issue #315
ltlcross -f FGa \
'ltl2tgba -G -D %f | autfilt --complement >%O' \
'ltl2tgba -G -D %f | autfilt --complement | autfilt --simplify-acceptance >%O'