diff --git a/NEWS b/NEWS index 17d9ceba5..bb33b9dc5 100644 --- a/NEWS +++ b/NEWS @@ -111,6 +111,8 @@ New in spot 1.99.6a (not yet released) Bug fixes: + * twa_graph would incorrectly replace named-states during + purge_dead_states and purge_unreachable_states. * twa::ap() would contain duplicates when an atomic proposition was registered several times. * product() would incorrectly mark the product of two diff --git a/spot/twa/twagraph.cc b/spot/twa/twagraph.cc index cf080589e..e4ee8d2b3 100644 --- a/spot/twa/twagraph.cc +++ b/spot/twa/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement de // l'Epita. // // This file is part of Spot, a model checking library. @@ -190,7 +190,7 @@ namespace spot if (current == todo.size()) return; // No unreachable state. init_number_ = todo[init_number_]; - g_.defrag_states(std::move(todo), current); + defrag_states(std::move(todo), current); } void twa_graph::purge_dead_states() @@ -266,6 +266,25 @@ namespace spot if (current == num_states) return; // No useless state. init_number_ = useful[init_number_]; - g_.defrag_states(std::move(useful), current); + defrag_states(std::move(useful), current); + } + + void twa_graph::defrag_states(std::vector&& newst, + unsigned used_states) + { + auto* names = get_named_prop>("state-names"); + if (names) + { + unsigned size = names->size(); + for (unsigned s = 0; s < size; ++s) + { + unsigned dst = newst[s]; + if (dst == s || dst == -1U) + continue; + (*names)[dst] = std::move((*names)[s]); + } + names->resize(used_states); + } + g_.defrag_states(std::move(newst), used_states); } } diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 0342e6f81..a4591ccf4 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -479,6 +479,8 @@ namespace spot return std::equal(trans1.begin() + 1, trans1.end(), trans2.begin() + 1); } + + void defrag_states(std::vector&& newst, unsigned used_states); }; inline twa_graph_ptr make_twa_graph(const bdd_dict_ptr& dict) diff --git a/tests/core/tgbagraph.test b/tests/core/tgbagraph.test index cb8fe8230..6976eda89 100755 --- a/tests/core/tgbagraph.test +++ b/tests/core/tgbagraph.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +# Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement # de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -221,6 +221,20 @@ digraph G { 101 [label="101"] 102 [label="102"] } +digraph G { + rankdir=LR + I [label="", style=invis, width=0] + I -> 2 + 0 [label="s1"] + 1 [label="s2"] + 2 [label="s3"] +} +digraph G { + rankdir=LR + I [label="", style=invis, width=0] + I -> 0 + 0 [label="s3"] +} EOF diff stdout expected diff --git a/tests/core/twagraph.cc b/tests/core/twagraph.cc index e7a54b99e..ca5a7e3ec 100644 --- a/tests/core/twagraph.cc +++ b/tests/core/twagraph.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita. // // This file is part of Spot, a model checking library. @@ -84,7 +84,29 @@ static void f1() spot::print_dot(std::cout, tg); } +// Test purge with named states. +static void f2() +{ + auto d = spot::make_bdd_dict(); + auto tg = make_twa_graph(d); + + auto s1 = tg->new_state(); + auto s2 = tg->new_state(); + auto s3 = tg->new_state(); + (void) s1; + (void) s2; + std::vector* names; + names = new std::vector({"s1", "s2", "s3"}); + + tg->set_named_prop>("state-names", names); + tg->set_init_state(s3); + spot::print_dot(std::cout, tg); + tg->purge_unreachable_states(); + spot::print_dot(std::cout, tg); +} + int main() { f1(); + f2(); }