LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps - is_well_typed.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 91 137 66.4 %
Date: 2024-03-08 02:52:28 Functions: 27 30 90.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/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

Generated by: LCOV version 1.14