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/pbes/detail/pbes_parameter_map.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_DETAIL_PBES_PARAMETER_MAP_H
      13             : #define MCRL2_PBES_DETAIL_PBES_PARAMETER_MAP_H
      14             : 
      15             : #include "mcrl2/core/detail/print_utility.h"
      16             : #include "mcrl2/pbes/pbes.h"
      17             : #include <regex>
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace pbes_system
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : /// \brief Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
      29             : typedef std::map<core::identifier_string, std::vector<data::variable>> pbes_parameter_map;
      30             : 
      31             : /// \brief Returns true if the declaration text matches with the variable d.
      32             : inline
      33           7 : bool match_declaration(const std::string& text, const data::variable& d, const data::data_specification& data_spec)
      34             : {
      35          14 :   std::vector<std::string> words = utilities::split(text, ":");
      36           7 :   if (words.size() != 2)
      37             :   {
      38           0 :     throw mcrl2::runtime_error("invalid parameter declaration: '" + text + "'");
      39             :   }
      40           7 :   std::string name = utilities::trim_copy(words[0]);
      41           7 :   std::string type = utilities::trim_copy(words[1]);
      42           7 :   if (name != "*" && core::identifier_string(name) != d.name())
      43             :   {
      44           1 :     return false;
      45             :   }
      46           6 :   return type == "*" || data::parse_sort_expression(type, data_spec) == d.sort();
      47           7 : }
      48             : 
      49             : /// \brief Find parameter declarations that match a given string.
      50             : inline
      51           5 : std::vector<data::variable> find_matching_parameters(const pbes& p, const std::string& name, const std::set<std::string>& declarations)
      52             : {
      53           5 :   std::set<data::variable> result;
      54          12 :   for (const pbes_equation& eqn: p.equations())
      55             :   {
      56           7 :     const propositional_variable& X = eqn.variable();
      57           7 :     if (name == "*" || name == std::string(X.name()))
      58             :     {
      59          12 :       for (const data::variable& v: X.parameters())
      60             :       {
      61             :         // find a declaration *k that accepts the variable *j
      62           9 :         for (const std::string& declaration: declarations)
      63             :         {
      64           7 :           if (match_declaration(declaration, v, p.data()))
      65             :           {
      66           5 :             result.insert(v);
      67           5 :             break;
      68             :           }
      69             :         }
      70             :       }
      71             :     }
      72             :   }
      73          10 :   return std::vector<data::variable>(result.begin(), result.end());
      74           5 : }
      75             : 
      76             : /// \brief Parses parameter selection for finite pbesinst algorithm
      77             : inline
      78           5 : pbes_parameter_map parse_pbes_parameter_map(const pbes& p, const std::string& text)
      79             : {
      80           5 :   pbes_parameter_map result;
      81             : 
      82             :   // maps propositional variable name to the corresponding variable declarations, for example:
      83             :   // X(b:Bool,c:C) X(d:*) Y(*:Bool) results in the mapping
      84             :   //
      85             :   // X -> { "b:Bool", "c:C", "d:*" }
      86             :   // Y -> { "*:Bool" }
      87           5 :   std::map<std::string, std::set<std::string>> parameter_declarations;
      88             : 
      89          10 :   for (const std::string& s: utilities::split(text, ";"))
      90             :   {
      91           5 :     std::string line = utilities::trim_copy(s);
      92           5 :     if (line.empty())
      93             :     {
      94           0 :       continue;
      95             :     }
      96           5 :     std::regex sre(R"((\*|\w*)\(([:,#*\s\w>-]*)\)\s*)", std::regex::icase);
      97           5 :     std::match_results<std::string::const_iterator> what;
      98           5 :     if (!regex_match(line, what, sre))
      99             :     {
     100           0 :       mCRL2log(log::warning) << "ignoring selection '" << line << "'" << std::endl;
     101           0 :       continue;
     102             :     }
     103           5 :     std::string X = what[1];
     104           5 :     utilities::trim(X);
     105           5 :     std::string word = what[2];
     106           5 :     utilities::trim(word);
     107          10 :     for (const std::string& parameter: utilities::regex_split(word, "\\s*,\\s*"))
     108             :     {
     109           5 :       parameter_declarations[X].insert(parameter);
     110           5 :     }
     111          10 :   }
     112             : 
     113             :   // expand the name "*"
     114           5 :   auto q = parameter_declarations.find("*");
     115           5 :   if (q != parameter_declarations.end())
     116             :   {
     117           0 :     std::set<std::string> v = q->second;
     118           0 :     parameter_declarations.erase(q);
     119           0 :     for (const pbes_equation& eqn: p.equations())
     120             :     {
     121           0 :       std::string name = eqn.variable().name();
     122           0 :       parameter_declarations[name].insert(v.begin(), v.end());
     123           0 :     }
     124           0 :   }
     125             : 
     126             :   // create a mapping from PBES variable names to the corresponding parameters
     127           5 :   std::map<core::identifier_string, data::variable_list> pbes_index;
     128          12 :   for (const pbes_equation& eqn: p.equations())
     129             :   {
     130           7 :     const propositional_variable& X = eqn.variable();
     131           7 :     pbes_index[X.name()] = X.parameters();
     132             :   }
     133             : 
     134          10 :   for (const auto& decl: parameter_declarations)
     135             :   {
     136           5 :     core::identifier_string name(decl.first);
     137           5 :     std::vector<data::variable> variables = find_matching_parameters(p, decl.first, decl.second);
     138             : 
     139             :     // sort variables according to their position in the PBES variable
     140           5 :     std::map<data::variable, std::size_t> m;
     141           5 :     std::size_t index = 0;
     142          12 :     for (const data::variable& v: pbes_index[name])
     143             :     {
     144           7 :       m[v] = index++;
     145             :     }
     146           5 :     std::sort(variables.begin(), variables.end(), [&](const data::variable& x, const data::variable& y) { return m[x] < m[y]; });
     147             : 
     148           5 :     result[name] = variables;
     149           5 :   }
     150             : 
     151          10 :   return result;
     152           5 : }
     153             : 
     154             : /// \brief Print a parameter map.
     155             : inline
     156             : std::ostream& print_pbes_parameter_map(std::ostream& out, const pbes_parameter_map& m)
     157             : {
     158             :   for (const auto& p: m)
     159             :   {
     160             :     out << p.first << " -> " << core::detail::print_list(p.second) << std::endl;
     161             :   }
     162             :   return out;
     163             : }
     164             : 
     165             : } // namespace detail
     166             : 
     167             : } // namespace pbes_system
     168             : 
     169             : } // namespace mcrl2
     170             : 
     171             : #endif // MCRL2_PBES_DETAIL_PBES_PARAMETER_MAP_H