From 238a9ffc1d580fdda6600599fefcfe6ad1c5d091 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 20 Jan 2021 22:18:42 +0100 Subject: [PATCH] merge_edge: clarify documentation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Reported by Florian Renkin. * spot/graph/graph.hh, spot/twa/twagraph.hh (merge_edge): Document that it is expected that state i can only be renamed as j if j≤i. --- spot/graph/graph.hh | 5 +++-- spot/twa/twagraph.hh | 9 ++++++--- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index 87bb063fd..bcd7045f0 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2018, 2020 Laboratoire de Recherche et +// Copyright (C) 2014-2018, 2020, 2021 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -1290,7 +1290,8 @@ namespace spot /// \brief Rename and remove states. /// /// \param newst A vector indicating how each state should be renumbered. - /// Use -1U to erase a state. + /// Use -1U to erase a state. All other numbers are expected to + /// satisfy newst[i] ≤ i for all i. /// \param used_states the number of states used (after renumbering) void defrag_states(std::vector&& newst, unsigned used_states) { diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 72cf886e8..2f49d7b16 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -695,9 +695,12 @@ namespace spot /// digraph::defrag_state() that additionally deals with universal /// branching. /// - /// \param newst A vector indicating how each state should be renumbered. - /// Use -1U to erase a state. - /// \param used_states the number of states used (after renumbering) + /// \param newst A vector indicating how each state should be + /// renumbered. Use -1U to erase a state. Ignoring the + /// occurrences of -1U, the renumbering is expected to + /// satisfy newst[i] ≤ i for all i. + /// \param used_states the number of states used + /// (after renumbering) void defrag_states(std::vector&& newst, unsigned used_states); /// \brief Print the data structures used to represent the