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
|