LCOV - code coverage report
Current view: top level - lps/include/mcrl2/lps - replace.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 77 79 97.5 %
Date: 2024-03-08 02:52:28 Functions: 19 23 82.6 %
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/replace.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_LPS_REPLACE_H
      13             : #define MCRL2_LPS_REPLACE_H
      14             : 
      15             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      16             : #include "mcrl2/lps/replace_capture_avoiding.h"
      17             : #include "mcrl2/process/replace.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace lps
      23             : {
      24             : 
      25             : namespace detail {
      26             : 
      27             : /// \cond INTERNAL_DOCS
      28             : } // namespace detail
      29             : 
      30             : //--- start generated lps replace code ---//
      31             : template <typename T, typename Substitution>
      32             : void replace_sort_expressions(T& x,
      33             :                               const Substitution& sigma,
      34             :                               bool innermost,
      35             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      36             :                              )
      37             : {
      38             :   data::detail::make_replace_sort_expressions_builder<lps::sort_expression_builder>(sigma, innermost).update(x);
      39             : }
      40             : 
      41             : template <typename T, typename Substitution>
      42             : T replace_sort_expressions(const T& x,
      43             :                            const Substitution& sigma,
      44             :                            bool innermost,
      45             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      46             :                           )
      47             : {
      48             :   T result;
      49             :   data::detail::make_replace_sort_expressions_builder<lps::sort_expression_builder>(sigma, innermost).apply(result, x);
      50             :   return result;
      51             : }
      52             : 
      53             : template <typename T, typename Substitution>
      54             : void replace_data_expressions(T& x,
      55             :                               const Substitution& sigma,
      56             :                               bool innermost,
      57             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      58             :                              )
      59             : {
      60             :   data::detail::make_replace_data_expressions_builder<lps::data_expression_builder>(sigma, innermost).update(x);
      61             : }
      62             : 
      63             : template <typename T, typename Substitution>
      64             : T replace_data_expressions(const T& x,
      65             :                            const Substitution& sigma,
      66             :                            bool innermost,
      67             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      68             :                           )
      69             : {
      70             :   T result;
      71             :   data::detail::make_replace_data_expressions_builder<lps::data_expression_builder>(sigma, innermost).apply(result, x);
      72             :   return result;
      73             : }
      74             : 
      75             : 
      76             : template <typename T, typename Substitution>
      77           1 : void replace_variables(T& x,
      78             :                        const Substitution& sigma,
      79             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      80             :                       )
      81             : {
      82           1 :   core::make_update_apply_builder<lps::data_expression_builder>(sigma).update(x);
      83           1 : }
      84             : 
      85             : template <typename T, typename Substitution>
      86             : T replace_variables(const T& x,
      87             :                     const Substitution& sigma,
      88             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      89             :                    )
      90             : {
      91             :   T result;
      92             :   core::make_update_apply_builder<lps::data_expression_builder>(sigma).apply(result, x);
      93             :   return result;
      94             : }
      95             : 
      96             : template <typename T, typename Substitution>
      97          14 : void replace_all_variables(T& x,
      98             :                            const Substitution& sigma,
      99             :                            typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     100             :                           )
     101             : {
     102          14 :   core::make_update_apply_builder<lps::variable_builder>(sigma).update(x);
     103          14 : }
     104             : 
     105             : template <typename T, typename Substitution>
     106         204 : T replace_all_variables(const T& x,
     107             :                         const Substitution& sigma,
     108             :                         typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     109             :                        )
     110             : {
     111         204 :   T result;
     112         204 :   core::make_update_apply_builder<lps::variable_builder>(sigma).apply(result, x);
     113         204 :   return result;
     114           0 : }
     115             : 
     116             : /// \\brief Applies the substitution sigma to x.
     117             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     118             : template <typename T, typename Substitution>
     119         203 : void replace_free_variables(T& x,
     120             :                             const Substitution& sigma,
     121             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     122             :                            )
     123             : {
     124         203 :   assert(data::is_simple_substitution(sigma));
     125         203 :   data::detail::make_replace_free_variables_builder<lps::data_expression_builder, lps::add_data_variable_builder_binding>(sigma).update(x);
     126         203 : }
     127             : 
     128             : /// \\brief Applies the substitution sigma to x.
     129             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     130             : template <typename T, typename Substitution>
     131         204 : T replace_free_variables(const T& x,
     132             :                          const Substitution& sigma,
     133             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     134             :                         )
     135             : {
     136         204 :   assert(data::is_simple_substitution(sigma));
     137         204 :   T result;
     138         204 :   data::detail::make_replace_free_variables_builder<lps::data_expression_builder, lps::add_data_variable_builder_binding>(sigma).apply(result, x);
     139         204 :   return result;
     140           0 : }
     141             : 
     142             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     143             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     144             : template <typename T, typename Substitution, typename VariableContainer>
     145             : void replace_free_variables(T& x,
     146             :                             const Substitution& sigma,
     147             :                             const VariableContainer& bound_variables,
     148             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     149             :                            )
     150             : {
     151             :   assert(data::is_simple_substitution(sigma));
     152             :   data::detail::make_replace_free_variables_builder<lps::data_expression_builder, lps::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
     153             : }
     154             : 
     155             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     156             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     157             : template <typename T, typename Substitution, typename VariableContainer>
     158             : T replace_free_variables(const T& x,
     159             :                          const Substitution& sigma,
     160             :                          const VariableContainer& bound_variables,
     161             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     162             :                         )
     163             : {
     164             :   assert(data::is_simple_substitution(sigma));
     165             :   T result;
     166             :   data::detail::make_replace_free_variables_builder<lps::data_expression_builder, lps::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
     167             :   return result;
     168             : }
     169             : //--- end generated lps replace code ---//
     170             : 
     171             : namespace detail {
     172             : 
     173             : /// \cond INTERNAL_DOCS
     174             : template <template <class> class Builder, template <template <class> class, class> class Binder, class Substitution>
     175             : struct replace_process_parameter_builder: public Binder<Builder, replace_process_parameter_builder<Builder, Binder, Substitution> >
     176             : {
     177             :   typedef Binder<Builder, replace_process_parameter_builder<Builder, Binder, Substitution> > super;
     178             :   using super::enter;
     179             :   using super::leave;
     180             :   using super::apply;
     181             :   using super::update;
     182             :   using super::is_bound;
     183             :   using super::bound_variables;
     184             :   using super::increase_bind_count;
     185             : 
     186             :   Substitution sigma;
     187             :   std::size_t count; // the bind count
     188             : 
     189          33 :   explicit replace_process_parameter_builder(Substitution sigma_)
     190          33 :     : sigma(sigma_), count(1)
     191          33 :   {}
     192             : 
     193             :   template <typename VariableContainer>
     194             :   replace_process_parameter_builder(Substitution sigma_, const VariableContainer& bound_variables)
     195             :     : sigma(sigma_), count(1)
     196             :   {
     197             :     increase_bind_count(bound_variables);
     198             :   }
     199             : 
     200         755 :   void apply(data::variable& result, const data::variable& x)
     201             :   {
     202         755 :     if (bound_variables().count(x) == count)
     203             :     {
     204         422 :       result = atermpp::down_cast<data::variable>(sigma(x));
     205         422 :       return;
     206             :     }
     207         333 :     result = x;
     208             :   }
     209             : 
     210             :   template <class T>
     211         667 :   void apply(T& result, const data::variable& x)
     212             :   {
     213         667 :     if (bound_variables().count(x) == count)
     214             :     {
     215         405 :       result = sigma(x);
     216         405 :       return;
     217             :     }
     218         262 :     result = static_cast<data::data_expression>(x);
     219             :   }
     220             : 
     221             :   template <class T>
     222         666 :   void apply(T& result, const data::assignment& x)
     223             :   {
     224         666 :     data::variable lhs;
     225         666 :     apply(lhs, x.lhs());
     226         666 :     data::data_expression rhs; 
     227         666 :     apply(rhs, x.rhs());
     228         666 :     data::make_assignment(result, lhs, rhs);
     229         666 :   }
     230             : 
     231          20 :   void update(lps::deadlock_summand& x)
     232             :   {
     233          20 :     count = 1;
     234          20 :     super::update(x);
     235          20 :   }
     236             : 
     237         145 :   void update(lps::action_summand& x)
     238             :   {
     239         145 :     count = 1;
     240         145 :     super::update(x);
     241         145 :     data::assignment_list assignments;
     242         145 :     super::apply(assignments, x.assignments());
     243         145 :     x.assignments() = assignments;
     244         145 :   }
     245             : 
     246          33 :   void update(lps::linear_process& x)
     247             :   {
     248          33 :     super::update(x);
     249          33 :     count = 0;
     250          33 :     data::variable_list process_parameters;
     251          33 :     super::apply(process_parameters, x.process_parameters());
     252          33 :     x.process_parameters() = process_parameters;
     253          33 :   }
     254             : };
     255             : 
     256             : template <template <class> class Builder, template <template <class> class, class> class Binder, class Substitution>
     257             : replace_process_parameter_builder<Builder, Binder, Substitution>
     258          33 : make_replace_process_parameters_builder(Substitution sigma)
     259             : {
     260          33 :   return replace_process_parameter_builder<Builder, Binder, Substitution>(sigma);
     261             : }
     262             : /// \endcond
     263             : 
     264             : } // namespace detail
     265             : 
     266             : /// \brief Applies a substitution to the process parameters of the specification spec.
     267             : template <typename Substitution>
     268          33 : void replace_process_parameters(specification& spec, Substitution sigma)
     269             : {
     270          33 :   lps::detail::make_replace_process_parameters_builder<lps::data_expression_builder, lps::add_data_variable_builder_binding>(sigma).update(spec);
     271          33 : }
     272             : 
     273             : /// \brief Applies a substitution to the process parameters of the specification spec.
     274             : inline
     275          33 : void replace_summand_variables(specification& spec, data::mutable_map_substitution<>& sigma)
     276             : {
     277          33 :   data::set_identifier_generator id_generator;
     278          58 :   for (const data::variable& v: data::substitution_variables(sigma))
     279             :   {
     280          25 :     id_generator.add_identifier(v.name());
     281          33 :   }
     282             : 
     283         178 :   for (action_summand& s: spec.process().action_summands())
     284             :   {
     285         145 :     s.summation_variables() = data::replace_variables(s.summation_variables(), sigma);
     286         145 :     s.condition() = data::replace_variables_capture_avoiding(s.condition(), sigma, id_generator);
     287         145 :     s.multi_action() = lps::replace_variables_capture_avoiding(s.multi_action(), sigma, id_generator);
     288         145 :     s.assignments() = data::replace_variables_capture_avoiding(s.assignments(), sigma, id_generator);
     289             :   }
     290          53 :   for (deadlock_summand& s: spec.process().deadlock_summands())
     291             :   {
     292          20 :     s.summation_variables() = data::replace_variables(s.summation_variables(), sigma);
     293          20 :     s.condition() = data::replace_variables_capture_avoiding(s.condition(), sigma, id_generator);
     294          20 :     lps::replace_variables_capture_avoiding(s.deadlock(), sigma, id_generator);
     295             :   }
     296          33 : }
     297             : 
     298             : } // namespace lps
     299             : 
     300             : } // namespace mcrl2
     301             : 
     302             : #endif // MCRL2_LPS_REPLACE_H

Generated by: LCOV version 1.14