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/is_well_typed.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_LPS_IS_WELL_TYPED_H 13 : #define MCRL2_LPS_IS_WELL_TYPED_H 14 : 15 : #include "mcrl2/data/detail/sequence_algorithm.h" 16 : #include "mcrl2/lps/detail/action_utility.h" 17 : #include "mcrl2/lps/stochastic_specification.h" 18 : #include <boost/iterator/transform_iterator.hpp> 19 : 20 : namespace mcrl2 { 21 : 22 : namespace lps { 23 : 24 : namespace detail 25 : { 26 : 27 : /// \brief Function object for applying a substitution to LPS data types. 28 : struct lps_well_typed_checker 29 : { 30 : // The result of the last well typedness check. 31 : bool result; 32 : 33 : // Error message are written to the output stream error. 34 : mutable std::ostringstream error; 35 : 36 635 : lps_well_typed_checker() 37 635 : : result(false) 38 635 : {} 39 : 40 : /// \brief Checks if the sort of t has type real 41 291 : bool check_time(const data::data_expression& t, const std::string& type) const 42 : { 43 291 : if (!data::sort_real::is_real(t.sort())) 44 : { 45 0 : error << "is_well_typed(" << type << ") failed: time " << t << " doesn't have sort real." << std::endl; 46 0 : return false; 47 : } 48 291 : return true; 49 : } 50 : 51 : /// \brief Checks if the sort of t has type bool 52 1987 : bool check_condition(const data::data_expression& t, const std::string& type) const 53 : { 54 1987 : if (!data::sort_bool::is_bool(t.sort())) 55 : { 56 0 : error << "is_well_typed(" << type << ") failed: condition " << t << " doesn't have sort bool." << std::endl; 57 0 : return false; 58 : } 59 1987 : return true; 60 : } 61 : 62 : /// \brief Checks if the assignments are well typed and have unique left hand sides 63 1499 : bool check_assignments(const data::assignment_list& l, const std::string& type) const 64 : { 65 1499 : if (!is_well_typed_container(l)) 66 : { 67 0 : error << "is_well_typed(" << type << ") failed: the assignments " << l << " are not well typed." << std::endl; 68 0 : return false; 69 : } 70 1880 : auto lhs = [](const data::assignment& a) { return a.lhs(); }; 71 1499 : if (data::detail::sequence_contains_duplicates( 72 1499 : boost::make_transform_iterator(l.begin(), lhs), 73 2998 : boost::make_transform_iterator(l.end() , lhs) 74 : ) 75 : ) 76 : { 77 0 : error << "is_well_typed(" << type << ") failed: data assignments " << l << " don't have unique left hand sides." << std::endl; 78 0 : return false; 79 : } 80 1499 : return true; 81 : } 82 : 83 : /// \brief Checks well typedness of the elements of a container 84 : template <typename Container> 85 2769 : bool is_well_typed_container(const Container& c) const 86 : { 87 6636 : for (auto i = c.begin(); i != c.end(); ++i) 88 : { 89 3867 : if (!is_well_typed(*i)) 90 : { 91 0 : return false; 92 : } 93 : } 94 2769 : return true; 95 : } 96 : 97 : /// \brief Checks well typedness of a sort expression. 98 : /// \param d A sort expression. 99 : bool is_well_typed(const data::sort_expression& d) const 100 : { 101 : (void)d; // Suppress an unused variable warning. 102 : return true; 103 : } 104 : 105 : /// \brief Checks well typedness of a variable. 106 : /// \param d A variable. 107 : bool is_well_typed(const data::variable& d) const 108 : { 109 : (void)d; // Suppress an unused variable warning. 110 : return true; 111 : } 112 : 113 : /// \brief Checks well typedness of a data expression 114 : /// \param d A data expression 115 : bool is_well_typed(const data::data_expression& d) const 116 : { 117 : (void)d; // Suppress an unused variable warning. 118 : return true; 119 : } 120 : 121 : /// \brief Traverses an assignment 122 : /// \param a An assignment 123 1880 : bool is_well_typed(const data::assignment& a) const 124 : { 125 1880 : if (a.lhs().sort() != a.rhs().sort()) 126 : { 127 0 : std::clog << "is_well_typed(data_assignment) failed: the left and right hand sides " 128 0 : << a.lhs() << " and " << a.rhs() << " have different sorts." << std::endl; 129 0 : return false; 130 : } 131 1880 : return true; 132 : } 133 : 134 : /// \brief Traverses an action label. 135 : /// \param d An action label. 136 : bool is_well_typed(const process::action_label& d) const 137 : { 138 : (void)d; // Suppress an unused variable warning. 139 : return true; 140 : } 141 : 142 : /// \brief Traverses an action. 143 : /// \param a An action. 144 : bool is_well_typed(const process::action& a) const 145 : { 146 : (void)a; // Suppress an unused variable warning. 147 : return true; 148 : } 149 : 150 : /// \brief Checks well typedness of a deadlock 151 : /// \param d A deadlock 152 : /// \return Returns true if 153 : /// <ul> 154 : /// <li>the (optional) time has sort Real</li> 155 : /// </ul> 156 488 : bool is_well_typed(const deadlock& d) const 157 : { 158 488 : if (d.has_time()) 159 : { 160 35 : check_time(d.time(), "deadlock"); 161 : } 162 488 : return true; 163 : } 164 : 165 : /// \brief Checks well typedness of a multi-action 166 : /// \param a A multi-action 167 : /// \return Returns true if 168 : /// <ul> 169 : /// <li>the (optional) time has sort Real</li> 170 : /// </ul> 171 1499 : bool is_well_typed(const multi_action& a) const 172 : { 173 1499 : if (a.has_time()) 174 : { 175 256 : check_time(a.time(), "multi_action"); 176 : } 177 1499 : return true; 178 : } 179 : 180 : /// \brief Checks well typedness of a summand 181 : /// \param s An action summand 182 1499 : bool is_well_typed(const action_summand& s) const 183 : { 184 1499 : if (!data::detail::unique_names(s.summation_variables())) 185 : { 186 0 : error << "is_well_typed(action_summand) failed: summation variables " << core::detail::print_list(s.summation_variables()) << " don't have unique names." << std::endl; 187 0 : return false; 188 : } 189 1499 : if (!check_condition(s.condition(), "action_summand")) 190 : { 191 0 : return false; 192 : } 193 1499 : if (!is_well_typed(s.multi_action())) 194 : { 195 0 : return false; 196 : } 197 1499 : if (!check_assignments(s.assignments(), "action_summand")) 198 : { 199 0 : return false; 200 : } 201 1499 : return true; 202 : } 203 : 204 : /// \brief Checks well typedness of a summand 205 : /// \param s A summand 206 488 : bool is_well_typed(const deadlock_summand& s) const 207 : { 208 488 : if (!check_condition(s.condition(), "deadlock_summand")) 209 : { 210 0 : return false; 211 : } 212 488 : if (!is_well_typed(s.deadlock())) 213 : { 214 0 : return false; 215 : } 216 488 : return true; 217 : } 218 : 219 : /// \brief Checks well typedness of a linear process 220 : /// \param p A linear_process 221 : /// \return True if 222 : /// <ul> 223 : /// <li>the process parameters have unique names</li> 224 : /// <li>process parameters and summation variables have different names</li> 225 : /// <li>the left hand sides of the assignments of summands are contained in the process parameters</li> 226 : /// <li>the summands are well typed</li> 227 : /// </ul> 228 : template <typename ActionSummand> 229 635 : bool is_well_typed(const linear_process_base<ActionSummand>& p) const 230 : { 231 : // check 2) 232 635 : if (!data::detail::unique_names(p.process_parameters())) 233 : { 234 0 : error << "is_well_typed(linear_process) failed: process parameters " << core::detail::print_list(p.process_parameters()) << " don't have unique names." << std::endl; 235 0 : return false; 236 : } 237 : 238 : // check 4) 239 635 : std::set<core::identifier_string> names; 240 1341 : for (auto i = p.process_parameters().begin(); i != p.process_parameters().end(); ++i) 241 : { 242 706 : names.insert(i->name()); 243 : } 244 2134 : for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i) 245 : { 246 1499 : if (!data::detail::check_variable_names(i->summation_variables(), names)) 247 : { 248 0 : error << "is_well_typed(linear_process) failed: some of the names of the summation variables " << core::detail::print_list(i->summation_variables()) << " also appear as process parameters." << std::endl; 249 0 : return false; 250 : } 251 : } 252 : 253 : // check 5) 254 2134 : for (auto i = p.action_summands().begin(); i != p.action_summands().end(); ++i) 255 : { 256 1499 : if (!data::detail::check_assignment_variables(i->assignments(), p.process_parameters())) 257 : { 258 0 : error << "is_well_typed(linear_process) failed: some left hand sides of the assignments " << core::detail::print_list(i->assignments()) << " do not appear as process parameters." << std::endl; 259 0 : return false; 260 : } 261 : } 262 : 263 : // check 6) 264 635 : if (!is_well_typed_container(p.action_summands())) 265 : { 266 0 : return false; 267 : } 268 635 : if (!is_well_typed_container(p.deadlock_summands())) 269 : { 270 0 : return false; 271 : } 272 635 : return true; 273 635 : } 274 : 275 : /// \brief Checks well typedness of a linear process specification. 276 : /// \param spec A linear process specification. 277 : /// \param free_variables Free variables that can be used. 278 : /// \return True if 279 : /// <ul> 280 : /// <li>the sorts occurring in the summation variables are declared in the data specification</li> 281 : /// <li>the sorts occurring in the process parameters are declared in the data specification </li> 282 : /// <li>the sorts occurring in the free variables are declared in the data specification </li> 283 : /// <li>the sorts occurring in the action labels are declared in the data specification </li> 284 : /// <li>the action labels occurring in the process are contained in action_labels() </li> 285 : /// <li>the process is well typed </li> 286 : /// <li>the data specification is well typed </li> 287 : /// <li>the initial process is well typed </li> 288 : /// <li>the free variables occurring in the linear process are declared in the global variable specification</li> 289 : /// <li>the free variables occurring in the initial process are declared in the global variable specification</li> 290 : /// <li>the global variables have unique names</li> 291 : /// </ul> 292 : template <typename LinearProcess, typename InitialProcessExpression> 293 634 : bool is_well_typed(const specification_base<LinearProcess, InitialProcessExpression>& spec, 294 : const std::set<data::variable>& free_variables) const 295 : { 296 634 : std::set<data::sort_expression> declared_sorts = data::detail::make_set(spec.data().sorts()); 297 634 : std::set<process::action_label> declared_labels = data::detail::make_set(spec.action_labels()); 298 634 : auto const& action_summands = spec.process().action_summands(); 299 : 300 : // check 1) 301 2132 : for (auto i = action_summands.begin(); i != action_summands.end(); ++i) 302 : { 303 1498 : if (!(data::detail::check_variable_sorts(i->summation_variables(), declared_sorts))) 304 : { 305 0 : error << "is_well_typed(specification) failed: some of the sorts of the summation variables " << core::detail::print_list(i->summation_variables()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl; 306 0 : return false; 307 : } 308 : } 309 : 310 : // check 2) 311 634 : if (!(data::detail::check_variable_sorts(spec.process().process_parameters(), declared_sorts))) 312 : { 313 0 : error << "is_well_typed(specification) failed: some of the sorts of the process parameters " << core::detail::print_list(spec.process().process_parameters()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl; 314 0 : return false; 315 : } 316 : 317 : // check 3) 318 634 : if (!(data::detail::check_variable_sorts(spec.global_variables(), declared_sorts))) 319 : { 320 0 : error << "is_well_typed(specification) failed: some of the sorts of the free variables " << core::detail::print_list(spec.global_variables()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl; 321 0 : return false; 322 : } 323 : 324 : // check 4) 325 634 : if (!(detail::check_action_label_sorts(spec.action_labels(), declared_sorts))) 326 : { 327 0 : error << "is_well_typed(specification) failed: some of the sorts occurring in the action labels " << core::detail::print_list(spec.action_labels()) << " are not declared in the data specification " << core::detail::print_list(spec.data().sorts()) << std::endl; 328 0 : return false; 329 : } 330 : 331 : // check 5) 332 2132 : for (const action_summand& s: action_summands) 333 : { 334 1498 : if (!(detail::check_action_labels(s.multi_action().actions(), declared_labels))) 335 : { 336 0 : error << "is_well_typed(specification) failed: some of the labels occurring in the actions " << core::detail::print_list(s.multi_action().actions()) << " are not declared in the action specification " << core::detail::print_list(spec.action_labels()) << std::endl; 337 0 : return false; 338 : } 339 : } 340 634 : if (!is_well_typed(spec.process())) 341 : { 342 0 : return false; 343 : } 344 634 : if (!spec.data().is_well_typed()) 345 : { 346 0 : return false; 347 : } 348 634 : if (!free_variables.empty()) 349 : { 350 0 : error << "is_well_typed(specification) failed: some of the free variables were not declared\n"; 351 0 : error << "declared global variables: " << core::detail::print_list(spec.global_variables()) << std::endl; 352 0 : error << "occurring free variables: " << core::detail::print_list(free_variables) << std::endl; 353 0 : return false; 354 : } 355 : 356 : // check 3) 357 634 : if (!data::detail::unique_names(spec.global_variables())) 358 : { 359 0 : error << "is_well_typed(specification) failed: global variables " << core::detail::print_list(spec.global_variables()) << " don't have unique names." << std::endl; 360 0 : return false; 361 : } 362 : 363 634 : return true; 364 634 : } 365 : 366 17 : bool is_well_typed(const specification& spec) const 367 : { 368 17 : std::set<data::variable> free_variables = lps::find_free_variables(spec); 369 34 : return is_well_typed(spec, free_variables); 370 17 : } 371 : 372 617 : bool is_well_typed(const stochastic_specification& spec) const 373 : { 374 617 : std::set<data::variable> free_variables = lps::find_free_variables(spec); 375 1234 : return is_well_typed(spec, free_variables); 376 617 : } 377 : 378 : template <typename Term> 379 635 : bool operator()(const Term& t) const 380 : { 381 635 : return is_well_typed(t); 382 : } 383 : }; 384 : 385 : /// \brief Checks well typedness of an LPS object. 386 : template <typename T> 387 607 : bool is_well_typed(const T& x) 388 : { 389 607 : lps::detail::lps_well_typed_checker checker; 390 1214 : return checker(x); 391 607 : } 392 : 393 : /// \brief Checks well typedness of an LPS object, and will print error messages to stderr. 394 : template <typename T> 395 28 : bool check_well_typedness(const T& x) 396 : { 397 28 : lps::detail::lps_well_typed_checker checker; 398 28 : bool result = checker(x); 399 28 : if (!result) 400 : { 401 0 : mCRL2log(log::error) << checker.error.str(); 402 : } 403 28 : return result; 404 28 : } 405 : 406 : } // namespace detail 407 : 408 : } // namespace lps 409 : 410 : } // namespace mcrl2 411 : 412 : #endif // MCRL2_LPS_IS_WELL_TYPED_H