Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/utilities/reachable_nodes.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_UTILITIES_REACHABLE_NODES_H
      13             : #define MCRL2_UTILITIES_REACHABLE_NODES_H
      14             : 
      15             : #include <boost/graph/adjacency_list.hpp> // to make the header compile standalone
      16             : #include <boost/graph/depth_first_search.hpp>
      17             : #include <boost/tuple/tuple.hpp>
      18             : 
      19             : #include <cstddef>
      20             : #include <iterator>
      21             : #include <vector>
      22             : 
      23             : namespace mcrl2 {
      24             : 
      25             : namespace utilities {
      26             : 
      27             : /// \cond INTERNAL_DOCS
      28             : namespace detail
      29             : {
      30             : 
      31             : template <typename Graph>
      32             : struct reachable_nodes_recorder: public boost::default_dfs_visitor
      33             : {
      34             :   typedef typename Graph::vertex_descriptor vertex_descriptor;
      35             :   std::vector<std::size_t>& m_result;
      36             : 
      37           9 :   reachable_nodes_recorder(std::vector<std::size_t>& result)
      38           9 :     : m_result(result)
      39           9 :   {}
      40             : 
      41             :   /// \brief Is called whenever a new vertex is discovered
      42             :   /// \param u A vertex
      43             :   /// \param g A graph
      44          27 :   void discover_vertex(vertex_descriptor u, const Graph& g)
      45             :   {
      46          27 :     m_result.push_back(boost::get(boost::vertex_index, g)[u]);
      47          27 :   }
      48             : };
      49             : } // namespace detail
      50             : /// \endcond
      51             : 
      52             : /// \brief Compute reachable nodes in a graph.
      53             : /// \param g A graph.
      54             : /// \param first Iterator to the first node.
      55             : /// \param last Iterator to the last node.
      56             : /// \return The indices of the nodes that are reachable from the nodes
      57             : /// given by the range of vertex descriptors [first, last].
      58             : template <typename Graph, typename Iter>
      59           9 : std::vector<std::size_t> reachable_nodes(const Graph& g, Iter first, Iter last)
      60             : {
      61             :   typedef boost::color_traits<boost::default_color_type> Color;
      62             : 
      63           9 :   std::vector<std::size_t> result;
      64           9 :   detail::reachable_nodes_recorder<Graph> recorder(result);
      65           9 :   std::vector<boost::default_color_type> colormap(boost::num_vertices(g), Color::white());
      66             : 
      67          30 :   for (Iter i = first; i != last; ++i)
      68             :   {
      69          21 :     boost::default_color_type c = Color::white();
      70          42 :     boost::depth_first_visit(g,
      71          21 :                              *i,
      72             :                              recorder,
      73          21 :                              boost::make_iterator_property_map(colormap.begin(), boost::get(boost::vertex_index, g), c)
      74             :                             );
      75             :   }
      76             : 
      77          18 :   return result;
      78           9 : }
      79             : 
      80             : } // namespace utilities
      81             : 
      82             : } // namespace mcrl2
      83             : 
      84             : #endif // MCRL2_UTILITIES_REACHABLE_NODES_H