diff --git a/ChangeLog b/ChangeLog index 783ae5d48..fb28ed409 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,10 @@ +2011-01-04 Alexandre Duret-Lutz + + Add trivial() and one_state_of() functions to scc_map. + + * src/tgbaalgos/scc.hh, src/tgbaalgos/scc.cc (scc_map::trivial, + scc_map::one_state_of): Two new helper functions. + 2011-01-04 Alexandre Duret-Lutz * src/tgba/tgbaunion.hh: Remove one useless include. diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 75bac5261..7279bb7a2 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -1,5 +1,5 @@ -// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement de -// l'Epita. +// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et +// Developpement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -74,6 +74,13 @@ namespace spot return scc_map_[n].succ; } + bool + scc_map::trivial(unsigned n) const + { + assert(scc_map_.size() > n); + return scc_map_[n].trivial; + } + bool scc_map::accepting(unsigned n) const { @@ -347,6 +354,12 @@ namespace spot return scc_map_[n].states; } + const state* scc_map::one_state_of(unsigned n) const + { + assert(scc_map_.size() > n); + return scc_map_[n].states.front(); + } + unsigned scc_map::scc_count() const { return scc_map_.size(); diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 57f26d3bf..e993f743b 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -105,6 +105,13 @@ namespace spot /// \pre This should only be called once build_map() has run. const succ_type& succ(unsigned n) const; + /// \brief Return whether an SCC is trivial. + /// + /// Trivial SCCs have one state and no self-loop. + /// + /// \pre This should only be called once build_map() has run. + bool trivial(unsigned n) const; + /// \brief Return whether an SCC is accepting. /// /// \pre This should only be called once build_map() has run. @@ -150,6 +157,14 @@ namespace spot /// \pre This should only be called once build_map() has run. const std::list& states_of(unsigned n) const; + /// \brief Return one state of an SCC. + /// + /// The state in the returned list is still owned by the scc_map + /// instance. It should NOT be deleted by the client code. + /// + /// \pre This should only be called once build_map() has run. + const state* one_state_of(unsigned n) const; + /// \brief Return the number of the SCC a state belongs too. /// /// \pre This should only be called once build_map() has run.