From cbfdcca1f91cde660f6a62f8b22c15265cb40a05 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 28 May 2009 11:45:16 +0200 Subject: [PATCH] Fix assertion in scc.cc --- ChangeLog | 7 +++++++ src/tgbaalgos/scc.cc | 4 ++-- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/ChangeLog b/ChangeLog index 1a919eb7c..cb105824d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2009-05-28 Alexandre Duret-Lutz + + * src/tgbaalgos/scc.cc (scc_map::relabel_component): Make sure + that the old label of each state is strictly positive. The + previous assertion (inherited from gtec) of "!= -1" is wrong, + because all negative values are now used to number SCCs. + 2009-05-26 Alexandre Duret-Lutz * src/tgba/tgba.hh (format_state): s/automata who/automata that/. diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 5bd6c19f1..21d4d27a3 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2008 Laboratoire de Recherche et Developpement de +// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement de // l'Epita. // // This file is part of Spot, a model checking library. @@ -87,7 +87,7 @@ namespace spot hash_type::iterator spi = h_.find(*i); assert(spi != h_.end()); assert(spi->first == *i); - assert(spi->second != -1); + assert(spi->second > 0); spi->second = n; } scc_map_.insert(std::make_pair(n, root_.front()));