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 #457.
* THANKS: Add Michaël.
This commit is contained in:
Alexandre Duret-Lutz 2021-02-18 22:15:58 +01:00
parent 4d23b7b770
commit cad3d7706c
3 changed files with 29 additions and 11 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
Matthias Heizmann
Maxime Bouton
Michaël Cadilhac
Michael Tautschnig
Michael Weber
Mikuláš Klokočka

17
spot/graph/graph.hh
View file

@ -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<unsigned>&& newst, unsigned used_states)
{
SPOT_ASSERT(newst.size() >= states_.size());

22
spot/twa/twagraph.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement
// Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
// de l'Epita.
//
// This file is part of Spot, a model checking library.
@ -554,7 +554,7 @@ namespace spot
///
/// In the first 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.
///
/// In the second pass, which is performed only on automata with
/// Fin-less acceptance, edges with the same source, destination,
@ -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<unsigned>&& newst, unsigned used_states);
/// \brief Print the data structures used to represent the