alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

twagraph: improve doc

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2021-02-18 22:15:58 +01:00
parent 57b508c767
commit 0b048e1c05
3 changed files with 28 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

1
THANKS
View file

@ -33,6 +33,7 @@ Kristin Y. Rozier
Martin Dieguez Lodeiro Martin Dieguez Lodeiro
Matthias Heizmann Matthias Heizmann
Maxime Bouton Maxime Bouton
Michaël Cadilhac
Michael Tautschnig Michael Tautschnig
Michael Weber Michael Weber
Mikuláš Klokočka Mikuláš Klokočka

17
spot/graph/graph.hh
View file

@ -1289,10 +1289,19 @@ namespace spot
/// \brief Rename and remove states. /// \brief Rename and remove states.
/// ///
/// \param newst A vector indicating how each state should be renumbered. /// This method is used to remove some states that have been
/// Use -1U to erase a state. All other numbers are expected to /// previously detected to be unreachable in order to "defragment"
/// satisfy newst[i] ≤ i for all i. /// the state vector. When a state is removed, all its outgoing
/// \param used_states the number of states used (after renumbering) /// 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<unsigned>&& newst, unsigned used_states) void defrag_states(std::vector<unsigned>&& newst, unsigned used_states)
{ {
SPOT_ASSERT(newst.size() >= states_.size()); SPOT_ASSERT(newst.size() >= states_.size());

20
spot/twa/twagraph.hh
View file

@ -559,7 +559,7 @@ namespace spot
/// ///
/// In the second pass, edges that share their source, destination, /// In the second pass, edges that share their source, destination,
/// and acceptance marks are merged into a single edge whose condition /// 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 /// If the automaton uses some universal edges, the method
/// merge_univ_dests() is also called. /// merge_univ_dests() is also called.
@ -695,12 +695,20 @@ namespace spot
/// digraph::defrag_state() that additionally deals with universal /// digraph::defrag_state() that additionally deals with universal
/// branching. /// 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 /// \param newst A vector indicating how each state should be
/// renumbered. Use -1U to erase a state. Ignoring the /// renumbered. Use -1U to mark an unreachable state for removal.
/// occurrences of -1U, the renumbering is expected to /// Ignoring the occurrences of -1U, the renumbering is expected
/// satisfy newst[i] ≤ i for all i. /// to satisfy newst[i] ≤ i for all i.
/// \param used_states the number of states used ///
/// (after renumbering) /// \param used_states the number of states used after
/// renumbering.
void defrag_states(std::vector<unsigned>&& newst, unsigned used_states); void defrag_states(std::vector<unsigned>&& newst, unsigned used_states);
/// \brief Print the data structures used to represent the /// \brief Print the data structures used to represent the