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/process/process_variable_strongly_connected_components.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_PROCESS_VARIABLE_STRONGLY_CONNECTED_COMPONENTS_H
      13             : #define MCRL2_PROCESS_PROCESS_VARIABLE_STRONGLY_CONNECTED_COMPONENTS_H
      14             : 
      15             : #include "mcrl2/process/find.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : namespace detail {
      22             : 
      23             : // Implementation of Tarjan's strongly connected components algorithm, based on
      24             : // http://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm
      25             : class tarjan_scc_algorithm
      26             : {
      27             :   public:
      28             :     typedef std::pair<std::size_t, std::size_t> edge;
      29             :     typedef std::vector<std::size_t> component;
      30             : 
      31             :   protected:
      32           8 :     static inline std::size_t undefined()
      33             :     {
      34           8 :       return std::size_t(-1);
      35             :     }
      36             : 
      37             :     struct vertex
      38             :     {
      39             :       std::size_t value;
      40             :       std::size_t index;
      41             :       std::size_t lowlink;
      42             :       bool onstack;
      43             : 
      44           4 :       bool operator==(const vertex& other) const
      45             :       {
      46           4 :         return value == other.value;
      47             :       }
      48             : 
      49           2 :       bool operator!=(const vertex& other) const
      50             :       {
      51           2 :         return !(*this == other);
      52             :       }
      53             : 
      54           2 :       vertex(std::size_t value_, std::size_t index_ = undefined(), std::size_t lowlink_ = undefined())
      55           2 :         : value(value_), index(index_), lowlink(lowlink_), onstack(false)
      56           2 :       {}
      57             :     };
      58             : 
      59           2 :     std::size_t strongconnect(std::size_t v_index, component& S, std::size_t index)
      60             :     {
      61           2 :       vertex& v = V[v_index];
      62           2 :       v.index = index;
      63           2 :       v.lowlink = index;
      64           2 :       index++;
      65           2 :       S.push_back(v_index);
      66           2 :       v.onstack = true;
      67             : 
      68           4 :       for (const edge& e: E)
      69             :       {
      70           2 :         auto u_index = e.first;
      71           2 :         auto w_index = e.second;
      72           2 :         const vertex& u = V[u_index];
      73           2 :         const vertex& w = V[w_index];
      74           2 :         if (u != v)
      75             :         {
      76           0 :           continue;
      77             :         }
      78           2 :         if (w.index == undefined())
      79             :         {
      80           0 :           index = strongconnect(w_index, S, index);
      81           0 :           v.lowlink = (std::min)(v.lowlink, w.lowlink);
      82             :         }
      83           2 :         else if (w.onstack)
      84             :         {
      85           2 :           v.lowlink = (std::min)(v.lowlink, w.index);
      86             :         }
      87             :       }
      88             : 
      89           2 :       if (v.lowlink == v.index)
      90             :       {
      91           2 :         component S1;
      92             :         while (true)
      93             :         {
      94           2 :           std::size_t w_index = S.back();
      95           2 :           S.pop_back();
      96           2 :           vertex& w = V[w_index];
      97           2 :           w.onstack = false;
      98           2 :           S1.push_back(w_index);
      99           2 :           if (w == v)
     100             :           {
     101           2 :             result.push_back(S1);
     102           2 :             break;
     103             :           }
     104           0 :         }
     105           2 :       }
     106           2 :       return index;
     107             :     }
     108             : 
     109             :     std::vector<vertex> V;
     110             :     std::vector<edge> E;
     111             :     std::size_t N;
     112             :     std::vector<component> result;
     113             : 
     114             :   public:
     115           2 :     tarjan_scc_algorithm()
     116           2 :     {}
     117             : 
     118             :     // The graph contains vertices [0, ... N).
     119             :     // The edges are pairs of vertices.
     120           2 :     void run(const std::vector<edge>& E_, std::size_t N_)
     121             :     {
     122           2 :       E = E_;
     123           2 :       N = N_;
     124           2 :       V.clear();
     125           2 :       result.clear();
     126             : 
     127           4 :       for (std::size_t i = 0; i < N; i++)
     128             :       {
     129           2 :         V.push_back(vertex(i));
     130             :       }
     131             : 
     132           2 :       component S;
     133           4 :       for (vertex& v: V)
     134             :       {
     135           2 :         if (v.index == undefined())
     136             :         {
     137           2 :           v.index = strongconnect(v.value, S, 0);
     138             :         }
     139             :       }
     140           2 :     }
     141             : 
     142           2 :     const std::vector<component>& components() const
     143             :     {
     144           2 :       return result;
     145             :     }
     146             : };
     147             : 
     148             : struct find_process_identifiers_traverser: public process_expression_traverser<find_process_identifiers_traverser>
     149             : {
     150             :   typedef process_expression_traverser<find_process_identifiers_traverser> super;
     151             :   using super::enter;
     152             :   using super::leave;
     153             :   using super::apply;
     154             : 
     155             :   std::set<process_identifier> result;
     156             : 
     157           8 :   void apply(const process::process_instance& x)
     158             :   {
     159           8 :     result.insert(x.identifier());
     160           8 :   }
     161             : 
     162           0 :   void apply(const process::process_instance_assignment& x)
     163             :   {
     164           0 :     result.insert(x.identifier());
     165           0 :   }
     166             : };
     167             : 
     168             : inline
     169           8 : std::set<process_identifier> find_process_identifiers(const process_expression& x)
     170             : {
     171           8 :   find_process_identifiers_traverser f;
     172           8 :   f.apply(x);
     173          16 :   return f.result;
     174           8 : }
     175             : 
     176             : struct process_variable_scc_algorithm
     177             : {
     178             :   std::map<process_identifier, std::size_t> index;
     179             :   std::map<process_identifier, std::set<process_identifier> > dependencies;
     180             : 
     181           2 :   void add_edge(const process_identifier& source, const process_identifier& target)
     182             :   {
     183           2 :     dependencies[source].insert(target);
     184           2 :   }
     185             : 
     186           2 :   void compute_index(const std::vector<process_equation>& equations)
     187             :   {
     188           2 :     index.clear();
     189           2 :     std::size_t i = 0;
     190           4 :     for (const process_equation& eqn: equations)
     191             :     {
     192           2 :       index[eqn.identifier()] = i++;
     193             :     }
     194           2 :   }
     195             : 
     196             :   void compute_dependencies(const std::vector<process_equation>& equations)
     197             :   {
     198             :     dependencies.clear();
     199             :     for (const process_equation& eqn: equations)
     200             :     {
     201             :       const process_identifier& source = eqn.identifier();
     202             :       for (const process_identifier& target: detail::find_process_identifiers(eqn.expression()))
     203             :       {
     204             :         add_edge(source, target);
     205             :       }
     206             :     }
     207             :   }
     208             : 
     209             :   // only add dependencies for equations reachable from init
     210           2 :   void compute_dependencies(const std::vector<process_equation>& equations, const process_expression& init)
     211             :   {
     212           2 :     dependencies.clear();
     213           2 :     std::set<process_identifier> todo;
     214           2 :     std::set<process_identifier> done;
     215             : 
     216           2 :     todo = find_process_identifiers(init);
     217           4 :     while (!todo.empty())
     218             :     {
     219             :       // pick an element from todo
     220           2 :       process_identifier source = *todo.begin();
     221           2 :       todo.erase(todo.begin());
     222           2 :       done.insert(source);
     223             : 
     224           2 :       const process_equation& eqn = find_equation(equations, source);
     225             : 
     226             :       // search for new identifiers in the rhs of the equation
     227           4 :       for (const process_identifier& target: find_process_identifiers(eqn.expression()))
     228             :       {
     229           2 :         add_edge(source, target);
     230           2 :         if (done.find(target) == done.end())
     231             :         {
     232           0 :           todo.insert(target);
     233             :         }
     234           2 :       }
     235           2 :     }
     236           2 :   }
     237             : 
     238           2 :   std::vector<std::set<process_identifier> > run_impl(const std::vector<process_equation>& equations)
     239             :   {
     240             :     // convert dependency graph to edge list
     241           2 :     std::vector<std::pair<std::size_t, std::size_t> > E;
     242           4 :     for (const auto& p: dependencies)
     243             :     {
     244           2 :       std::size_t source = index[p.first];
     245           4 :       for (const process_identifier& id: p.second)
     246             :       {
     247           2 :         std::size_t target = index[id];
     248           2 :         E.push_back({ source, target });
     249             :       }
     250             :     }
     251             : 
     252             :     // compute sccs
     253           2 :     tarjan_scc_algorithm algorithm;
     254           2 :     algorithm.run(E, index.size());
     255             : 
     256             :     // make result
     257           2 :     std::vector<std::set<process_identifier> > result;
     258           4 :     for (const auto& component: algorithm.components())
     259             :     {
     260           2 :       std::set<process_identifier> S;
     261           4 :       for (std::size_t i: component)
     262             :       {
     263           2 :         S.insert(equations[i].identifier());
     264             :       }
     265           2 :       result.push_back(S);
     266           2 :     }
     267           4 :     return result;
     268           2 :   }
     269             : 
     270             :   // make scc for all equations
     271             :   std::vector<std::set<process_identifier> > run(const std::vector<process_equation>& equations)
     272             :   {
     273             :     compute_index(equations);
     274             :     compute_dependencies(equations);
     275             :     return run_impl(equations);
     276             :   }
     277             : 
     278             :   // make scc for the equations reachable from init
     279           2 :   std::vector<std::set<process_identifier> > run(const std::vector<process_equation>& equations, const process_expression& init)
     280             :   {
     281           2 :     compute_index(equations);
     282           2 :     compute_dependencies(equations, init);
     283           2 :     return run_impl(equations);
     284             :   }
     285             : };
     286             : 
     287             : } // namespace detail
     288             : 
     289             : /// \brief Computes an SCC graph of the equations
     290             : inline
     291             : std::vector<std::set<process_identifier> > process_variable_strongly_connected_components(const std::vector<process_equation>& equations)
     292             : {
     293             :   detail::process_variable_scc_algorithm algorithm;
     294             :   return algorithm.run(equations);
     295             : }
     296             : 
     297             : /// \brief Compute an SCC graph of the equations reachable from init
     298             : inline
     299           2 : std::vector<std::set<process_identifier> > process_variable_strongly_connected_components(const std::vector<process_equation>& equations, const process_expression& init)
     300             : {
     301           2 :   detail::process_variable_scc_algorithm algorithm;
     302           4 :   return algorithm.run(equations, init);
     303           2 : }
     304             : 
     305             : } // namespace process
     306             : 
     307             : } // namespace mcrl2
     308             : 
     309             : #endif // MCRL2_PROCESS_PROCESS_VARIABLE_STRONGLY_CONNECTED_COMPONENTS_H