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 0 : } 39 : 40 : // for traversal of reachable process equations starting in the initial state 41 : 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 2 : 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 2 : } 80 : 81 2 : return eqn; 82 2 : } 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 2 : std::vector<std::set<process_identifier> > sccs = process_variable_strongly_connected_components(equations, init); 91 2 : 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 2 : process_traversal_algorithm algorithm(equations, init); 102 4 : 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 2 : 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 2 : } 114 : } 115 4 : return result; 116 2 : } 117 : 118 : } // namespace detail 119 : 120 : } // namespace process 121 : 122 : } // namespace mcrl2 123 : 124 : #endif // MCRL2_PROCESS_DETAIL_PCRL_EQUATION_CACHE_H