Line data    Source code

       1             : // Author(s): Wieger Wesselink, Thomas Neele
       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/parameter_selection.h
      10             : /// \brief
      11             : 
      12             : #ifndef MCRL2_LPS_DETAIL_PARAMETER_SELECTION_H
      13             : #define MCRL2_LPS_DETAIL_PARAMETER_SELECTION_H
      14             : 
      15             : #include "mcrl2/core/detail/print_utility.h"
      16             : #include "mcrl2/data/parse.h"
      17             : #include <regex>
      18             : 
      19             : namespace mcrl2::lps::detail
      20             : {
      21             : 
      22             : /// \brief Returns true if the selection name:type matches with the variable v.
      23             : inline
      24           3 : bool match_selection(const data::variable& v, const std::string& name, const std::string& type, const data::data_specification& data_spec)
      25             : {
      26           3 :   if (name != "*" && core::identifier_string(name) != v.name())
      27             :   {
      28           0 :     return false;
      29             :   }
      30           3 :   return type == "*" || data::parse_sort_expression(type, data_spec) == v.sort();
      31             : }
      32             : 
      33             : /// \brief Find parameter declarations that match a given string.
      34             : template <typename OutputIterator>
      35             : inline
      36           1 : std::vector<data::variable> find_matching_parameters(
      37             :   const data::variable_list& params,
      38             :   const data::data_specification& dataspec,
      39             :   const std::vector<std::pair<std::string, std::string>>& selections,
      40             :   OutputIterator o
      41             :   )
      42             : {
      43           1 :   std::set<data::variable> result;
      44           5 :   for (const data::variable& v: params)
      45             :   {
      46           6 :     for (const auto& [name, type]: selections)
      47             :     {
      48           3 :       if (match_selection(v, name, type, dataspec))
      49             :       {
      50           1 :         *o = v;
      51             :       }
      52             :     }
      53             :   }
      54           2 :   return std::vector<data::variable>(result.begin(), result.end());
      55           1 : }
      56             : 
      57             : /// \brief Parses parameter selection for finite pbesinst algorithm
      58             : inline
      59           1 : std::vector<data::variable> parse_lps_parameter_selection(const data::variable_list& params, const data::data_specification& dataspec, const std::string& text)
      60             : {
      61           1 :   std::vector<data::variable> result;
      62             : 
      63           1 :   std::string line = utilities::trim_copy(text);
      64           1 :   if (line.empty())
      65             :   {
      66           0 :     throw mcrl2::runtime_error("The parameter selection argument is empty.");
      67             :   }
      68           1 :   std::regex sre(R"(\s*(\w[\w']*|\*)\s*:\s*(\w[\w']*|\*)\s*)", std::regex::icase);
      69           1 :   std::vector<std::pair<std::string, std::string>> selections;
      70           2 :   for (const std::string& var_sort: utilities::split(text, ","))
      71             :   {
      72           1 :     std::match_results<std::string::const_iterator> what;
      73           1 :     if (!std::regex_match(var_sort, what, sre))
      74             :     {
      75           0 :       mCRL2log(log::warning) << "Ignoring " << var_sort << " since it does not follow the necessary format (NAME:SORT)." << std::endl;
      76           0 :       continue;
      77             :     }
      78             : 
      79           1 :     selections.push_back(std::make_pair(what[1], what[2]));
      80           2 :   }
      81             : 
      82           1 :   find_matching_parameters(params, dataspec, selections, std::inserter(result, result.end()));
      83             : 
      84             :   // sort the parameters in result according to their position in params
      85           1 :   std::map<data::variable, std::size_t> m;
      86           1 :   std::size_t index = 0;
      87           4 :   for (const data::variable& v: params)
      88             :   {
      89           3 :     m[v] = index++;
      90             :   }
      91           1 :   std::sort(result.begin(), result.end(), [&](const data::variable& x, const data::variable& y) { return m[x] < m[y]; });
      92             : 
      93           2 :   return result;
      94           1 : }
      95             : 
      96             : } // namespace mcrl2::lps::detail
      97             : 
      98             : #endif // MCRL2_LPS_DETAIL_PARAMETER_SELECTION_H