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/resolve_name_clashes.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_RESOLVE_NAME_CLASHES_H
      13             : #define MCRL2_LPS_RESOLVE_NAME_CLASHES_H
      14             : 
      15             : #include "mcrl2/lps/replace.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace lps {
      20             : 
      21             : namespace detail {
      22             : 
      23             : // returns the names of the variables in v
      24             : template <typename VariableContainer>
      25         203 : std::set<core::identifier_string> variable_names(const VariableContainer& vars)
      26             : {
      27         203 :   std::set<core::identifier_string> result;
      28         761 :   for (const data::variable& v: vars)
      29             :   {
      30         355 :     result.insert(v.name());
      31             :   }
      32         203 :   return result;
      33           0 : }
      34             : 
      35             : // returns the names of variables in v that are also in w
      36             : template <typename VariableContainer>
      37         427 : std::set<core::identifier_string> variable_name_clashes(const VariableContainer& vars, const std::set<core::identifier_string>& w)
      38             : {
      39         427 :   std::set<core::identifier_string> result;
      40        1036 :   for (const data::variable& v: vars)
      41             :   {
      42         182 :     if (w.find(v.name()) != w.end())
      43             :     {
      44          14 :       result.insert(v.name());
      45             :     }
      46             :   }
      47         427 :   return result;
      48           0 : }
      49             : 
      50             : inline
      51         354 : void resolve_summand_variable_name_clashes(action_summand& summand, 
      52             :                                            const std::set<core::identifier_string>& process_parameter_names, 
      53             :                                            data::set_identifier_generator& generator)
      54             : {
      55         354 :   const data::variable_list& summation_variables = summand.summation_variables();
      56         354 :   std::set<core::identifier_string> names = variable_name_clashes(summation_variables, process_parameter_names);
      57         354 :   if (!names.empty())
      58             :   {
      59          14 :     data::mutable_map_substitution<> sigma;
      60          28 :     for (const data::variable& v: summation_variables)
      61             :     {
      62          14 :       if (process_parameter_names.find(v.name()) != process_parameter_names.end())
      63             :       {
      64          14 :         sigma[v] = data::variable(generator(v.name()), v.sort());
      65             :       }
      66             :     }
      67          14 :     lps::replace_all_variables(summand, sigma);
      68          14 :   }
      69         354 : }
      70             : 
      71             : inline
      72          73 : void resolve_summand_variable_name_clashes(deadlock_summand& summand, 
      73             :                                            const std::set<core::identifier_string>& process_parameter_names, 
      74             :                                            data::set_identifier_generator& generator)
      75             : {
      76          73 :   const data::variable_list& summation_variables = summand.summation_variables();
      77          73 :   std::set<core::identifier_string> names = variable_name_clashes(summation_variables, process_parameter_names);
      78          73 :   if (!names.empty())
      79             :   {
      80           0 :     data::mutable_map_substitution<> sigma;
      81           0 :     for (const data::variable& v: summation_variables)
      82             :     {
      83           0 :       if (process_parameter_names.find(v.name()) != process_parameter_names.end())
      84             :       {
      85           0 :         sigma[v] = data::variable(generator(v.name()), v.sort());
      86             :       }
      87             :     }
      88           0 :     lps::replace_all_variables(summand, sigma);
      89           0 :   }
      90          73 : }
      91             : 
      92             : inline
      93         135 : void resolve_summand_variable_name_clashes(stochastic_action_summand& summand, 
      94             :                                            const std::set<core::identifier_string>& process_parameter_names, 
      95             :                                            data::set_identifier_generator& generator)
      96             : {
      97         135 :   data::mutable_map_substitution<> sigma;
      98         135 :   std::set<core::identifier_string> summation_names;
      99             : 
     100             :   // handle the summation variables
     101         163 :   for (const data::variable& v: summand.summation_variables())
     102             :   {
     103          28 :     if (process_parameter_names.find(v.name()) != process_parameter_names.end())
     104             :     {
     105           0 :       sigma[v] = data::variable(generator(v.name()), v.sort());
     106             :     }
     107          28 :     summation_names.insert(v.name());
     108             :   }
     109         135 :   if (!sigma.empty())
     110             :   {
     111           0 :     lps::replace_all_variables(summand, sigma);
     112             :   }
     113             : 
     114             :   // handle the distribution variables
     115         135 :   sigma.clear();
     116             : 
     117         244 :   for (const data::variable& v: summand.distribution().variables())
     118             :   {
     119         116 :     if (process_parameter_names.find(v.name()) != process_parameter_names.end() ||
     120         116 :         summation_names.find(v.name()) != summation_names.end())  // Check stochastic variables also with respect to the summand variables. 
     121             :     {
     122         102 :       sigma[v] = data::variable(generator(v.name()), v.sort());
     123             :     }
     124             :   }
     125         135 :   if (!sigma.empty())
     126             :   {
     127         102 :     summand.distribution() = lps::replace_all_variables(summand.distribution(), sigma);
     128         102 :     summand.assignments() = lps::replace_all_variables(summand.assignments(), sigma);
     129             :   }
     130         135 : }
     131             : 
     132             : } // namespace detail
     133             : 
     134             : /// \brief Renames summand variables such that there are no name clashes between summand variables and process parameters
     135             : template <typename Specification>
     136         203 : void resolve_summand_variable_name_clashes(Specification& spec)
     137             : {
     138         203 :   typename Specification::process_type& proc = spec.process();
     139         203 :   std::set<core::identifier_string> process_parameter_names = detail::variable_names(proc.process_parameters());
     140             : 
     141         203 :   data::set_identifier_generator generator;
     142         203 :   generator.add_identifiers(lps::find_identifiers(spec));
     143         203 :   generator.add_identifiers(data::function_and_mapping_identifiers(spec.data()));
     144             : 
     145         692 :   for (typename Specification::process_type::action_summand_type& s: proc.action_summands())
     146             :   {
     147         489 :     detail::resolve_summand_variable_name_clashes(s, process_parameter_names, generator);
     148             :   }
     149             : 
     150         276 :   for (deadlock_summand& s: proc.deadlock_summands())
     151             :   {
     152          73 :     detail::resolve_summand_variable_name_clashes(s, process_parameter_names, generator);
     153             :   }
     154         203 : }
     155             : 
     156             : } // namespace lps
     157             : 
     158             : } // namespace mcrl2
     159             : 
     160             : #endif // MCRL2_LPS_RESOLVE_NAME_CLASHES_H