LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - replace.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 17 19 89.5 %
Date: 2024-03-08 02:52:28 Functions: 4 4 100.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/modal_formula/replace.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_REPLACE_H
      13             : #define MCRL2_MODAL_FORMULA_REPLACE_H
      14             : 
      15             : #include "mcrl2/lps/replace.h"
      16             : #include "mcrl2/modal_formula/replace_capture_avoiding.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace action_formulas
      22             : {
      23             : 
      24             : //--- start generated action_formulas replace code ---//
      25             : template <typename T, typename Substitution>
      26             : void replace_sort_expressions(T& x,
      27             :                               const Substitution& sigma,
      28             :                               bool innermost,
      29             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      30             :                              )
      31             : {
      32             :   data::detail::make_replace_sort_expressions_builder<action_formulas::sort_expression_builder>(sigma, innermost).update(x);
      33             : }
      34             : 
      35             : template <typename T, typename Substitution>
      36             : T replace_sort_expressions(const T& x,
      37             :                            const Substitution& sigma,
      38             :                            bool innermost,
      39             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      40             :                           )
      41             : {
      42             :   T result;
      43             :   data::detail::make_replace_sort_expressions_builder<action_formulas::sort_expression_builder>(sigma, innermost).apply(result, x);
      44             :   return result;
      45             : }
      46             : 
      47             : template <typename T, typename Substitution>
      48             : void replace_data_expressions(T& x,
      49             :                               const Substitution& sigma,
      50             :                               bool innermost,
      51             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      52             :                              )
      53             : {
      54             :   data::detail::make_replace_data_expressions_builder<action_formulas::data_expression_builder>(sigma, innermost).update(x);
      55             : }
      56             : 
      57             : template <typename T, typename Substitution>
      58             : T replace_data_expressions(const T& x,
      59             :                            const Substitution& sigma,
      60             :                            bool innermost,
      61             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      62             :                           )
      63             : {
      64             :   T result;
      65             :   data::detail::make_replace_data_expressions_builder<action_formulas::data_expression_builder>(sigma, innermost).apply(result, x);
      66             :   return result;
      67             : }
      68             : 
      69             : 
      70             : template <typename T, typename Substitution>
      71             : void replace_variables(T& x,
      72             :                        const Substitution& sigma,
      73             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      74             :                       )
      75             : {
      76             :   core::make_update_apply_builder<action_formulas::data_expression_builder>(sigma).update(x);
      77             : }
      78             : 
      79             : template <typename T, typename Substitution>
      80             : T replace_variables(const T& x,
      81             :                     const Substitution& sigma,
      82             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      83             :                    )
      84             : {
      85             :   T result;
      86             :   core::make_update_apply_builder<action_formulas::data_expression_builder>(sigma).apply(result, x);
      87             :   return result;
      88             : }
      89             : 
      90             : template <typename T, typename Substitution>
      91             : void replace_all_variables(T& x,
      92             :                            const Substitution& sigma,
      93             :                            typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      94             :                           )
      95             : {
      96             :   core::make_update_apply_builder<action_formulas::variable_builder>(sigma).update(x);
      97             : }
      98             : 
      99             : template <typename T, typename Substitution>
     100             : T replace_all_variables(const T& x,
     101             :                         const Substitution& sigma,
     102             :                         typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     103             :                        )
     104             : {
     105             :   T result;
     106             :   core::make_update_apply_builder<action_formulas::variable_builder>(sigma).apply(result, x);
     107             :   return result;
     108             : }
     109             : 
     110             : /// \\brief Applies the substitution sigma to x.
     111             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     112             : template <typename T, typename Substitution>
     113             : void replace_free_variables(T& x,
     114             :                             const Substitution& sigma,
     115             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     116             :                            )
     117             : {
     118             :   assert(data::is_simple_substitution(sigma));
     119             :   data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).update(x);
     120             : }
     121             : 
     122             : /// \\brief Applies the substitution sigma to x.
     123             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     124             : template <typename T, typename Substitution>
     125             : T replace_free_variables(const T& x,
     126             :                          const Substitution& sigma,
     127             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     128             :                         )
     129             : {
     130             :   assert(data::is_simple_substitution(sigma));
     131             :   T result;
     132             :   data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).apply(result, x);
     133             :   return result;
     134             : }
     135             : 
     136             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     137             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     138             : template <typename T, typename Substitution, typename VariableContainer>
     139             : void replace_free_variables(T& x,
     140             :                             const Substitution& sigma,
     141             :                             const VariableContainer& bound_variables,
     142             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     143             :                            )
     144             : {
     145             :   assert(data::is_simple_substitution(sigma));
     146             :   data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
     147             : }
     148             : 
     149             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     150             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     151             : template <typename T, typename Substitution, typename VariableContainer>
     152             : T replace_free_variables(const T& x,
     153             :                          const Substitution& sigma,
     154             :                          const VariableContainer& bound_variables,
     155             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     156             :                         )
     157             : {
     158             :   assert(data::is_simple_substitution(sigma));
     159             :   T result;
     160             :   data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
     161             :   return result;
     162             : }
     163             : //--- end generated action_formulas replace code ---//
     164             : 
     165             : } // namespace action_formulas
     166             : 
     167             : namespace regular_formulas
     168             : {
     169             : 
     170             : //--- start generated regular_formulas replace code ---//
     171             : template <typename T, typename Substitution>
     172             : void replace_sort_expressions(T& x,
     173             :                               const Substitution& sigma,
     174             :                               bool innermost,
     175             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     176             :                              )
     177             : {
     178             :   data::detail::make_replace_sort_expressions_builder<regular_formulas::sort_expression_builder>(sigma, innermost).update(x);
     179             : }
     180             : 
     181             : template <typename T, typename Substitution>
     182             : T replace_sort_expressions(const T& x,
     183             :                            const Substitution& sigma,
     184             :                            bool innermost,
     185             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     186             :                           )
     187             : {
     188             :   T result;
     189             :   data::detail::make_replace_sort_expressions_builder<regular_formulas::sort_expression_builder>(sigma, innermost).apply(result, x);
     190             :   return result;
     191             : }
     192             : 
     193             : template <typename T, typename Substitution>
     194             : void replace_data_expressions(T& x,
     195             :                               const Substitution& sigma,
     196             :                               bool innermost,
     197             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     198             :                              )
     199             : {
     200             :   data::detail::make_replace_data_expressions_builder<regular_formulas::data_expression_builder>(sigma, innermost).update(x);
     201             : }
     202             : 
     203             : template <typename T, typename Substitution>
     204             : T replace_data_expressions(const T& x,
     205             :                            const Substitution& sigma,
     206             :                            bool innermost,
     207             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     208             :                           )
     209             : {
     210             :   T result;
     211             :   data::detail::make_replace_data_expressions_builder<regular_formulas::data_expression_builder>(sigma, innermost).apply(result, x);
     212             :   return result;
     213             : }
     214             : 
     215             : 
     216             : template <typename T, typename Substitution>
     217             : void replace_variables(T& x,
     218             :                        const Substitution& sigma,
     219             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     220             :                       )
     221             : {
     222             :   core::make_update_apply_builder<regular_formulas::data_expression_builder>(sigma).update(x);
     223             : }
     224             : 
     225             : template <typename T, typename Substitution>
     226             : T replace_variables(const T& x,
     227             :                     const Substitution& sigma,
     228             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     229             :                    )
     230             : {
     231             :   T result;
     232             :   core::make_update_apply_builder<regular_formulas::data_expression_builder>(sigma).apply(result, x);
     233             :   return result;
     234             : }
     235             : 
     236             : template <typename T, typename Substitution>
     237             : void replace_all_variables(T& x,
     238             :                            const Substitution& sigma,
     239             :                            typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     240             :                           )
     241             : {
     242             :   core::make_update_apply_builder<regular_formulas::variable_builder>(sigma).update(x);
     243             : }
     244             : 
     245             : template <typename T, typename Substitution>
     246             : T replace_all_variables(const T& x,
     247             :                         const Substitution& sigma,
     248             :                         typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     249             :                        )
     250             : {
     251             :   T result;
     252             :   core::make_update_apply_builder<regular_formulas::variable_builder>(sigma).apply(result, x);
     253             :   return result;
     254             : }
     255             : 
     256             : /// \\brief Applies the substitution sigma to x.
     257             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     258             : template <typename T, typename Substitution>
     259             : void replace_free_variables(T& x,
     260             :                             const Substitution& sigma,
     261             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     262             :                            )
     263             : {
     264             :   assert(data::is_simple_substitution(sigma));
     265             :   data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).update(x);
     266             : }
     267             : 
     268             : /// \\brief Applies the substitution sigma to x.
     269             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     270             : template <typename T, typename Substitution>
     271             : T replace_free_variables(const T& x,
     272             :                          const Substitution& sigma,
     273             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     274             :                         )
     275             : {
     276             :   assert(data::is_simple_substitution(sigma));
     277             :   T result;
     278             :   data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).apply(result, x);
     279             :   return result;
     280             : }
     281             : 
     282             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     283             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     284             : template <typename T, typename Substitution, typename VariableContainer>
     285             : void replace_free_variables(T& x,
     286             :                             const Substitution& sigma,
     287             :                             const VariableContainer& bound_variables,
     288             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     289             :                            )
     290             : {
     291             :   assert(data::is_simple_substitution(sigma));
     292             :   data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
     293             : }
     294             : 
     295             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     296             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     297             : template <typename T, typename Substitution, typename VariableContainer>
     298             : T replace_free_variables(const T& x,
     299             :                          const Substitution& sigma,
     300             :                          const VariableContainer& bound_variables,
     301             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     302             :                         )
     303             : {
     304             :   assert(data::is_simple_substitution(sigma));
     305             :   T result;
     306             :   data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
     307             :   return result;
     308             : }
     309             : //--- end generated regular_formulas replace code ---//
     310             : 
     311             : } // namespace regular_formulas
     312             : 
     313             : namespace state_formulas
     314             : {
     315             : 
     316             : //--- start generated state_formulas replace code ---//
     317             : template <typename T, typename Substitution>
     318             : void replace_sort_expressions(T& x,
     319             :                               const Substitution& sigma,
     320             :                               bool innermost,
     321             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     322             :                              )
     323             : {
     324             :   data::detail::make_replace_sort_expressions_builder<state_formulas::sort_expression_builder>(sigma, innermost).update(x);
     325             : }
     326             : 
     327             : template <typename T, typename Substitution>
     328             : T replace_sort_expressions(const T& x,
     329             :                            const Substitution& sigma,
     330             :                            bool innermost,
     331             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     332             :                           )
     333             : {
     334             :   T result;
     335             :   data::detail::make_replace_sort_expressions_builder<state_formulas::sort_expression_builder>(sigma, innermost).apply(result, x);
     336             :   return result;
     337             : }
     338             : 
     339             : template <typename T, typename Substitution>
     340             : void replace_data_expressions(T& x,
     341             :                               const Substitution& sigma,
     342             :                               bool innermost,
     343             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     344             :                              )
     345             : {
     346             :   data::detail::make_replace_data_expressions_builder<state_formulas::data_expression_builder>(sigma, innermost).update(x);
     347             : }
     348             : 
     349             : template <typename T, typename Substitution>
     350             : T replace_data_expressions(const T& x,
     351             :                            const Substitution& sigma,
     352             :                            bool innermost,
     353             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     354             :                           )
     355             : {
     356             :   T result;
     357             :   data::detail::make_replace_data_expressions_builder<state_formulas::data_expression_builder>(sigma, innermost).apply(result, x);
     358             :   return result;
     359             : }
     360             : 
     361             : 
     362             : template <typename T, typename Substitution>
     363             : void replace_variables(T& x,
     364             :                        const Substitution& sigma,
     365             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     366             :                       )
     367             : {
     368             :   core::make_update_apply_builder<state_formulas::data_expression_builder>(sigma).update(x);
     369             : }
     370             : 
     371             : template <typename T, typename Substitution>
     372             : T replace_variables(const T& x,
     373             :                     const Substitution& sigma,
     374             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     375             :                    )
     376             : {
     377             :   T result;
     378             :   core::make_update_apply_builder<state_formulas::data_expression_builder>(sigma).apply(result, x);
     379             :   return result;
     380             : }
     381             : 
     382             : template <typename T, typename Substitution>
     383             : void replace_all_variables(T& x,
     384             :                            const Substitution& sigma,
     385             :                            typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     386             :                           )
     387             : {
     388             :   core::make_update_apply_builder<state_formulas::variable_builder>(sigma).update(x);
     389             : }
     390             : 
     391             : template <typename T, typename Substitution>
     392             : T replace_all_variables(const T& x,
     393             :                         const Substitution& sigma,
     394             :                         typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     395             :                        )
     396             : {
     397             :   T result;
     398             :   core::make_update_apply_builder<state_formulas::variable_builder>(sigma).apply(result, x);
     399             :   return result;
     400             : }
     401             : 
     402             : /// \\brief Applies the substitution sigma to x.
     403             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     404             : template <typename T, typename Substitution>
     405             : void replace_free_variables(T& x,
     406             :                             const Substitution& sigma,
     407             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     408             :                            )
     409             : {
     410             :   assert(data::is_simple_substitution(sigma));
     411             :   data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).update(x);
     412             : }
     413             : 
     414             : /// \\brief Applies the substitution sigma to x.
     415             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     416             : template <typename T, typename Substitution>
     417             : T replace_free_variables(const T& x,
     418             :                          const Substitution& sigma,
     419             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     420             :                         )
     421             : {
     422             :   assert(data::is_simple_substitution(sigma));
     423             :   T result;
     424             :   data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).apply(result, x);
     425             :   return result;
     426             : }
     427             : 
     428             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     429             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     430             : template <typename T, typename Substitution, typename VariableContainer>
     431             : void replace_free_variables(T& x,
     432             :                             const Substitution& sigma,
     433             :                             const VariableContainer& bound_variables,
     434             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     435             :                            )
     436             : {
     437             :   assert(data::is_simple_substitution(sigma));
     438             :   data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
     439             : }
     440             : 
     441             : /// \\brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     442             : /// \\pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     443             : template <typename T, typename Substitution, typename VariableContainer>
     444             : T replace_free_variables(const T& x,
     445             :                          const Substitution& sigma,
     446             :                          const VariableContainer& bound_variables,
     447             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     448             :                         )
     449             : {
     450             :   assert(data::is_simple_substitution(sigma));
     451             :   T result;
     452             :   data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).apply(result, x, bound_variables);
     453             :   return result;
     454             : }
     455             : //--- end generated state_formulas replace code ---//
     456             : 
     457             : namespace detail
     458             : {
     459             : 
     460             : /// \cond INTERNAL_DOCS
     461             : template <template <class> class Builder, class Substitution>
     462             : struct substitute_state_formulas_builder: public Builder<substitute_state_formulas_builder<Builder, Substitution> >
     463             : {
     464             :   typedef Builder<substitute_state_formulas_builder<Builder, Substitution> > super;
     465             :   using super::enter;
     466             :   using super::leave;
     467             :   using super::update;
     468             :   using super::apply;
     469             : 
     470             :   Substitution sigma;
     471             :   bool innermost;
     472             : 
     473           1 :   substitute_state_formulas_builder(Substitution sigma_, bool innermost_)
     474           1 :     : sigma(sigma_),
     475           1 :       innermost(innermost_)
     476           1 :   {}
     477             : 
     478             :   template <class T>
     479           5 :   void apply(T& result, const state_formula& x)
     480             :   {
     481           5 :     if (innermost)
     482             :     {
     483           5 :       state_formula y;
     484           5 :       super::apply(y, x);
     485           5 :       result = sigma(y);
     486           5 :       return;
     487           5 :     }
     488           0 :     result = sigma(x);
     489             :   }
     490             : };
     491             : 
     492             : template <template <class> class Builder, class Substitution>
     493             : substitute_state_formulas_builder<Builder, Substitution>
     494           1 : make_replace_state_formulas_builder(Substitution sigma, bool innermost)
     495             : {
     496           1 :   return substitute_state_formulas_builder<Builder, Substitution>(sigma, innermost);
     497             : }
     498             : /// \endcond
     499             : 
     500             : } // namespace detail
     501             : 
     502             : template <typename T, typename Substitution>
     503             : void replace_state_formulas(T& x,
     504             :                               Substitution sigma,
     505             :                               bool innermost = true,
     506             :                               typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
     507             :                              )
     508             : {
     509             :   state_formulas::detail::make_replace_state_formulas_builder<state_formulas::state_formula_builder>(sigma, innermost).update(x);
     510             : }
     511             : 
     512             : template <typename T, typename Substitution>
     513           1 : T replace_state_formulas(const T& x,
     514             :                            Substitution sigma,
     515             :                            bool innermost = true,
     516             :                            typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
     517             :                           )
     518             : {
     519           1 :   T result;
     520           1 :   state_formulas::detail::make_replace_state_formulas_builder<state_formulas::state_formula_builder>(sigma, innermost).apply(result, x);
     521           1 :   return result;
     522           0 : }
     523             : 
     524             : } // namespace state_formulas
     525             : 
     526             : } // namespace mcrl2
     527             : 
     528             : #endif // MCRL2_MODAL_FORMULA_REPLACE_H

Generated by: LCOV version 1.14