diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index 9375622bf..04ea0cb81 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement de -// l'Epita. +// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -300,7 +300,7 @@ namespace spot todo.emplace_back(init_number_, 0U, begin, end); } - do + for (;;) { unsigned& tid = std::get<1>(todo.back()); const unsigned*& begin = std::get<2>(todo.back()); @@ -308,6 +308,8 @@ namespace spot if (tid == 0U && begin == end) { todo.pop_back(); + if (todo.empty()) + break; unsigned src = std::get<0>(todo.back()); if ((int)src >= 0) order.emplace_back(src); @@ -334,7 +336,6 @@ namespace spot todo.emplace_back(dst, succ, begin, end); } } - while (!todo.empty()); } // Process states in topological order diff --git a/tests/core/alternating.test b/tests/core/alternating.test index 61a827a12..7805765f7 100644 --- a/tests/core/alternating.test +++ b/tests/core/alternating.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2016 Laboratoire de Recherche et Développement de -# l'Epita (LRDE). +# Copyright (C) 2016, 2017 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -319,9 +319,9 @@ State: 3 --END-- EOF -autfilt --remove-unreachable-states ex4 > out4 +run 0 autfilt --remove-unreachable-states ex4 > out4 diff expect4 out4 -autfilt --remove-dead-states ex4 > out4 +run 0 autfilt --remove-dead-states ex4 > out4 diff ex2 out4 @@ -338,7 +338,7 @@ State: 1 --END-- EOF -autfilt --remove-dead-states ex5 > out5 +run 0 autfilt --remove-dead-states ex5 > out5 cat >expect <