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

twagraph: fix purge_dead_states on alternating automata

Browse source 
* tests/core/alternating.test: Run some of the test through
valgrind to exhibit the bug.
* spot/twa/twagraph.cc: Fix it.
This commit is contained in:
Alexandre Duret-Lutz 2017-01-10 10:29:32 +01:00
parent 042c7a0f5b
commit 12ecb3febf
2 changed files with 10 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

9
spot/twa/twagraph.cc
View file

@ -1,6 +1,6 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement de // Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
// l'Epita. // Développement de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -300,7 +300,7 @@ namespace spot
todo.emplace_back(init_number_, 0U, begin, end); todo.emplace_back(init_number_, 0U, begin, end);
} }
do for (;;)
{ {
unsigned& tid = std::get<1>(todo.back()); unsigned& tid = std::get<1>(todo.back());
const unsigned*& begin = std::get<2>(todo.back()); const unsigned*& begin = std::get<2>(todo.back());
@ -308,6 +308,8 @@ namespace spot
if (tid == 0U && begin == end) if (tid == 0U && begin == end)
{ {
todo.pop_back(); todo.pop_back();
if (todo.empty())
break;
unsigned src = std::get<0>(todo.back()); unsigned src = std::get<0>(todo.back());
if ((int)src >= 0) if ((int)src >= 0)
order.emplace_back(src); order.emplace_back(src);
@ -334,7 +336,6 @@ namespace spot
todo.emplace_back(dst, succ, begin, end); todo.emplace_back(dst, succ, begin, end);
} }
} }
while (!todo.empty());
} }
// Process states in topological order // Process states in topological order

10
tests/core/alternating.test
View file

@ -1,7 +1,7 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2016 Laboratoire de Recherche et Développement de # Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement
# 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.
# #
@ -319,9 +319,9 @@ State: 3
--END-- --END--
EOF EOF
autfilt --remove-unreachable-states ex4 > out4 run 0 autfilt --remove-unreachable-states ex4 > out4
diff expect4 out4 diff expect4 out4
autfilt --remove-dead-states ex4 > out4 run 0 autfilt --remove-dead-states ex4 > out4
diff ex2 out4 diff ex2 out4
@ -338,7 +338,7 @@ State: 1
--END-- --END--
EOF EOF
autfilt --remove-dead-states ex5 > out5 run 0 autfilt --remove-dead-states ex5 > out5
cat >expect <<EOF cat >expect <<EOF
HOA: v1 HOA: v1
States: 1 States: 1