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/lps/detail/specification_property_map.h 10 : /// \brief A property map containing properties of an LPS specification. 11 : 12 : #ifndef MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H 13 : #define MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H 14 : 15 : #include "mcrl2/data/detail/data_property_map.h" 16 : #include "mcrl2/lps/specification.h" 17 : #include <boost/algorithm/string/split.hpp> 18 : #include <boost/algorithm/string/trim.hpp> 19 : 20 : namespace mcrl2 21 : { 22 : 23 : namespace lps 24 : { 25 : 26 : namespace detail 27 : { 28 : 29 : /// \brief Stores the following properties of a linear process specification: 30 : /// <table> 31 : /// <tr><th>property </th><th>description </th><th>format </th></tr> 32 : /// <tr><td>summand_count </td><td>The number of summands </td><td>NUMBER </td></tr> 33 : /// <tr><td>tau_summand_count </td><td>The number of tau summands </td><td>NUMBER </td></tr> 34 : /// <tr><td>delta_summand_count </td><td>The number of delta summands </td><td>NUMBER </td></tr> 35 : /// <tr><td>declared_free_variables </td><td>The declared free variables </td><td>NAME:SORT; ... ; NAME:SORT </td></tr> 36 : /// <tr><td>declared_free_variable_names</td><td>The names of the declared free variables </td><td>NAME; ... ; NAME </td></tr> 37 : /// <tr><td>declared_variable_count </td><td>The number of declared free variables </td><td>NUMBER </td></tr> 38 : /// <tr><td>used_free_variables </td><td>The used free variables </td><td>NAME:SORT; ... ; NAME:SORT </td></tr> 39 : /// <tr><td>used_free_variables_names </td><td>The names of the used free variables </td><td>NAME; ... ; NAME </td></tr> 40 : /// <tr><td>used_free_variable_count </td><td>The number of used free variables </td><td>NUMBER </td></tr> 41 : /// <tr><td>process_parameters </td><td>The process parameters </td><td>NAME:SORT; ... ; NAME:SORT </td></tr> 42 : /// <tr><td>process_parameter_names </td><td>The names of the process parameters </td><td>NAME; ... ; NAME </td></tr> 43 : /// <tr><td>process_parameter_count </td><td>The number of process parameters </td><td>NUMBER </td></tr> 44 : /// <tr><td>declared_action_labels </td><td>The names of the declared action labels </td><td>NAME; ... ; NAME </td></tr> 45 : /// <tr><td>declared_action_label_count </td><td>The number of declared action labels </td><td>NUMBER </td></tr> 46 : /// <tr><td>used_action_labels </td><td>The names of the used action labels </td><td>NAME; ... ; NAME </td></tr> 47 : /// <tr><td>used_action_label_count </td><td>The number of used action labels </td><td>NUMBER </td></tr> 48 : /// <tr><td>used_multi_actions </td><td>The used multi-actions (sets of label names)</td><td>{NAME,...,NAME}; ... ; {NAME,...,NAME}</td></tr> 49 : /// <tr><td>used_multi_action_count </td><td>The number of used multi-actions </td><td>NUMBER 50 : /// </table> 51 : template <typename Specification = specification> 52 : class specification_property_map: protected mcrl2::data::detail::data_property_map<specification_property_map<Specification> > 53 : { 54 : protected: 55 : 56 : // Allow base class access to protected functions 57 : friend class data::detail::data_property_map<specification_property_map<Specification> >; 58 : 59 : typedef data::detail::data_property_map<specification_property_map> super; 60 : 61 : using super::m_data; 62 : using super::names; 63 : using super::print; 64 : using super::parse_unsigned_int; 65 : using super::parse_set_string; 66 : using super::parse_set_multiset_string; 67 : 68 171 : std::string print(const process::action_label& l) const 69 : { 70 171 : return core::pp(l.name()); 71 : } 72 : 73 : std::string print(const process::action& a) const 74 : { 75 : return process::pp(a); 76 : } 77 : 78 : std::string print(const deadlock& x) const 79 : { 80 : return lps::pp(x); 81 : } 82 : 83 : std::string print(const multi_action& x) const 84 : { 85 : return lps::pp(x); 86 : } 87 : 88 34 : std::string print(const std::set<std::multiset<process::action_label> >& v) const 89 : { 90 34 : std::set<std::string> elements; 91 83 : for (const auto& s: v) 92 : { 93 49 : elements.insert(print(s)); 94 : } 95 68 : return utilities::string_join(elements, "; "); 96 34 : } 97 : 98 : // super class compare functions 99 : using super::compare; 100 : 101 41 : std::string compare_property(std::string property, std::string x, std::string y) const 102 : { 103 41 : if (property == "summand_count") 104 : { 105 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 106 : } 107 40 : else if (property == "tau_summand_count") 108 : { 109 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 110 : } 111 39 : else if (property == "delta_summand_count") 112 : { 113 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 114 : } 115 38 : else if (property == "declared_free_variables") 116 : { 117 0 : return compare(property, parse_set_string(x), parse_set_string(y)); 118 : } 119 38 : else if (property == "declared_free_variable_names") 120 : { 121 1 : return compare(property, parse_set_string(x), parse_set_string(y)); 122 : } 123 37 : else if (property == "declared_free_variable_count") 124 : { 125 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 126 : } 127 36 : else if (property == "used_free_variables") 128 : { 129 0 : return compare(property, parse_set_string(x), parse_set_string(y)); 130 : } 131 36 : else if (property == "used_free_variable_names") 132 : { 133 1 : return compare(property, parse_set_string(x), parse_set_string(y)); 134 : } 135 35 : else if (property == "used_free_variable_count") 136 : { 137 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 138 : } 139 34 : else if (property == "process_parameters") 140 : { 141 0 : return compare(property, parse_set_string(x), parse_set_string(y)); 142 : } 143 34 : else if (property == "process_parameter_names") 144 : { 145 26 : return compare(property, parse_set_string(x), parse_set_string(y)); 146 : } 147 8 : else if (property == "process_parameter_count") 148 : { 149 2 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 150 : } 151 6 : else if (property == "declared_action_labels") 152 : { 153 1 : return compare(property, parse_set_string(x), parse_set_string(y)); 154 : } 155 5 : else if (property == "declared_action_label_count") 156 : { 157 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 158 : } 159 4 : else if (property == "used_action_labels") 160 : { 161 1 : return compare(property, parse_set_string(x), parse_set_string(y)); 162 : } 163 3 : else if (property == "used_action_label_count") 164 : { 165 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 166 : } 167 2 : else if (property == "used_multi_actions") 168 : { 169 1 : return compare(property, parse_set_multiset_string(x), parse_set_multiset_string(y)); 170 : } 171 1 : else if (property == "used_multi_action_count") 172 : { 173 1 : return compare(property, parse_unsigned_int(x), parse_unsigned_int(y)); 174 : } 175 0 : return "ERROR: unknown property " + property + " encountered!"; 176 : } 177 : 178 : //--------------------------------------------// 179 : // compute functions 180 : //--------------------------------------------// 181 : // TODO: the compute functions can be combined for efficiency 182 34 : std::set<std::multiset<process::action_label> > compute_used_multi_actions(const Specification& spec) const 183 : { 184 34 : std::set<std::multiset<process::action_label> > result; 185 91 : for (auto i = spec.process().action_summands().begin(); i != spec.process().action_summands().end(); ++i) 186 : { 187 57 : std::multiset<process::action_label> labels; 188 167 : for (const process::action& a: i->multi_action().actions()) 189 : { 190 53 : labels.insert(a.label()); 191 : } 192 57 : result.insert(labels); 193 : } 194 34 : return result; 195 0 : } 196 : 197 34 : std::set<process::action_label> compute_used_action_labels(const Specification& spec) const 198 : { 199 34 : std::set<process::action_label> result; 200 91 : for (auto i = spec.process().action_summands().begin(); i != spec.process().action_summands().end(); ++i) 201 : { 202 167 : for (const process::action& a: i->multi_action().actions()) 203 : { 204 53 : result.insert(a.label()); 205 : } 206 : } 207 34 : return result; 208 0 : } 209 : 210 34 : std::size_t compute_tau_summand_count(const Specification& spec) const 211 : { 212 34 : std::size_t result = 0; 213 34 : auto const& summands = spec.process().action_summands(); 214 91 : for (auto i = summands.begin(); i != summands.end(); ++i) 215 : { 216 57 : if (i->is_tau()) 217 : { 218 4 : result++; 219 : } 220 : } 221 34 : return result; 222 : } 223 : 224 34 : std::set<data::variable> compute_used_free_variables(const Specification& spec) const 225 : { 226 34 : return lps::find_free_variables(spec.process()); 227 : } 228 : 229 : public: 230 : /// \brief Constructor. 231 : /// The strings may appear in a random order, and not all of them need to be present 232 27 : specification_property_map(const std::string& text) 233 27 : : super(text) 234 27 : {} 235 : 236 : /// \brief Constructor 237 : /// Initializes the specification_property_map with a linear process specification 238 34 : specification_property_map(const Specification& spec) 239 34 : { 240 34 : std::size_t summand_count = spec.process().summand_count(); 241 34 : std::size_t tau_summand_count = compute_tau_summand_count(spec); 242 34 : std::size_t delta_summand_count = spec.process().deadlock_summands().size(); 243 34 : const std::set<data::variable>& declared_free_variables = spec.global_variables(); 244 34 : std::set<data::variable> used_free_variables = compute_used_free_variables(spec); 245 34 : auto const& params = spec.process().process_parameters(); 246 34 : std::set<data::variable> process_parameters(params.begin(), params.end()); 247 34 : auto const& action_labels = spec.action_labels(); 248 34 : std::set<process::action_label> declared_action_labels(action_labels.begin(),action_labels.end()); 249 34 : std::set<process::action_label> used_action_labels = compute_used_action_labels(spec); 250 34 : auto used_multi_actions = compute_used_multi_actions(spec); 251 : 252 34 : m_data["summand_count" ] = print(summand_count); 253 34 : m_data["tau_summand_count" ] = print(tau_summand_count); 254 34 : m_data["delta_summand_count" ] = print(delta_summand_count); 255 34 : m_data["declared_free_variables" ] = print(declared_free_variables, false); 256 34 : m_data["declared_free_variable_names"] = print(names(declared_free_variables), false); 257 34 : m_data["declared_free_variable_count"] = print(declared_free_variables.size()); 258 34 : m_data["used_free_variables" ] = print(used_free_variables, false); 259 34 : m_data["used_free_variable_names" ] = print(names(used_free_variables), false); 260 34 : m_data["used_free_variable_count" ] = print(used_free_variables.size()); 261 34 : m_data["process_parameters" ] = print(process_parameters, false); 262 34 : m_data["process_parameter_names" ] = print(names(process_parameters), false); 263 34 : m_data["process_parameter_count" ] = print(process_parameters.size()); 264 34 : m_data["declared_action_labels" ] = print(declared_action_labels, false); 265 34 : m_data["declared_action_label_count" ] = print(declared_action_labels.size()); 266 34 : m_data["used_action_labels" ] = print(used_action_labels, false); 267 34 : m_data["used_action_label_count" ] = print(used_action_labels.size()); 268 34 : m_data["used_multi_actions" ] = print(used_multi_actions); 269 34 : m_data["used_multi_action_count" ] = print(used_multi_actions.size()); 270 34 : } 271 : 272 : using super::to_string; 273 : using super::data; 274 : using super::operator[]; 275 : 276 27 : std::string compare(const specification_property_map<Specification>& other) const 277 : { 278 27 : return super::compare(other); 279 : } 280 : 281 : /// \brief Returns a textual overview of some properties of an LPS 282 0 : std::string info() const 283 : { 284 0 : std::ostringstream out; 285 0 : out << "Number of summands : " << (*this)["summand_count" ] << "\n"; 286 0 : out << "Number of tau-summands : " << (*this)["tau_summand_count" ] << "\n"; 287 0 : out << "Number of declared global variables : " << (*this)["declared_free_variable_count"] << "\n"; 288 0 : out << "Number of process parameters : " << (*this)["process_parameter_count" ] << "\n"; 289 0 : out << "Number of declared action labels : " << (*this)["declared_action_label_count" ] << "\n"; 290 0 : out << "Number of used actions : " << (*this)["used_action_label_count" ] << "\n"; 291 0 : out << "Number of used multi-actions : " << (*this)["used_multi_action_count" ] << "\n"; 292 0 : return out.str(); 293 0 : } 294 : }; 295 : 296 : } // namespace detail 297 : 298 : } // namespace lps 299 : 300 : } // namespace mcrl2 301 : 302 : #endif // MCRL2_LPS_DETAIL_SPECIFICATION_PROPERTY_MAP_H