Line data Source code
1 : // Author(s): Frank Stappers, Jeroen Keiren, Thomas Neele
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 :
10 : /** \file lpsparunfoldlib.cpp
11 : *
12 : * \brief This file contains the code for the tool lpsparunfold that allows to replace
13 : * complex data types by simpler ones.
14 : */
15 :
16 : #include <iterator>
17 : #include "mcrl2/lps/lpsparunfoldlib.h"
18 : #include "mcrl2/lps/replace.h"
19 :
20 : using namespace mcrl2;
21 : using namespace mcrl2::core;
22 : using namespace mcrl2::data;
23 : using namespace mcrl2::log;
24 : using mcrl2::lps::lpsparunfold;
25 :
26 : /* Remarks
27 : - replace on vectors does not work
28 : - vector pretty print does not work
29 : - alias::name() [basic_sort] results in a basic sort, differs form basic_sort::name() [string]
30 : */
31 :
32 : namespace mcrl2::lps::detail
33 : {
34 :
35 5 : unfold_cache_element& unfold_data_manager::get_cache_element(const data::sort_expression& sort)
36 : {
37 5 : assert(sort != data::sort_expression());
38 :
39 5 : std::map< data::sort_expression, unfold_cache_element >::iterator ce = m_cache.find(sort);
40 5 : if(ce == m_cache.end())
41 : {
42 : /* Not using cache */
43 1 : unfold_cache_element& new_cache_element = m_cache[sort];
44 : /* Alg */
45 : /* 1 */
46 1 : new_cache_element.fresh_basic_sort = generate_fresh_basic_sort(sort);
47 1 : m_dataspec.add_sort(new_cache_element.fresh_basic_sort );
48 :
49 : /* 2 */
50 1 : determine_affected_constructors(sort);
51 :
52 : // If there are no constructors, there is nothing to be done.
53 1 : if (!new_cache_element.affected_constructors.empty())
54 : {
55 : /* 4 */
56 1 : create_new_constructors(sort);
57 : /* 6 */
58 1 : create_case_function(sort, sort);
59 : /* 7 */
60 1 : create_determine_function(sort);
61 : /* 8-12 */
62 1 : create_projection_functions(sort);
63 : }
64 1 : return new_cache_element;
65 : }
66 : else
67 : {
68 : /* Using cache */
69 4 : mCRL2log(log::verbose) << "Update using cache for sort: \"" << data::pp(sort) << "\"..." << std::endl;
70 4 : return ce->second;
71 : }
72 : }
73 :
74 1 : data::basic_sort unfold_data_manager::generate_fresh_basic_sort(const data::sort_expression& sort)
75 : {
76 : //Generate a fresh Basic Sort
77 1 : std::string hint("S");
78 1 : if(data::is_basic_sort(sort))
79 : {
80 1 : hint = atermpp::down_cast<basic_sort>(sort).name();
81 : }
82 0 : else if(data::is_container_sort(sort))
83 : {
84 0 : hint = filter_illegal_characters(data::pp(sort));
85 : }
86 :
87 1 : const data::basic_sort result(m_identifier_generator(hint));
88 1 : mCRL2log(log::verbose) << "Generated fresh sort \"" << data::pp(result) << "\" for \"" << data::pp(sort) << "\"" << std::endl;
89 2 : return result;
90 1 : }
91 :
92 6 : core::identifier_string unfold_data_manager::generate_fresh_function_symbol_name(const std::string& str)
93 : {
94 : //Generate a fresh name for a constructor of mapping
95 12 : const core::identifier_string result(m_identifier_generator(filter_illegal_characters(str)));
96 6 : mCRL2log(debug) << "Generated a fresh function symbol name: " << result << std::endl;
97 6 : return result;
98 0 : }
99 :
100 3 : data::variable unfold_data_manager::generate_fresh_variable(std::string str, const sort_expression& sort)
101 : {
102 6 : return data::variable(m_identifier_generator(str.append("_pp")), sort);
103 : }
104 :
105 1 : void unfold_data_manager::determine_affected_constructors(const data::sort_expression& sort)
106 : {
107 1 : unfold_cache_element& new_cache_element = m_cache[sort];
108 1 : assert(new_cache_element.affected_constructors.empty());
109 :
110 1 : new_cache_element.affected_constructors = m_dataspec.constructors(sort);
111 :
112 1 : mCRL2log(debug) << "constructors of unfolded sort:\t";
113 1 : mCRL2log(log::verbose) << "" << sort << " has " << new_cache_element.affected_constructors.size() << " constructor function(s)" << std::endl;
114 :
115 1 : if(log::mCRL2logEnabled(debug))
116 : {
117 0 : for (const function_symbol& f : new_cache_element.affected_constructors)
118 : {
119 0 : mCRL2log(debug) << "\t" << f << std::endl;
120 : }
121 : }
122 1 : }
123 :
124 1 : void unfold_data_manager::create_new_constructors(const data::sort_expression& sort)
125 : {
126 1 : unfold_cache_element& new_cache_element = m_cache[sort];
127 1 : assert(new_cache_element.new_constructors.empty());
128 :
129 3 : for (const function_symbol& func: new_cache_element.affected_constructors)
130 : {
131 2 : std::string prefix = "c_";
132 2 : prefix.append(func.name());
133 0 : const data::function_symbol f(generate_fresh_function_symbol_name(prefix),
134 2 : new_cache_element.fresh_basic_sort);
135 2 : new_cache_element.new_constructors.push_back(f);
136 2 : m_dataspec.add_constructor(f);
137 2 : mCRL2log(debug) << "\t" << f << std::endl;
138 2 : }
139 1 : mCRL2log(debug) << "- Created " << new_cache_element.new_constructors.size() << " fresh \" c_ \" constructor(s)" << std::endl;
140 1 : }
141 :
142 4 : data::function_symbol unfold_data_manager::create_case_function(const sort_expression& det_sort, const sort_expression& output_sort)
143 : {
144 4 : unfold_cache_element& new_cache_element = m_cache[det_sort];
145 : // Generate new function symbol that is used for all case functions related
146 : // to unfolding new_cache_element.fresh_basic_sort.
147 4 : if (new_cache_element.case_function_name == core::identifier_string())
148 : {
149 1 : std::string str = "C_";
150 1 : str.append(new_cache_element.fresh_basic_sort.name());
151 : new_cache_element.case_function_name =
152 1 : generate_fresh_function_symbol_name(str);
153 1 : }
154 :
155 : // Check if the function symbol was already in the cache; if not, create and add it
156 : std::map<mcrl2::data::sort_expression, mcrl2::data::function_symbol>::const_iterator
157 4 : case_function_it = new_cache_element.case_functions.find(output_sort);
158 4 : if(case_function_it == new_cache_element.case_functions.end())
159 : {
160 : // all except first argument are the sort of the unfolded type.
161 3 : data::sort_expression_vector fsl(new_cache_element.affected_constructors.size() + 1, output_sort);
162 3 : fsl[0] = new_cache_element.fresh_basic_sort ;
163 :
164 3 : data::function_symbol fs(new_cache_element.case_function_name,
165 3 : data::function_sort(fsl, output_sort));
166 :
167 3 : mCRL2log(debug) << "- Created C map: " << fs << std::endl;
168 3 : new_cache_element.case_functions[output_sort] = fs;
169 3 : m_dataspec.add_mapping(fs);
170 :
171 : // generate and add equations.
172 3 : generate_case_function_equations(det_sort, fs);
173 3 : return fs;
174 3 : }
175 : else
176 : {
177 1 : return case_function_it->second;
178 : }
179 : }
180 :
181 1 : void unfold_data_manager::create_determine_function(const data::sort_expression& sort)
182 : {
183 1 : unfold_cache_element& new_cache_element = m_cache[sort];
184 1 : std::string str = "Det_";
185 1 : str.append(std::string(new_cache_element.fresh_basic_sort.name()));
186 : new_cache_element.determine_function =
187 2 : data::function_symbol(generate_fresh_function_symbol_name(str),
188 2 : data::make_function_sort_(sort,
189 1 : new_cache_element.fresh_basic_sort ));
190 1 : mCRL2log(debug) << "\t" << new_cache_element.determine_function << std::endl;
191 1 : m_dataspec.add_mapping(new_cache_element.determine_function);
192 :
193 1 : generate_determine_function_equations(sort);
194 1 : }
195 :
196 1 : void unfold_data_manager::create_projection_functions(const data::sort_expression& sort)
197 : {
198 1 : unfold_cache_element& new_cache_element = m_cache[sort];
199 1 : std::string str = "pi_";
200 1 : str.append(std::string(new_cache_element.fresh_basic_sort.name()));
201 :
202 3 : for (const function_symbol& f: new_cache_element.affected_constructors)
203 : {
204 2 : if (is_function_sort(f.sort()))
205 : {
206 1 : const function_sort fs = atermpp::down_cast<function_sort>(f.sort());
207 3 : for (const sort_expression& argument_sort: fs.domain())
208 : {
209 4 : const data::function_symbol map(generate_fresh_function_symbol_name(str),
210 2 : data::make_function_sort_(sort,
211 2 : argument_sort));
212 2 : m_dataspec.add_mapping(map);
213 2 : new_cache_element.projection_functions.push_back(map);
214 2 : }
215 1 : }
216 : }
217 :
218 1 : if(mCRL2logEnabled(debug))
219 : {
220 0 : for (const function_symbol& f : new_cache_element.projection_functions)
221 : {
222 0 : mCRL2log(debug) << "\t" << f << std::endl;
223 : }
224 : }
225 :
226 1 : generate_projection_function_equations(sort);
227 1 : }
228 :
229 1 : void unfold_data_manager::generate_projection_function_equations(const data::sort_expression& sort)
230 : {
231 1 : unfold_cache_element& new_cache_element = m_cache[sort];
232 : // Add projection functions for the arguments of the original constructors.
233 1 : function_symbol_vector::const_iterator pi_it = new_cache_element.projection_functions.begin();
234 3 : for (const function_symbol& f : new_cache_element.affected_constructors)
235 : {
236 2 : const variable_vector f_arguments(m_data_equation_argument_generator.arguments(f));
237 2 : const variable_list f_arguments_list(f_arguments.begin(), f_arguments.end());
238 :
239 4 : for(const variable& arg: f_arguments)
240 : {
241 2 : const application lhs(*pi_it, application(f, f_arguments_list));
242 2 : m_dataspec.add_equation(data_equation(f_arguments_list, lhs, arg));
243 :
244 : // For the same projection function, generate right hand sides with default
245 : // values if the projection function is applied to an expression with a
246 : // constructor that it was not intended for.
247 6 : for (const function_symbol& g: new_cache_element.affected_constructors)
248 : {
249 4 : if (f != g)
250 : {
251 : const variable_vector g_arguments(
252 2 : m_data_equation_argument_generator.arguments(g));
253 2 : const variable_list g_arguments_list(g_arguments.begin(), g_arguments.end());
254 2 : application lhs;
255 2 : if (g_arguments.empty())
256 : {
257 2 : lhs = application(*pi_it, g);
258 : }
259 : else
260 : {
261 0 : lhs = application(
262 0 : *pi_it, application(g, g_arguments_list));
263 : }
264 : try
265 : {
266 2 : const data_expression rhs = m_representative_generator(lhs.sort());
267 2 : m_dataspec.add_equation(data_equation(g_arguments_list, lhs, rhs));
268 2 : }
269 0 : catch (runtime_error& e)
270 : {
271 0 : mCRL2log(debug) << "Failed to generate equation " << data::pp(lhs)
272 : << "= ... as no default term of sort "
273 0 : << data::pp(lhs.sort()) << " could be generated.\n"
274 0 : << e.what() << "\n";
275 0 : }
276 2 : }
277 : }
278 :
279 : // If so desired, add distribution of pi over if and case functions
280 : // pi(if(b,x,y))=if(b,pi(x),pi(y));
281 : // pi(C(e,x1,x2,...))=C(e,pi(x1),pi(x2),...);
282 2 : create_distribution_law_over_case(sort, *pi_it, data::if_(sort));
283 2 : create_distribution_law_over_case(sort, *pi_it, new_cache_element.case_functions[sort]);
284 :
285 2 : ++pi_it;
286 2 : }
287 2 : }
288 1 : }
289 :
290 : // Add equation for f(C(e, d_1, ..., d_n)) = C(e, f(d_1), ..., f(d_n))
291 : // note: the case_function parameter must be copied; passing by reference
292 : // may lead to crashes if the argument is an element of
293 : // new_cache_element.case_functions if a new case function is introduced.
294 6 : void unfold_data_manager::create_distribution_law_over_case(
295 : const data::sort_expression& sort,
296 : const data::function_symbol& f,
297 : const data::function_symbol case_function)
298 : {
299 6 : assert(case_function.sort().target_sort() == atermpp::down_cast<function_sort>(f.sort()).domain().front());
300 :
301 : // C(e, d_1, ..., d_n)
302 6 : variable_vector lhs_args = m_data_equation_argument_generator.arguments(case_function);
303 6 : application lhs(f, application(case_function, lhs_args));
304 :
305 : // Construct rhs arguments e, f(d_1), ..., f(d_n)
306 6 : data_expression_vector rhs_args;
307 6 : variable_vector::const_iterator args = lhs_args.begin();
308 24 : for (variable_vector::const_iterator i = lhs_args.begin(); i != lhs_args.end(); ++i)
309 : {
310 18 : if(i == lhs_args.begin())
311 : {
312 6 : rhs_args.push_back(*args);
313 : }
314 : else
315 : {
316 12 : rhs_args.emplace_back(application(f, *i));
317 : }
318 : }
319 :
320 : // Determine the new case function or if function symbol.
321 6 : data::function_symbol new_case_function;
322 6 : if(data::is_if_function_symbol(case_function))
323 : {
324 3 : new_case_function = data::if_(f.sort().target_sort());
325 : }
326 : else
327 : {
328 3 : new_case_function = create_case_function(sort, f.sort().target_sort());
329 : }
330 :
331 6 : data::application rhs(new_case_function , rhs_args);
332 6 : data::data_equation result(lhs_args, lhs, rhs);
333 6 : m_dataspec.add_equation(result);
334 :
335 6 : mCRL2log(log::verbose) << "- Added distribution law for \"" << data::pp(f) << "\" over \"" << data::pp(case_function) << "\": " << data::pp(result) << std::endl;
336 6 : }
337 :
338 3 : void unfold_data_manager::generate_case_function_equations(const data::sort_expression& sort, const data::function_symbol& case_function)
339 : {
340 3 : mCRL2log(log::verbose) << "- Generating case function equations for:\t" << data::pp(case_function) << ": " << data::pp(case_function.sort()) << "" << std::endl;
341 :
342 3 : unfold_cache_element& new_cache_element = m_cache[sort];
343 3 : assert(atermpp::down_cast<function_sort>(case_function.sort()).domain().size() == new_cache_element.new_constructors.size() + 1);
344 : /* Generate variable identifier string for projection */
345 3 : const variable_vector vars = m_data_equation_argument_generator.arguments(case_function);
346 3 : const variable_list used_vars(++vars.begin(), vars.end()); // all but the first parameter are used in the data equation.
347 :
348 : // We generate one equation for each of the constructors of the new sort,
349 : // projecting out the corresponding argument.
350 : // C(c_i, d_1,...,d_(i-1), d_i, d_(i+1), ..., d_n) = d_i;
351 3 : data_expression_vector sub_args(vars.begin(), vars.end());
352 : // vars_it represents d_i above.
353 3 : variable_vector::const_iterator vars_it = vars.begin();
354 3 : ++vars_it; // first variable to be skipped.
355 :
356 9 : for(data::function_symbol new_constructor: new_cache_element.new_constructors)
357 : {
358 6 : sub_args[0] = new_constructor; // set c_i
359 6 : const application lhs(case_function , sub_args);
360 6 : m_dataspec.add_equation(data_equation(used_vars, lhs, *vars_it));
361 6 : ++vars_it;
362 6 : }
363 :
364 : // Add an equation that removes a case function if all (except the first)
365 : // argument are the same.
366 : // C(x, d_n, ...., d_n) = d_n
367 3 : data_expression_vector eq_args(new_cache_element.new_constructors.size() + 1, vars.back());
368 3 : eq_args[0] = vars.front();
369 3 : const application lhs(case_function , eq_args);
370 9 : m_dataspec.add_equation(data_equation(data::variable_list({vars.front(), vars.back()}), lhs, vars.back()));
371 :
372 3 : if (m_dataspec.equal_sorts(case_function.sort().target_sort(), vars.front().sort()))
373 : {
374 : // Add an equation that rewrites to the first argument if the remainder are the corresponding constructors
375 : // C(x, c_1, ..., c_n) = x
376 3 : data_expression_vector cs_args{vars.front()};
377 3 : for (const function_symbol& cs: new_cache_element.new_constructors)
378 : {
379 2 : cs_args.push_back(cs);
380 : }
381 2 : m_dataspec.add_equation(data_equation(data::variable_list({vars.front()}), application(case_function, cs_args), vars.front()));
382 1 : }
383 :
384 : // If the case function maps to the Booleans, we can replace it by a disjunction.
385 : // Note: this may make the data specification inconsistent.
386 3 : if(m_possibly_inconsistent && sort_bool::is_bool(case_function.sort().target_sort()))
387 : {
388 : // C(x, d_1, ..., d_n) = (d_1 && x == c_1) || (c_2 && x == c_2) || .... (d_n && x == c_n)
389 0 : const data::variable_list args(vars.begin(), vars.end());
390 0 : const application lhs(case_function, args);
391 :
392 0 : data_expression_vector disjuncts;
393 0 : vars_it = vars.begin();
394 0 : const variable det_var = *vars_it++;
395 0 : for(const function_symbol& constructor: new_cache_element.new_constructors)
396 : {
397 0 : if(vars_it == vars.end())
398 : {
399 0 : throw mcrl2::runtime_error("The number of variables and the number of constructors differs.");
400 : }
401 0 : disjuncts.push_back(
402 0 : sort_bool::and_(*vars_it++, equal_to(det_var, constructor)));
403 : }
404 :
405 0 : m_dataspec.add_equation(data_equation(args, lhs, lazy::join_or(disjuncts.begin(), disjuncts.end())));
406 :
407 : // We also need to add rules for equality on the new sort.
408 0 : for(const function_symbol& left: new_cache_element.new_constructors)
409 : {
410 0 : for(const function_symbol& right: new_cache_element.new_constructors)
411 : {
412 0 : if (left != right)
413 : {
414 0 : const application lhs = data::equal_to(left, right);
415 0 : const data_expression rhs = data::false_();
416 0 : m_dataspec.add_equation(data_equation(lhs, rhs));
417 0 : }
418 : }
419 : }
420 0 : }
421 3 : }
422 :
423 1 : void unfold_data_manager::generate_determine_function_equations(const data::sort_expression& sort)
424 : {
425 1 : unfold_cache_element& new_cache_element = m_cache[sort];
426 1 : function_symbol_vector::const_iterator constructor_it = new_cache_element.new_constructors.begin();
427 3 : for (const function_symbol& f: new_cache_element.affected_constructors)
428 : {
429 2 : assert(constructor_it != new_cache_element.new_constructors.end());
430 : /* Creating an equation for the detector function */
431 2 : const variable_vector function_arguments = m_data_equation_argument_generator.arguments(f);
432 2 : if(function_arguments.empty())
433 : {
434 1 : m_dataspec.add_equation(data_equation(
435 2 : application(new_cache_element.determine_function, f),
436 1 : *constructor_it));
437 : }
438 : else
439 : {
440 1 : const variable_list args(function_arguments.begin(), function_arguments.end());
441 1 : m_dataspec.add_equation(data_equation(
442 : args,
443 2 : application(new_cache_element.determine_function,
444 2 : application(f,args)),
445 1 : *constructor_it));
446 1 : }
447 2 : ++constructor_it;
448 2 : }
449 :
450 : /* Add additional distribution laws for Det over if and case functions
451 : Det(if(b,x,y))=if(b,Det(x),Det(y));
452 : Det(C(e,x1,x2,...))=C(e,Det(x1),Det(x2),...);
453 : */
454 1 : create_distribution_law_over_case(sort, new_cache_element.determine_function, data::if_(sort));
455 1 : create_distribution_law_over_case(sort, new_cache_element.determine_function, new_cache_element.case_functions[sort]);
456 1 : }
457 :
458 : } // namespace mcrl2::lps::detail
459 :
460 :
461 : /// \brief Constructor
462 1 : lpsparunfold::lpsparunfold(lps::stochastic_specification& spec,
463 : std::map< data::sort_expression , unfold_cache_element >& cache,
464 : bool alt_case_placement,
465 : bool possibly_inconsistent,
466 1 : bool unfold_pattern_matching)
467 : : lps::detail::lps_algorithm<lps::stochastic_specification>(spec),
468 1 : m_run_before(false),
469 1 : m_datamgr(cache, spec.data(), possibly_inconsistent),
470 1 : m_pattern_unfolder(m_datamgr),
471 1 : m_alt_case_placement(alt_case_placement),
472 2 : m_unfold_pattern_matching(unfold_pattern_matching)
473 : {
474 1 : m_datamgr.add_used_identifiers(lps::find_identifiers(spec));
475 1 : m_datamgr.add_used_identifiers(data::find_identifiers(spec.data()));
476 5 : for (const function_symbol& f : spec.data().constructors())
477 : {
478 4 : m_datamgr.add_used_identifier(f.name());
479 : }
480 27 : for (const function_symbol& f : spec.data().mappings())
481 : {
482 26 : m_datamgr.add_used_identifier(f.name());
483 : }
484 1 : }
485 :
486 1 : void lpsparunfold::unfold_summands(lps::stochastic_action_summand_vector& summands)
487 : {
488 2 : for (lps::stochastic_action_summand& summand: summands)
489 : {
490 1 : data::assignment_vector new_assignments;
491 2 : for (const data::assignment& k: summand.assignments())
492 : {
493 1 : if (k.lhs() == m_unfold_parameter)
494 : {
495 1 : const data::data_expression_vector new_rhs = unfold_constructor(k.rhs());
496 1 : const data::assignment_vector injected_assignments = data::make_assignment_vector(m_injected_parameters, new_rhs);
497 1 : new_assignments.insert(new_assignments.end(), injected_assignments.begin(), injected_assignments.end());
498 1 : }
499 : else
500 : {
501 0 : new_assignments.push_back(k);
502 : }
503 : }
504 1 : summand.assignments() = data::assignment_list(new_assignments.begin(), new_assignments.end());
505 1 : }
506 1 : }
507 :
508 0 : lpsparunfold::case_func_replacement lpsparunfold::parameter_case_function()
509 : {
510 0 : const unfold_cache_element& new_cache_element = m_datamgr.get_cache_element(m_unfold_parameter.sort());
511 0 : data_expression_vector dev;
512 :
513 0 : auto new_pars_it = m_injected_parameters.cbegin();
514 0 : ++new_pars_it;
515 :
516 0 : for (const data::function_symbol& constr: new_cache_element.affected_constructors )
517 : {
518 0 : data::data_expression case_func_arg = constr;
519 :
520 0 : if (is_function_sort(constr.sort()))
521 : {
522 0 : sort_expression_list dom = function_sort(constr.sort()).domain();
523 0 : data_expression_vector arg;
524 :
525 0 : for (const data::sort_expression& arg_sort: dom)
526 : {
527 0 : if (new_pars_it->sort() != arg_sort)
528 : {
529 0 : throw runtime_error("Unexpected new parameter encountered, maybe they were not sorted well.");
530 : }
531 0 : arg.push_back(*new_pars_it++);
532 : }
533 0 : case_func_arg = data::application(constr, arg);
534 0 : }
535 :
536 0 : dev.push_back(case_func_arg);
537 0 : }
538 :
539 0 : return std::make_tuple(m_unfold_parameter, new_cache_element.case_functions, m_injected_parameters[0], dev);
540 :
541 0 : }
542 :
543 1 : void lpsparunfold::update_linear_process(std::size_t parameter_at_index)
544 : {
545 : /* Get process parameters from lps */
546 1 : const data::variable_list& process_parameters = m_spec.process().process_parameters();
547 :
548 : /* Iterator pointing to the parameter that needs to be unfolded */
549 : data::variable_list::const_iterator unfold_parameter_it =
550 1 : process_parameters.begin();
551 1 : std::advance(unfold_parameter_it, parameter_at_index);
552 :
553 1 : mCRL2log(log::verbose) << "Updating LPS..." << std::endl;
554 :
555 : /* Create new process parameters */
556 1 : data::variable_vector new_process_parameters;
557 :
558 : /* Expand unfold_parameter */
559 1 : mCRL2log(log::verbose) << " Unfolding parameter " << unfold_parameter_it->name() << " at index " << parameter_at_index << "..." << std::endl;
560 :
561 : /* First copy the initial part of the parameters */
562 2 : new_process_parameters.insert(new_process_parameters.end(),
563 1 : process_parameters.begin(),
564 : unfold_parameter_it);
565 :
566 1 : const unfold_cache_element& new_cache_element = m_datamgr.get_cache_element(m_unfold_parameter.sort());
567 1 : const data::variable param = m_datamgr.generate_fresh_variable(m_unfold_parameter.name(), new_cache_element.fresh_basic_sort );
568 1 : m_injected_parameters.push_back(param);
569 :
570 1 : mCRL2log(log::verbose)
571 0 : << "- Created process parameter " << data::pp(m_injected_parameters.back())
572 0 : << " of type " << data::pp(new_cache_element.fresh_basic_sort ) << "" << std::endl;
573 :
574 3 : for (const data::function_symbol& constructor: new_cache_element.affected_constructors)
575 : {
576 2 : if (is_function_sort(constructor.sort()))
577 : {
578 1 : const sort_expression_list domain = function_sort(constructor.sort()).domain();
579 3 : for (const sort_expression& s: domain)
580 : {
581 2 : const data::variable param = m_datamgr.generate_fresh_variable(m_unfold_parameter.name(), s);
582 2 : m_injected_parameters.push_back(param);
583 2 : mCRL2log(log::verbose) << "- Injecting process parameter: " << param
584 0 : << "::" << pp(s) << std::endl;
585 2 : }
586 1 : }
587 1 : else if (is_basic_sort(constructor.sort())
588 0 : || is_structured_sort(constructor.sort())
589 1 : || is_container_sort(constructor.sort()))
590 : {
591 1 : mCRL2log(debug) << "- No process parameters are injected for constant: "
592 0 : << constructor << std::endl;
593 : }
594 : else
595 : {
596 0 : throw mcrl2::runtime_error("Parameter " + pp(constructor) + " has an unsupported type " + pp(constructor.sort()));
597 : }
598 : }
599 :
600 1 : new_process_parameters.insert(new_process_parameters.end(),
601 : m_injected_parameters.begin(),
602 : m_injected_parameters.end());
603 :
604 :
605 1 : ++unfold_parameter_it;
606 : /* Copy the remainder of the parameters */
607 1 : new_process_parameters.insert(new_process_parameters.end(),
608 1 : unfold_parameter_it, process_parameters.end());
609 :
610 1 : mCRL2log(debug) << "- New LPS process parameters: " << data::pp(new_process_parameters) << std::endl;
611 :
612 : // update the summands in new_lps
613 1 : unfold_summands(m_spec.process().action_summands());
614 :
615 : // Replace occurrences of unfolded parameters by the corresponding case function
616 : // Clear process parameters first, to ensure capture avoiding substitution
617 : // ignores the process parameters.
618 1 : m_spec.process().process_parameters() = data::variable_list();
619 1 : if (m_alt_case_placement)
620 : {
621 0 : m_datamgr.create_case_function(m_unfold_parameter.sort(), data::sort_bool::bool_()); // conditions
622 0 : m_datamgr.create_case_function(m_unfold_parameter.sort(), data::sort_real::real_()); // time/distributions
623 :
624 : // process parameters
625 0 : for (const data::variable& param : new_process_parameters)
626 : {
627 0 : m_datamgr.create_case_function(m_unfold_parameter.sort(), param.sort());
628 : }
629 :
630 : // parameters of actions
631 0 : for (const process::action_label& action_label : m_spec.action_labels())
632 : {
633 0 : for (const sort_expression& s : action_label.sorts())
634 : {
635 0 : m_datamgr.create_case_function(m_unfold_parameter.sort(), s);
636 : }
637 : }
638 :
639 0 : mCRL2log(log::verbose) << "- Inserting case functions into the process using alternative case placement" << std::endl;
640 : // place the case functions
641 0 : insert_case_functions(m_spec.process(), parameter_case_function(), m_datamgr.id_gen());
642 : }
643 : else
644 : {
645 1 : mCRL2log(log::verbose) << "- Inserting case functions into the process using default case placement" << std::endl;
646 : //Prepare parameter substitution
647 1 : const mutable_map_substitution< std::map< data::variable , data::data_expression > > s{parameter_substitution()};
648 1 : lps::replace_variables_capture_avoiding(m_spec.process(), s);
649 1 : }
650 :
651 1 : if (m_unfold_pattern_matching)
652 : {
653 : // Unfold pattern matching mappings in parameter updates, requires intermediate rewriting
654 1 : data::rewriter rewr(m_spec.data());
655 2 : for (action_summand& sum: m_spec.process().action_summands())
656 : {
657 1 : data::assignment_vector new_assignments;
658 4 : for (const assignment& as: sum.assignments())
659 : {
660 3 : new_assignments.emplace_back(as.lhs(), unfold_pattern_matching(rewr(as.rhs()), m_pattern_unfolder));
661 : }
662 1 : sum.assignments() = data::assignment_list(new_assignments.begin(), new_assignments.end());
663 1 : }
664 1 : }
665 :
666 : // NB: order is important. If we first replace the parameters, they are changed
667 : // again when performing the capture avoiding substitution, most likely leading
668 : // to an LPS that is not well-formed.
669 1 : m_spec.process().process_parameters() = data::variable_list(new_process_parameters.begin(), new_process_parameters.end());
670 :
671 1 : mCRL2log(debug) << "\nNew LPS:\n" << lps::pp(m_spec.process()) << std::endl;
672 :
673 1 : assert(check_well_typedness(m_spec.process()));
674 1 : }
675 :
676 1 : void lpsparunfold::update_linear_process_initialization(
677 : std::size_t parameter_at_index)
678 : {
679 : //
680 : //update inital process
681 : //
682 1 : mCRL2log(log::verbose) << "Updating initialization...\n" << std::endl;
683 :
684 : //Unfold parameters
685 1 : data::data_expression_vector new_init;
686 1 : size_t index=0;
687 2 : for (const data::data_expression& k: m_spec.initial_process().expressions())
688 : {
689 1 : if (index == parameter_at_index)
690 : {
691 1 : const data::data_expression_vector ins = unfold_constructor(k);
692 : //Replace unfold parameters in affected assignments
693 1 : new_init.insert(new_init.end(), ins.begin(), ins.end());
694 1 : }
695 : else
696 : {
697 0 : new_init.push_back(k);
698 : }
699 1 : ++index;
700 1 : }
701 :
702 3 : m_spec.initial_process() = stochastic_process_initializer(
703 2 : data_expression_list(new_init.begin(), new_init.end()),
704 2 : m_spec.initial_process().distribution());
705 :
706 1 : mCRL2log(debug) << "Expressions for the new initial state: " << data::pp(m_spec.initial_process().expressions()) << std::endl;
707 1 : }
708 :
709 1 : std::map<data::variable, data::data_expression> lpsparunfold::parameter_substitution()
710 : {
711 1 : const unfold_cache_element& new_cache_element = m_datamgr.get_cache_element(m_unfold_parameter.sort());
712 1 : std::map<data::variable, data::data_expression> result;
713 :
714 1 : data_expression_vector dev;
715 :
716 1 : auto new_pars_it = m_injected_parameters.cbegin();
717 1 : dev.push_back(data_expression(*new_pars_it));
718 1 : ++new_pars_it;
719 :
720 3 : for (const data::function_symbol& constr: new_cache_element.affected_constructors)
721 : {
722 2 : data::data_expression case_func_arg = constr;
723 :
724 2 : if (is_function_sort(constr.sort()))
725 : {
726 1 : sort_expression_list dom = function_sort(constr.sort()).domain();
727 1 : data_expression_vector arg;
728 :
729 3 : for (const data::sort_expression& arg_sort: dom)
730 : {
731 2 : if (new_pars_it->sort() != arg_sort)
732 : {
733 0 : throw runtime_error("Unexpected new parameter encountered, maybe they were not sorted well.");
734 : }
735 2 : arg.push_back(*new_pars_it++);
736 : }
737 1 : case_func_arg = data::application(constr, arg);
738 1 : }
739 :
740 2 : dev.push_back(case_func_arg);
741 2 : }
742 1 : mCRL2log(log::verbose)
743 0 : << "Parameter substitution:\t" << m_unfold_parameter
744 0 : << "\t->\t" << data::application(new_cache_element.case_functions.at(m_unfold_parameter.sort()), dev) << std::endl;
745 1 : result.insert(std::make_pair(
746 2 : m_unfold_parameter, data::application(new_cache_element.case_functions.at(m_unfold_parameter.sort()), dev)));
747 2 : return result;
748 1 : }
749 :
750 6 : data::data_expression lpsparunfold::apply_function(const function_symbol& f, const data_expression& de) const
751 : {
752 6 : if(m_alt_case_placement && is_if_application(de))
753 : {
754 0 : return data::if_(atermpp::down_cast<data::application>(de)[0],
755 0 : apply_function(f, atermpp::down_cast<data::application>(de)[1]),
756 0 : apply_function(f, atermpp::down_cast<data::application>(de)[2]));
757 : }
758 : else
759 : {
760 6 : return application(f, de);
761 : }
762 : }
763 :
764 2 : data::data_expression_vector lpsparunfold::unfold_constructor(const data_expression& de)
765 : {
766 2 : assert(de.sort() == m_unfold_parameter.sort());
767 2 : const unfold_cache_element& new_cache_element = m_datamgr.get_cache_element(m_unfold_parameter.sort());
768 2 : data::data_expression_vector result;
769 :
770 : // Replace global variables with fresh global variables.
771 3 : if(data::is_variable(de) &&
772 3 : m_spec.global_variables().find(atermpp::down_cast<variable>(de)) != m_spec.global_variables().end())
773 : {
774 : // don't care for det position
775 0 : variable v = m_datamgr.generate_fresh_variable("dc", new_cache_element.determine_function.sort().target_sort());
776 0 : result.push_back(v);
777 0 : m_spec.global_variables().insert(v);
778 :
779 : // don't cares for each of the arguments
780 0 : for (const function_symbol& f: new_cache_element.projection_functions)
781 : {
782 0 : v = m_datamgr.generate_fresh_variable("dc", f.sort().target_sort());
783 0 : result.push_back(v);
784 0 : m_spec.global_variables().insert(v);
785 : }
786 0 : }
787 : else
788 : {
789 : /* Det function */
790 2 : result.emplace_back(apply_function(new_cache_element.determine_function, de));
791 :
792 6 : for (const function_symbol& f: new_cache_element.projection_functions)
793 : {
794 4 : result.emplace_back(apply_function(f, de));
795 : }
796 : }
797 :
798 2 : return result;
799 0 : }
800 :
801 1 : data::variable lpsparunfold::process_parameter_at(const std::size_t index)
802 : {
803 1 : mCRL2log(debug) << "- Number of parameters in LPS: " << m_spec.process().process_parameters().size() << "" << std::endl;
804 1 : mCRL2log(log::verbose) << "Unfolding process parameter at index: " << index << "" << std::endl;
805 1 : if ( m_spec.process().process_parameters().size() <= index)
806 : {
807 0 : throw mcrl2::runtime_error("Given index out of bounds. Index value needs to be in the range [0," + std::to_string(m_spec.process().process_parameters().size()) + ").");
808 : }
809 :
810 1 : data::variable_list::const_iterator parameter_it = m_spec.process().process_parameters().begin();
811 1 : std::advance(parameter_it, index);
812 2 : return *parameter_it;
813 : }
814 :
815 1 : void lpsparunfold::algorithm(const std::size_t parameter_at_index)
816 : {
817 : // Can only be run once as local data structures are not cleared
818 1 : assert(!m_run_before);
819 1 : m_run_before = true;
820 :
821 1 : m_unfold_parameter = process_parameter_at(parameter_at_index);
822 1 : const unfold_cache_element& new_cache_element = m_datamgr.get_cache_element(m_unfold_parameter.sort());
823 :
824 : // Perform the actual unfolding (if needed)
825 1 : if (new_cache_element.affected_constructors.empty())
826 : {
827 0 : mCRL2log(log::verbose) << "The selected process parameter " << m_unfold_parameter.name() << " has no constructors." << std::endl;
828 0 : mCRL2log(log::verbose) << "No need to unfold." << std::endl;
829 : }
830 : else
831 : {
832 1 : update_linear_process(parameter_at_index);
833 1 : update_linear_process_initialization(parameter_at_index);
834 : }
835 :
836 1 : assert(check_well_typedness(m_spec));
837 1 : }
|
