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/process_context.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H 13 : #define MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H 14 : 15 : #include "mcrl2/data/detail/data_utility.h" 16 : #include "mcrl2/process/detail/action_context.h" 17 : #include "mcrl2/process/process_expression.h" 18 : 19 : namespace mcrl2 { 20 : 21 : namespace process { 22 : 23 : namespace detail { 24 : 25 : class process_context 26 : { 27 : private: 28 : std::multimap<core::identifier_string, process_identifier> m_process_identifiers; 29 : 30 : // returns true if all left hand sides of assignments appear as the name of a variable in parameters 31 441 : bool is_matching_assignment(const data::untyped_identifier_assignment_list& assignments, const data::variable_list& parameters) const 32 : { 33 1404 : for (const data::untyped_identifier_assignment& a: assignments) 34 : { 35 5217 : if (std::find_if(parameters.begin(), parameters.end(), [&](const data::variable& v) { return a.lhs() == v.name(); }) == parameters.end()) 36 : { 37 0 : return false; 38 : } 39 : } 40 441 : return true; 41 : } 42 : 43 : // returns an assignment that does not match with the list of parameters 44 0 : data::untyped_identifier_assignment find_violating_assignment(const data::untyped_identifier_assignment_list& assignments, const data::variable_list& parameters) const 45 : { 46 : using utilities::detail::contains; 47 0 : std::set<core::identifier_string> parameter_names; 48 0 : for (const data::variable& param: parameters) 49 : { 50 0 : parameter_names.insert(param.name()); 51 : } 52 0 : auto i = std::find_if(assignments.begin(), assignments.end(), [&](const data::untyped_identifier_assignment& a) { return !contains(parameter_names, a.lhs()); }); 53 0 : assert(i != assignments.end()); 54 0 : return *i; 55 0 : } 56 : 57 : public: 58 2562 : bool is_declared(const core::identifier_string& name) const 59 : { 60 2562 : return m_process_identifiers.find(name) != m_process_identifiers.end(); 61 : } 62 : 63 : template <typename ProcessIdentifierContainer> 64 1148 : void add_process_identifiers(const ProcessIdentifierContainer& ids, const action_context& action_ctx, const data::sort_type_checker& sort_typechecker) 65 : { 66 2304 : for (const process_identifier& id: ids) 67 : { 68 1146 : const core::identifier_string& name = id.name(); 69 : 70 1146 : if (action_ctx.is_declared(name)) 71 : { 72 0 : throw mcrl2::runtime_error("declaration of both process and action " + core::pp(name)); 73 : } 74 : 75 : // Insert id in m_process_identifiers; N.B. Before that check if it already exists 76 1146 : auto range = m_process_identifiers.equal_range(id.name()); 77 1146 : if (range.first != m_process_identifiers.end()) 78 : { 79 81 : for (auto i = range.first; i != range.second; ++i) 80 : { 81 12 : if (i->second == id) 82 : { 83 0 : throw mcrl2::runtime_error("double declaration of process " + process::pp(id)); 84 : } 85 : } 86 : } 87 1146 : m_process_identifiers.insert(range.first, std::make_pair(id.name(), id)); 88 : 89 3257 : for (const data::variable& v: id.variables()) 90 : { 91 965 : sort_typechecker(v.sort()); 92 : } 93 : 94 : //check that all formal parameters of the process are unique. 95 1146 : if (!data::detail::unique_names(id.variables())) 96 : { 97 0 : throw mcrl2::runtime_error("the formal variables in process " + process::pp(id) + " are not unique"); 98 : } 99 : } 100 1148 : } 101 : 102 : // returns the process identifier that corresponds to the untyped process assignment x 103 441 : process_identifier match_untyped_process_instance_assignment(const untyped_process_assignment& x) const 104 : { 105 441 : auto range = m_process_identifiers.equal_range(x.name()); 106 441 : if (range.first == m_process_identifiers.end()) 107 : { 108 0 : throw mcrl2::runtime_error("process " + core::pp(x.name()) + " not declared"); 109 : } 110 441 : std::vector<process_identifier> result; 111 882 : for (auto k = range.first; k != range.second; ++k) 112 : { 113 441 : const process_identifier& id = k->second; 114 441 : if (is_matching_assignment(x.assignments(), id.variables())) 115 : { 116 441 : result.push_back(id); 117 : } 118 : } 119 441 : if (result.empty()) 120 : { 121 0 : std::string detailed_message; 122 : 123 : // If there is only one matching process, give a more detailed error message. 124 0 : if (std::distance(range.first, range.second) == 1) 125 : { 126 0 : const process_identifier& id = range.first->second; 127 0 : const data::untyped_identifier_assignment& a = find_violating_assignment(x.assignments(), id.variables()); 128 0 : detailed_message = "Missing parameter: " + core::pp(a.lhs()) + '\n'; 129 0 : } 130 0 : throw mcrl2::runtime_error("There is no process " + core::pp(x.name()) + " containing all assignments in " + process::pp(x) + ".\n" + detailed_message); 131 0 : } 132 441 : if (result.size() > 1) 133 : { 134 0 : throw mcrl2::runtime_error("There are multiple processes named " + core::pp(x.name()) + " containing all assignments in " + process::pp(x) + "."); 135 : } 136 882 : return result.front(); 137 441 : } 138 : 139 2121 : process_instance make_process_instance(const core::identifier_string& name, const data::sort_expression_list& formal_parameters, const data::data_expression_list& actual_parameters) const 140 : { 141 2121 : auto range = m_process_identifiers.equal_range(name); 142 2121 : assert(range.first != m_process_identifiers.end()); 143 2145 : for (auto k = range.first; k != range.second; ++k) 144 : { 145 2145 : const process_identifier& id = k->second; 146 2145 : if (data::detail::parameter_sorts(id.variables()) == formal_parameters) 147 : { 148 4242 : return process_instance(id, actual_parameters); 149 : } 150 : } 151 0 : throw mcrl2::runtime_error("no matching process found for " + core::pp(name) + "(" + data::pp(formal_parameters) + ")"); 152 : } 153 : 154 2121 : data::sorts_list matching_process_sorts(const core::identifier_string& name, const data::data_expression_list& parameters) const 155 : { 156 2121 : data::sorts_list result; 157 2121 : auto range = m_process_identifiers.equal_range(name); 158 4278 : for (auto k = range.first; k != range.second; ++k) 159 : { 160 2157 : const process_identifier& id = k->second; 161 2157 : if (id.variables().size() == parameters.size()) 162 : { 163 2121 : result.push_front(data::detail::parameter_sorts(id.variables())); 164 : } 165 : } 166 4242 : return atermpp::reverse(result); 167 2121 : } 168 : 169 1135 : void clear() 170 : { 171 1135 : m_process_identifiers.clear(); 172 1135 : } 173 : }; 174 : 175 : } // namespace detail 176 : 177 : } // namespace process 178 : 179 : } // namespace mcrl2 180 : 181 : #endif // MCRL2_PROCESS_DETAIL_PROCESS_CONTEXT_H