diff --git a/src/graph/ngraph.hh b/src/graph/ngraph.hh index 102d6b582..3027b77c1 100644 --- a/src/graph/ngraph.hh +++ b/src/graph/ngraph.hh @@ -77,6 +77,13 @@ namespace spot return p.first->second; } + /// \brief Give an alternate name to a state. + /// \return true iff the newname was already used. + bool alias_state(state s, name newname) + { + return !name_to_state.insert(std::make_pair(newname, s)).second; + } + state get_state(name n) const { return name_to_state.at(n); diff --git a/src/graphtest/ngraph.cc b/src/graphtest/ngraph.cc index 3ab980c4f..b11ee855d 100644 --- a/src/graphtest/ngraph.cc +++ b/src/graphtest/ngraph.cc @@ -389,10 +389,12 @@ bool f9() spot::named_graph gg(g); auto s1 = gg.new_state("s1"); gg.new_state("s2"); - gg.new_state("s3"); + auto s3 = gg.new_state("s3"); + gg.alias_state(s3, "s3b"); + gg.new_transition("s1", "s2", 1, 3); gg.new_transition("s1", "s3", 2, 5); - gg.new_transition("s2", "s3", 3, 7); + gg.new_transition("s2", "s3b", 3, 7); gg.new_transition("s3", "s2", 4, 9); dot(std::cout, gg);