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

merge_edge: clarify documentation

Browse source 
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.
This commit is contained in:
Alexandre Duret-Lutz 2021-01-20 22:18:42 +01:00
parent 2072151499
commit 238a9ffc1d
2 changed files with 9 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
spot/graph/graph.hh
View file

@ -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<unsigned>&& newst, unsigned used_states)
{

9
spot/twa/twagraph.hh
View file

@ -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<unsigned>&& newst, unsigned used_states);
/// \brief Print the data structures used to represent the