From 0b048e1c05113936409c26b73e8eb001f0af5c6f Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 18 Feb 2021 22:15:58 +0100 Subject: [PATCH] twagraph: improve doc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Based on report by Michaël Cadilhac. * spot/graph/graph.hh, spot/twa/twagraph.hh (defrag_state): Clarify that only unreachable states are meant to be removed. * spot/twa/twagraph.hh (merge_edges): Typo in comment. Fixes #454. * THANKS: Add Michaël. --- THANKS | 1 + spot/graph/graph.hh | 17 +++++++++++++---- spot/twa/twagraph.hh | 20 ++++++++++++++------ 3 files changed, 28 insertions(+), 10 deletions(-) diff --git a/THANKS b/THANKS index 7d3596140..cd1a8be60 100644 --- a/THANKS +++ b/THANKS @@ -33,6 +33,7 @@ Kristin Y. Rozier Martin Dieguez Lodeiro Matthias Heizmann Maxime Bouton +Michaël Cadilhac Michael Tautschnig Michael Weber Mikuláš Klokočka diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index bcd7045f0..507bc849e 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -1289,10 +1289,19 @@ namespace spot /// \brief Rename and remove states. /// - /// \param newst A vector indicating how each state should be renumbered. - /// 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) + /// This method is used to remove some states that have been + /// previously detected to be unreachable in order to "defragment" + /// the state vector. When a state is removed, all its outgoing + /// transition are removed as well. Removing reachable states + /// should NOT be attempted, because the incoming edges will be + /// dangling. + /// + /// \param newst A vector indicating how each state should be + /// renumbered. Use -1U to erase an unreachable 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) { SPOT_ASSERT(newst.size() >= states_.size()); diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 2f49d7b16..b8e248916 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -559,7 +559,7 @@ namespace spot /// /// In the second pass, edges that share their source, destination, /// and acceptance marks are merged into a single edge whose condition - /// is the conjunction of the conditions of the original edges. + /// is the disjunction of the conditions of the original edges. /// /// If the automaton uses some universal edges, the method /// merge_univ_dests() is also called. @@ -695,12 +695,20 @@ namespace spot /// digraph::defrag_state() that additionally deals with universal /// branching. /// + /// This method is used to remove some states that have been + /// previously detected to be unreachable in order to "defragment" + /// the state vector. When a state is removed, all its outgoing + /// transition are removed as well. Removing reachable states + /// should NOT be attempted, because the incoming edges will be + /// dangling. + /// /// \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) + /// renumbered. Use -1U to mark an unreachable state for removal. + /// 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