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

powerset: fix segfault when the initial state is a sink

Browse source 
Reported by Raven Beutner.

* spot/twaalgos/minimize.cc: Improve comment.
* spot/twaalgos/powerset.cc: Fix handling of an initial state that
is also a sink.
* tests/core/wdba2.test: Add test case.
* NEWS: Mention the bug.
This commit is contained in:
Alexandre Duret-Lutz 2023-04-18 15:04:58 +02:00
parent ae10361bdd
commit 0e54a85310
4 changed files with 55 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

3
NEWS
View file

@ -30,6 +30,9 @@ New in spot 2.11.4.dev (not yet released)
verbatim. We also changed the behavior of as_twa() to not merge
identical states.
- Fix segfaults occuring in determinization of 1-state terminal
automata.
New in spot 2.11.4 (2023-02-10)
Python:

6
spot/twaalgos/minimize.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2010-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2010-2020, 2023 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
@ -394,8 +394,8 @@ namespace spot
else
{
// Find any accepting sink state, to speed up the
// determinization by merging all states containing a sink
// state.
// determinization by merging all macro-states containing a
// sink state.
std::vector<unsigned> acc_sinks;
unsigned ns = a->num_states();
if (!a->prop_terminal().is_true())

26
spot/twaalgos/powerset.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2009-2011, 2013-2019, 2021 Laboratoire de Recherche et
// Copyright (C) 2009-2011, 2013-2019, 2021, 2023 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -217,17 +217,19 @@ namespace spot
pm.map_.emplace_back(std::move(ps));
}
{
unsigned init_num = aut->get_init_state_number();
auto bvi = make_bitvect(ns);
bvi->set(init_num);
power_state ps{init_num};
unsigned num = res->new_state();
res->set_init_state(num);
seen[bvi] = num;
assert(pm.map_.size() == num);
pm.map_.emplace_back(std::move(ps));
toclean.emplace_back(bvi);
// Add the initial state unless it's a sink.
if (unsigned init_num = aut->get_init_state_number();
!acc_sinks || !acc_sinks->get(init_num))
{
auto bvi = make_bitvect(ns);
bvi->set(init_num);
power_state ps{init_num};
unsigned num = res->new_state();
res->set_init_state(num);
seen[bvi] = num;
assert(pm.map_.size() == num);
pm.map_.emplace_back(std::move(ps));
toclean.emplace_back(bvi);
}
// outgoing map

37
tests/core/wdba2.test
View file

@ -1,7 +1,7 @@
#!/bin/sh
# -*- coding: utf-8 -*-
# Copyright (C) 2012, 2014, 2015, 2018, 2019 Laboratoire de Recherche et
# Développement de l'Epita (LRDE).
# Copyright (C) 2012, 2014-2015, 2018-2019, 2023 Laboratoire de
# Recherche et Développement de l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
#
@ -82,3 +82,36 @@ EOF
autfilt --small --high -C -Hi input > output
diff output expected
# This test comes from a report from Raven Beutner and used to cause a
# segfault.
cat >input <<EOF
HOA: v1
States: 1
Start: 0
AP: 3 "l0" "l1" "l2"
acc-name: generalized-Buchi 0
Acceptance: 0 t
--BODY--
State: 0
[0&1] 0
[2] 0
[!2] 0
--END--
EOF
autfilt --small -S input >output
cat >expected <<EOF
HOA: v1
States: 1
Start: 0
AP: 0
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc colored complete
properties: deterministic terminal
--BODY--
State: 0 {0}
[t] 0
--END--
EOF
diff output expected