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

gfguarantee: fix automaton modification during iteration

Browse source 
Fixes #449.

* spot/twaalgos/gfguarantee.cc (do_g_f_terminal_inplace): Save
edge additions to perform them after the loop.  Otherwise,
reallocating the edge buffer might break the iteration.
This commit is contained in:
Alexandre Duret-Lutz 2021-01-17 20:44:33 +01:00
parent 44c074bbad
commit 7a9f0a3fd9
1 changed files with 29 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

44
spot/twaalgos/gfguarantee.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2018 Laboratoire de Recherche et Développement // Copyright (C) 2018, 2021 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -268,7 +268,26 @@ namespace spot
} }
} }
// No we do the redirection. // No we do the redirections.
// We will modify most of the edges in place, but some cases
// require the addition of new edges. However we cannot add
// edges during the iteration, because that may reallocate
// the edge vector. So we postpone all edge creations by
// storing them into this array. All postponed additions
// correspond to Büchi accepting edges, so we do not have to
// store the mark_t.
struct edge_info {
edge_info(unsigned s, unsigned d, bdd c) noexcept
: src(s), dst(d), cond(c)
{
}
unsigned src;
unsigned dst;
bdd cond;
};
std::vector<edge_info> new_edges;
for (auto& e: aut->edges()) for (auto& e: aut->edges())
{ {
// Don't bother with terminal states, they won't be // Don't bother with terminal states, they won't be
@ -330,9 +349,7 @@ namespace spot
// combination. // combination.
bool ts = term[si.scc_of(ei.dst)]; bool ts = term[si.scc_of(ei.dst)];
if (ts) if (ts)
{ want_merge_edges = true;
want_merge_edges = true;
}
if (first) if (first)
{ {
e.acc = {0}; e.acc = {0};
@ -351,16 +368,10 @@ namespace spot
} }
else else
{ {
unsigned dst = ei.dst;
if (ts) if (ts)
{ new_init = dst = init;
aut->new_edge(e.src, init, cond, {0}); new_edges.emplace_back(e.src, dst, cond);
new_init = init;
}
else
{
aut->new_edge(e.src, ei.dst,
cond, {0});
}
} }
} }
} }
@ -382,7 +393,7 @@ namespace spot
} }
else else
{ {
aut->new_edge(e.src, ei.dst, cond, {0}); new_edges.emplace_back(e.src, ei.dst, cond);
} }
} }
} }
@ -394,6 +405,9 @@ namespace spot
e.acc = {}; e.acc = {};
} }
} }
// Now that the iteration is over, commit all new edges.
for (auto& e: new_edges)
aut->new_edge(e.src, e.dst, e.cond, {0});
// In a deterministic and suspendable automaton, all states // In a deterministic and suspendable automaton, all states
// recognize the same language, so we can freely move the // recognize the same language, so we can freely move the
// initial state. We decide to use the source of any // initial state. We decide to use the source of any