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_capture_avoiding.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_LPS_REPLACE_CAPTURE_AVOIDING_H
13 : #define MCRL2_LPS_REPLACE_CAPTURE_AVOIDING_H
14 :
15 : #include "mcrl2/lps/builder.h"
16 : #include "mcrl2/lps/find.h"
17 : #include "mcrl2/process/replace_capture_avoiding.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace lps {
22 :
23 : namespace detail {
24 :
25 : template <template <class> class Builder, class Derived, class Substitution>
26 : struct add_capture_avoiding_replacement: public process::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution>
27 : {
28 : typedef process::detail::add_capture_avoiding_replacement<Builder, Derived, Substitution> super;
29 : using super::enter;
30 : using super::leave;
31 : using super::apply;
32 : using super::update;
33 : using super::sigma;
34 :
35 1686 : explicit add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater<Substitution>& sigma)
36 1686 : : super(sigma)
37 1686 : { }
38 :
39 : template <typename ActionSummand>
40 1491 : void do_action_summand(ActionSummand& x, const data::variable_list& v)
41 : {
42 1491 : x.summation_variables() = v;
43 1491 : data::data_expression condition;
44 2982 : lps::multi_action multi_action;
45 1491 : data::assignment_list assignments;
46 :
47 1491 : apply(condition, x.condition());
48 1491 : apply(multi_action, x.multi_action());
49 1491 : apply(assignments, x.assignments());
50 :
51 1491 : x.condition() = condition;
52 1491 : x.multi_action() = multi_action;
53 1491 : x.assignments() = assignments;
54 1491 : }
55 :
56 8 : void update(action_summand& x)
57 : {
58 8 : data::variable_list sumvars = x.summation_variables();
59 8 : data::variable_list v1 = sigma.add_fresh_variable_assignments(sumvars);
60 8 : do_action_summand(x, v1);
61 8 : sigma.remove_fresh_variable_assignments(sumvars);
62 8 : }
63 :
64 1483 : void update(stochastic_action_summand& x)
65 : {
66 1483 : data::variable_list sumvars = x.summation_variables();
67 1483 : data::variable_list v1 = sigma.add_fresh_variable_assignments(sumvars);
68 1483 : do_action_summand(x, v1);
69 :
70 1483 : lps::stochastic_distribution dist;
71 1483 : apply(dist, x.distribution(), x.assignments());
72 1483 : x.distribution() = dist;
73 1483 : sigma.remove_fresh_variable_assignments(sumvars);
74 1483 : }
75 :
76 0 : void update(deadlock_summand& x)
77 : {
78 0 : data::variable_list sumvars = x.summation_variables();
79 0 : data::variable_list v1 = sigma.add_fresh_variable_assignments(sumvars);
80 0 : x.summation_variables() = v1;
81 :
82 0 : data::data_expression condition;
83 0 : apply(condition, x.condition());
84 0 : x.condition() = condition;
85 :
86 0 : update(x.deadlock());
87 0 : sigma.remove_fresh_variable_assignments(sumvars);
88 0 : }
89 :
90 : template <typename LinearProcess>
91 1 : void do_linear_process(LinearProcess& x)
92 : {
93 1 : data::variable_list process_params = x.process_parameters();
94 1 : data::variable_list v1 = sigma.add_fresh_variable_assignments(process_params);
95 1 : x.process_parameters() = v1;
96 1 : update(x.action_summands());
97 1 : update(x.deadlock_summands());
98 1 : sigma.remove_fresh_variable_assignments(process_params);
99 1 : }
100 :
101 : void update(linear_process& x)
102 : {
103 : do_linear_process(x);
104 : }
105 :
106 1 : void update(stochastic_linear_process& x)
107 : {
108 1 : do_linear_process(x);
109 1 : }
110 :
111 : template <typename Specification>
112 : void do_specification(Specification& x)
113 : {
114 : data::variable_list global_vars = x.global_variables();
115 : data::variable_list v1 = sigma.add_fresh_variable_assignments(global_vars);
116 : x.global_variables() = std::set<data::variable>(v1.begin(), v1.end());
117 :
118 : typename Specification::process_type process;
119 : process::action_label_list action_labels;
120 : typename Specification::initial_process_type initial_process;
121 :
122 : apply(process, x.process());
123 : apply(action_labels, x.action_labels());
124 : apply(initial_process, x.initial_process());
125 : x.process() = process;
126 : x.action_labels() = action_labels;
127 : x.initial_process() = initial_process;
128 :
129 : sigma.remove_fresh_variable_assignments(global_vars);
130 : }
131 :
132 : void operator()(specification& x)
133 : {
134 : do_specification(x);
135 : }
136 :
137 : void operator()(stochastic_specification& x)
138 : {
139 : do_specification(x);
140 : }
141 :
142 : template<class T>
143 : void apply(T& /* result */, const stochastic_distribution& /* x */)
144 : {
145 : assert(false); // This function should never be called. If a stochastic distribution is
146 : // changed, the associated parameter list should be changed too.
147 : }
148 :
149 : /// In the code below, it is essential that the assignments are also updated. They are passed by reference and changed in place.
150 : template<class T>
151 1483 : void apply(T& result, const stochastic_distribution& x, data::assignment_list& assignments)
152 : {
153 1483 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
154 :
155 1483 : data::data_expression dist;
156 1483 : apply(dist, x.distribution());
157 1483 : data::assignment_list aux_assignments;
158 1483 : apply(aux_assignments, assignments);
159 1483 : assignments = aux_assignments;
160 1483 : result = stochastic_distribution(v1, dist);
161 1483 : sigma.remove_fresh_variable_assignments(x.variables());
162 1483 : }
163 :
164 : /// In the code below, it is essential that the assignments are also updated. They are passed by reference and changed in place.
165 : template<class T>
166 0 : void apply(T& result, const stochastic_distribution& x, data::data_expression_list& pars)
167 : {
168 0 : data::variable_list v1 = sigma.add_fresh_variable_assignments(x.variables());
169 :
170 0 : data::data_expression dist;
171 0 : apply(dist, x.distribution());
172 0 : data::data_expression_list aux_pars;
173 0 : apply(aux_pars, pars);
174 0 : pars = aux_pars;
175 0 : result = stochastic_distribution(v1, dist);
176 0 : sigma.remove_fresh_variable_assignments(x.variables());
177 0 : }
178 : };
179 :
180 : } // namespace detail
181 :
182 : //--- start generated lps replace_capture_avoiding code ---//
183 : /// \\brief Applies sigma as a capture avoiding substitution to x.
184 : /// \\param x The object to which the subsitution is applied.
185 : /// \\param sigma A substitution.
186 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
187 : template <typename T, typename Substitution>
188 1513 : void replace_variables_capture_avoiding(T& x,
189 : Substitution& sigma,
190 : data::set_identifier_generator& id_generator,
191 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
192 : )
193 : {
194 1513 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
195 1513 : data::detail::apply_replace_capture_avoiding_variables_builder<lps::data_expression_builder, lps::detail::add_capture_avoiding_replacement>(sigma1).update(x);
196 1513 : }
197 :
198 : /// \\brief Applies sigma as a capture avoiding substitution to x.
199 : /// \\param x The object to which the substiution is applied.
200 : /// \\param sigma A substitution.
201 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
202 : template <typename T, typename Substitution>
203 164 : T replace_variables_capture_avoiding(const T& x,
204 : Substitution& sigma,
205 : data::set_identifier_generator& id_generator,
206 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
207 : )
208 : {
209 164 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
210 328 : T result;
211 164 : data::detail::apply_replace_capture_avoiding_variables_builder<lps::data_expression_builder, lps::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x);
212 328 : return result;
213 164 : }
214 :
215 : /// \\brief Applies sigma as a capture avoiding substitution to x.
216 : /// \\param x The object to which the subsitution is applied.
217 : /// \\param sigma A substitution.
218 : template <typename T, typename Substitution>
219 1491 : void replace_variables_capture_avoiding(T& x,
220 : Substitution& sigma,
221 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
222 : )
223 : {
224 1491 : data::set_identifier_generator id_generator;
225 1491 : id_generator.add_identifiers(lps::find_identifiers(x));
226 3938 : for (const data::variable& v: substitution_variables(sigma))
227 : {
228 2447 : id_generator.add_identifier(v.name());
229 : }
230 1491 : lps::replace_variables_capture_avoiding(x, sigma, id_generator);
231 1491 : }
232 :
233 : /// \\brief Applies sigma as a capture avoiding substitution to x.
234 : /// \\param x The object to which the substiution is applied.
235 : /// \\param sigma A substitution.
236 : template <typename T, typename Substitution>
237 : T replace_variables_capture_avoiding(const T& x,
238 : Substitution& sigma,
239 : typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
240 : )
241 : {
242 : data::set_identifier_generator id_generator;
243 : id_generator.add_identifiers(lps::find_identifiers(x));
244 : for (const data::variable& v: substitution_variables(sigma))
245 : {
246 : id_generator.add_identifier(v.name());
247 : }
248 : return lps::replace_variables_capture_avoiding(x, sigma, id_generator);
249 : }
250 : //--- end generated lps replace_capture_avoiding code ---//
251 :
252 : /// \\brief Applies sigma as a capture avoiding substitution to x with x a distribution..
253 : /// \\details The capture avoiding substitution must also be applied to the expression to which the distribution is applied.
254 : /// \\param x The object to which the substiution is applied.
255 : /// \\param pars The parameter list to which the distribution is applied.
256 : /// \\param sigma A substitution.
257 : /// \\param id_generator An identifier generator that generates names that do not appear in x and sigma
258 : template <typename Substitution>
259 0 : stochastic_distribution replace_variables_capture_avoiding(
260 : const stochastic_distribution& x,
261 : data::data_expression_list& pars,
262 : Substitution& sigma,
263 : data::set_identifier_generator& id_generator
264 : )
265 : {
266 0 : data::detail::capture_avoiding_substitution_updater<Substitution> sigma1(sigma, id_generator);
267 0 : stochastic_distribution result;
268 0 : data::detail::apply_replace_capture_avoiding_variables_builder<lps::data_expression_builder, lps::detail::add_capture_avoiding_replacement>(sigma1).apply(result, x, pars);
269 0 : return result;
270 0 : }
271 :
272 : /// \\brief Applies sigma as a capture avoiding substitution to a stochastic_distribution and a list of parameters.
273 : /// \\param x The object to which the substiution is applied.
274 : /// \\param pars The parameters of which the variables are bound. This list is changed if necessary.
275 : /// \\param sigma A substitution.
276 : template <typename Substitution>
277 : stochastic_distribution replace_variables_capture_avoiding(
278 : const stochastic_distribution& x,
279 : data::data_expression_list& pars,
280 : Substitution& sigma
281 : )
282 : {
283 : data::set_identifier_generator id_generator;
284 : id_generator.add_identifiers(lps::find_identifiers(x));
285 : for (const data::variable& v: substitution_variables(sigma))
286 : {
287 : id_generator.add_identifier(v.name());
288 : }
289 : return lps::replace_variables_capture_avoiding(x, pars, sigma, id_generator);
290 : }
291 :
292 :
293 : } // namespace lps
294 :
295 : } // namespace mcrl2
296 :
297 : #endif // MCRL2_LPS_REPLACE_CAPTURE_AVOIDING_H
|
