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

improve doc for purge_unreachable_states and purge_dead_states

Browse source 
* spot/twa/twagraph.hh: Here.
This commit is contained in:
Alexandre Duret-Lutz 2016-11-11 15:38:25 +01:00
parent ee85cf7759
commit dce83a649b
1 changed files with 20 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

23
spot/twa/twagraph.hh
View file

@ -439,13 +439,30 @@ namespace spot
/// extremities and acceptance.
void merge_edges();
/// Remove all states without successors.
/// \brief Remove all dead states
///
/// Dead states are all the states that cannot be part of
/// an infinite run of the automaton. This includes
/// states without successors, unreachable states, and states
/// that only have dead successors.
///
/// \see purge_unreachable_states
void purge_dead_states();
/// Remove all unreachable states.
/// \brief Remove all unreachable states.
///
/// A state is unreachable if it cannot be reached from the initial state.
///
/// Use this function if you have declared more states than you
/// actually need in the automaton.
///
/// purge_dead_states() will remove more states than
/// purge_unreachable_states().
///
/// \see purge_dead_states
void purge_unreachable_states();
/// \brief Remove unused atomic proposition
/// \brief Remove unused atomic propositions
///
/// Remove, from the list of atomic propositions registered by the
/// automaton, those that are not actually used by its labels.