LCOV - code coverage report
Current view: top level - process/include/mcrl2/process/detail - pcrl_equation_cache.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 36 39 92.3 %
Date: 2020-09-22 00:46:14 Functions: 6 6 100.0 %
Legend: Lines: hit not hit

          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/detail/pcrl_equation_cache.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_DETAIL_PCRL_EQUATION_CACHE_H
      13             : #define MCRL2_PROCESS_DETAIL_PCRL_EQUATION_CACHE_H
      14             : 
      15             : #include "mcrl2/process/alphabet_efficient.h"
      16             : #include "mcrl2/process/process_variable_strongly_connected_components.h" // find_process_identifiers
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace process {
      21             : 
      22             : namespace detail {
      23             : 
      24             : // Returns a mapping P -> alphabet(P) for all pCRL equations P.
      25             : // TODO: This mapping can probably be computed more efficiently using the SCC decomposition of the equations.
      26             : inline
      27           1 : std::map<process_identifier, multi_action_name_set> compute_pcrl_equation_cache(const std::vector<process_equation>& equations)
      28             : {
      29           1 :   std::map<process_identifier, multi_action_name_set> result;
      30           1 :   for (const process_equation& eqn: equations)
      31             :   {
      32           0 :     if (is_pcrl(eqn.expression()))
      33             :     {
      34           0 :       result[eqn.identifier()] = alphabet_efficient(eqn.expression(), equations);
      35             :     }
      36             :   }
      37           1 :   return result;
      38             : }
      39             : 
      40             : // for traversal of reachable process equations starting in the initial state
      41           2 : struct process_traversal_algorithm
      42             : {
      43             :   const std::vector<process_equation>& equations;
      44             :   const process_expression& init;
      45             : 
      46             :   std::set<process_identifier> todo;
      47             :   std::set<process_identifier> done;
      48             : 
      49           2 :   process_traversal_algorithm(const std::vector<process_equation>& equations_, const process_expression& init_)
      50           2 :     : equations(equations_), init(init_)
      51             :   {
      52           2 :     todo = find_process_identifiers(init);
      53           2 :   }
      54             : 
      55             :   // returns true if there is another reachable process equation
      56           6 :   bool has_next()
      57             :   {
      58           6 :     return !todo.empty();
      59             :   }
      60             : 
      61           2 :   const process_equation& next()
      62             :   {
      63           2 :     assert(has_next());
      64             : 
      65             :     // pick an element from todo
      66           4 :     process_identifier id = *todo.begin();
      67           2 :     todo.erase(todo.begin());
      68           2 :     done.insert(id);
      69             : 
      70           2 :     const process_equation& eqn = find_equation(equations, id);
      71             : 
      72             :     // search for new identifiers in the rhs of the equation
      73           4 :     for (const process_identifier& id: find_process_identifiers(eqn.expression()))
      74             :     {
      75           2 :       if (done.find(id) == done.end())
      76             :       {
      77           0 :         todo.insert(id);
      78             :       }
      79             :     }
      80             : 
      81           4 :     return eqn;
      82             :   }
      83             : };
      84             : 
      85             : // Returns a mapping P -> alphabet(P) for all pCRL equations P that are reachable from init.
      86             : inline
      87           2 : std::map<process_identifier, multi_action_name_set> compute_pcrl_equation_cache(const std::vector<process_equation>& equations, const process_expression& init)
      88             : {
      89             :   // use the scc decomposition to ensure that the alphabet for equations in the same scc is computed only once
      90           4 :   std::vector<std::set<process_identifier> > sccs = process_variable_strongly_connected_components(equations, init);
      91           4 :   std::map<process_identifier, std::size_t> scc_index;
      92           4 :   for (std::size_t i = 0; i < sccs.size(); i++)
      93             :   {
      94           4 :     for (const process_identifier& id: sccs[i])
      95             :     {
      96           2 :       scc_index[id] = i;
      97             :     }
      98             :   }
      99             : 
     100           2 :   std::map<process_identifier, multi_action_name_set> result;
     101           4 :   process_traversal_algorithm algorithm(equations, init);
     102           6 :   while (algorithm.has_next())
     103             :   {
     104           2 :     const process_equation& eqn = algorithm.next();
     105           2 :     if (is_pcrl(eqn.expression()) && result.find(eqn.identifier()) == result.end())
     106             :     {
     107           4 :       multi_action_name_set A = alphabet_efficient(eqn.expression(), equations);
     108           2 :       const std::set<process_identifier>& scc = sccs[scc_index[eqn.identifier()]];
     109           4 :       for (const process_identifier& id: scc)
     110             :       {
     111           2 :         result[id] = A;
     112             :       }
     113             :     }
     114             :   }
     115           4 :   return result;
     116             : }
     117             : 
     118             : } // namespace detail
     119             : 
     120             : } // namespace process
     121             : 
     122             : } // namespace mcrl2
     123             : 
     124             : #endif // MCRL2_PROCESS_DETAIL_PCRL_EQUATION_CACHE_H

Generated by: LCOV version 1.13