Line data Source code
1 : // Author(s): Frank Stappers, 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 : /// \file lpsparunfold/lpsparunfoldlib.h
10 : /// \brief Unfold process parameters in mCRL2 process specifications.
11 :
12 : #ifndef MCRL2_LPS_LPSPARUNFOLDLIB_H
13 : //Fileinfo
14 : #define MCRL2_LPS_LPSPARUNFOLDLIB_H
15 :
16 : #include "mcrl2/data/consistency.h"
17 : #include "mcrl2/data/representative_generator.h"
18 : #include "mcrl2/data/unfold_pattern_matching.h"
19 : #include "mcrl2/lps/detail/lps_algorithm.h"
20 : #include "mcrl2/lps/replace_capture_avoiding.h"
21 :
22 : namespace mcrl2::lps
23 : {
24 :
25 : /// \brief Element in the cache that keeps track of the information for a single
26 : /// unfolded sort, say s.
27 : struct unfold_cache_element
28 : {
29 : mcrl2::data::function_symbol_vector affected_constructors; // constructors for s
30 : mcrl2::data::basic_sort fresh_basic_sort; // new sort introduced to represent s
31 : mcrl2::data::function_symbol_vector new_constructors; // constructors for fresh_basic_sort
32 : mcrl2::core::identifier_string case_function_name; // name of the case function introduced to deal with sort s
33 : // case functions for sort s. Note this may be more due to, e.g., adding distribution rules.
34 : // invariant: case_functions.front() is the case function
35 : // C: fresh_basic_sort # s # ... # s -> s
36 : std::map<mcrl2::data::sort_expression, mcrl2::data::function_symbol> case_functions;
37 : mcrl2::data::function_symbol determine_function; // Det function for s
38 : mcrl2::data::function_symbol_vector projection_functions; // pi functions for s
39 : };
40 :
41 : namespace detail
42 : {
43 : /// \brief Fresh variable generator for the arguments of a function symbol.
44 : ///
45 : /// Intended for use to generate variables in the left hand side of a data equation.
46 : /// Therefore, reuse of fresh variables is allowed in multiple equations.
47 : /// This generator reuses such variable names.
48 : class data_equation_argument_generator
49 : {
50 : public:
51 1 : data_equation_argument_generator(
52 : data::set_identifier_generator& identifier_generator)
53 1 : : m_identifier_generator(identifier_generator)
54 1 : {}
55 :
56 : /// Generate argument variables for f.
57 15 : data::variable_vector arguments(const data::function_symbol& f)
58 : {
59 15 : data::variable_vector result;
60 15 : std::map<data::sort_expression, std::size_t> used_arguments;
61 15 : if (is_function_sort(f.sort()))
62 : {
63 42 : for(const data::sort_expression& arg_sort: atermpp::down_cast<data::function_sort>(f.sort()).domain())
64 : {
65 : // Check if we already used the sort for this function symbol.
66 31 : if(used_arguments.find(arg_sort) == used_arguments.end())
67 : {
68 21 : used_arguments[arg_sort] = 0;
69 : }
70 :
71 : // Check if we need to generate a new variable.
72 31 : if(m_variables[arg_sort].size() == used_arguments[arg_sort])
73 : {
74 7 : m_variables[arg_sort].emplace_back(m_identifier_generator("d"), arg_sort);
75 : }
76 :
77 : // Push new variable
78 31 : result.push_back(m_variables[arg_sort].at(used_arguments[arg_sort]));
79 31 : ++used_arguments[arg_sort];
80 : }
81 : }
82 30 : return result;
83 15 : }
84 :
85 : protected:
86 : data::set_identifier_generator& m_identifier_generator;
87 : std::map<data::sort_expression, data::variable_vector> m_variables;
88 : };
89 :
90 : class unfold_data_manager
91 : {
92 : private:
93 : /// \brief cache for previously unfolded sorts.
94 : /// facilitates reuse of previously introduced sorts and function symbols.
95 : std::map< mcrl2::data::sort_expression , unfold_cache_element >& m_cache;
96 :
97 : data::data_specification& m_dataspec;
98 :
99 : /// \brief set of identifiers to use during fresh variable generation
100 : mcrl2::data::set_identifier_generator m_identifier_generator;
101 :
102 : /// \brief generator for arguments in left hand side of data equations
103 : detail::data_equation_argument_generator m_data_equation_argument_generator;
104 :
105 : /// \brief a generator for default data expressions of a given sort;
106 : mcrl2::data::representative_generator m_representative_generator;
107 :
108 : /// \brief Boolean indicating whether rewrite rules may be added that could make
109 : /// the data specification inconsistent.
110 : bool m_possibly_inconsistent;
111 :
112 : public:
113 1 : unfold_data_manager(std::map< mcrl2::data::sort_expression , unfold_cache_element >& cache, data::data_specification& dataspec, bool possibly_inconsistent)
114 1 : : m_cache(cache)
115 1 : , m_dataspec(dataspec)
116 1 : , m_identifier_generator()
117 1 : , m_data_equation_argument_generator(m_identifier_generator)
118 1 : , m_representative_generator(dataspec)
119 1 : , m_possibly_inconsistent(possibly_inconsistent)
120 1 : {}
121 :
122 1 : const data::data_specification& dataspec() const { return m_dataspec; }
123 :
124 30 : void add_used_identifier(const core::identifier_string& id)
125 : {
126 30 : m_identifier_generator.add_identifier(id);
127 30 : }
128 :
129 2 : void add_used_identifiers(const std::set<core::identifier_string>& ids)
130 : {
131 2 : m_identifier_generator.add_identifiers(ids);
132 2 : }
133 :
134 0 : data::set_identifier_generator& id_gen()
135 : {
136 0 : return m_identifier_generator;
137 : }
138 :
139 : unfold_cache_element& get_cache_element(const data::sort_expression& sort);
140 :
141 0 : bool is_cached(const data::sort_expression& sort) const
142 : {
143 0 : return m_cache.find(sort) != m_cache.end();
144 : }
145 :
146 0 : bool is_constructor(const data::function_symbol& f) const
147 : {
148 0 : return utilities::detail::contains(m_dataspec.constructors(), f);
149 : }
150 :
151 0 : const std::vector<data::function_symbol>& get_constructors(const data::sort_expression& sort)
152 : {
153 0 : return get_cache_element(sort).affected_constructors;
154 : }
155 :
156 0 : data::data_expression create_cases(const data::data_expression& target, const data::data_expression_vector& rhss)
157 : {
158 0 : unfold_cache_element& cache_elem = get_cache_element(target.sort());
159 0 : data::application first_arg(cache_elem.determine_function, target);
160 :
161 0 : data::data_expression_vector args;
162 0 : args.push_back(first_arg);
163 0 : for (const data::data_expression& rhs: rhss)
164 : {
165 0 : args.push_back(rhs);
166 : }
167 :
168 0 : return data::application(cache_elem.case_functions.at(rhss.front().sort()), args);
169 0 : }
170 :
171 0 : const data::function_symbol_vector& get_projection_funcs(const data::function_symbol& f)
172 : {
173 0 : return get_cache_element(f.sort().target_sort()).projection_functions;
174 : }
175 :
176 : /** \brief Generates a fresh basic sort given a sort expression.
177 : * \param sort This sort's name will be used to derive a name for the new sort
178 : * \return A fresh basic sort.
179 : **/
180 : mcrl2::data::basic_sort generate_fresh_basic_sort(const data::sort_expression& sort);
181 :
182 : /** \brief Generates a fresh name for a constructor or mapping.
183 : * \param str a string value. The value is used to generate a fresh
184 : * name for a constructor or mapping.
185 : * \post A fresh name for a constructor or mapping is generated.
186 : * \return A fresh name for a constructor or mapping.
187 : **/
188 : mcrl2::core::identifier_string generate_fresh_function_symbol_name(const std::string& str);
189 :
190 : /** \brief Generates variable of type sort based on a given string str.
191 : * \param str a string value. The value is used to generate a fresh
192 : * variable name.
193 : * \param sort The sort of the variable to generate.
194 : * \post A fresh variable is generated, which has an unique name.
195 : * \return A fresh variable.
196 : **/
197 : mcrl2::data::variable generate_fresh_variable(std::string str, const data::sort_expression& sort);
198 :
199 :
200 : /** \brief Creates the determine function.
201 : * \param sort The sort on which this function operates
202 : * \return A function that maps constructors to the fresh basic sort
203 : **/
204 : void create_determine_function(const data::sort_expression& sort);
205 :
206 : /** \brief Creates projection functions for the unfolded process parameter.
207 : * \param sort The sort on which these functions operate
208 : * \return A function that returns the projection functions for the
209 : * constructors of the unfolded process parameter.
210 : **/
211 : void create_projection_functions(const data::sort_expression& sort);
212 :
213 : /** \brief Determines the constructors that are affected with the unfold
214 : * process parameter.
215 : * \param sort The sort for which to find constructors
216 : * \post The constructors that are affected with the unfold
217 : * process parameter are stored in m_affected_constructors
218 : **/
219 : void determine_affected_constructors(const data::sort_expression& sort);
220 :
221 : /** \brief Creates a set of constructors for the fresh basic sort
222 : * \param sort The sort for which to create analogous constructors
223 : * \return The constructors that are created for the fresh basic sort
224 : **/
225 : void create_new_constructors(const data::sort_expression& sort);
226 :
227 : /** \brief Creates the case function with number of arguments determined by
228 : * the number of affected constructors, the sort of the arguments and
229 : * result are determined by sort..
230 : * \param det_sort The sort whose constructor is determined in the first argument
231 : * \param output_sort The sort of the arguments and return sort of the case function
232 : * \return A function that returns the corresponding constructor given the
233 : * case selector and constructors.
234 : **/
235 : data::function_symbol create_case_function(const data::sort_expression& det_sort, const data::sort_expression& output_sort);
236 :
237 : /** \brief Create distribution rules for distribution_functions over case_functions
238 : **/
239 : void create_distribution_law_over_case(
240 : const data::sort_expression& sort,
241 : const data::function_symbol& function_for_distribution,
242 : const data::function_symbol case_function);
243 :
244 :
245 : /** \brief Create the data equations for case functions */
246 : void generate_case_function_equations(
247 : const data::sort_expression& sort,
248 : const data::function_symbol& case_function);
249 :
250 : /** \brief Create the data equations for the determine function */
251 : void generate_determine_function_equations(const data::sort_expression& sort);
252 :
253 : /** \brief Create the data equations for the projection functions */
254 : void generate_projection_function_equations(const data::sort_expression& sort);
255 :
256 40 : static bool char_filter(char c)
257 : {
258 : // Put unwanted characters here
259 40 : return c==' ' || c==':' || c==',' || c=='|'
260 40 : || c=='>' || c=='[' || c==']' || c=='@'
261 38 : || c=='.' || c=='{' || c=='}' || c=='#'
262 38 : || c=='%' || c=='&' || c=='*' || c=='!'
263 80 : || c=='(' || c==')'
264 : ;
265 : }
266 :
267 6 : std::string filter_illegal_characters(std::string in) const
268 : {
269 6 : in.resize(std::remove_if(in.begin(), in.end(), &char_filter) - in.begin());
270 6 : return in;
271 : }
272 : };
273 :
274 : /// @brief Class for unfolding expressions f(a1,...,an) based on the pattern-matching
275 : /// rewrite rules that define f.
276 : class pattern_match_unfolder
277 : {
278 : private:
279 : unfold_data_manager& m_datamgr;
280 : data::representative_generator m_repgen;
281 : std::map<data::function_symbol, bool> m_is_pattern_matching;
282 : std::map<data::function_symbol, data::data_equation> m_new_eqns;
283 :
284 : /// @brief Finds all rewriting equations for f
285 0 : const data::data_equation_vector find_equations(const data::function_symbol& f)
286 : {
287 0 : data::data_equation_vector result;
288 0 : for (const data::data_equation& eqn: m_datamgr.dataspec().equations())
289 : {
290 0 : if (data::detail::get_top_fs(eqn.lhs()) == f)
291 : {
292 0 : result.push_back(eqn);
293 : }
294 : }
295 0 : return result;
296 0 : }
297 :
298 : /// @brief Checks whether f is defined by pattern matching
299 0 : bool is_pattern_matching(const data::function_symbol& f)
300 : {
301 0 : auto find_result = m_is_pattern_matching.find(f);
302 0 : if (find_result != m_is_pattern_matching.end())
303 : {
304 0 : return find_result->second;
305 : }
306 0 : data::data_equation_vector eqns = find_equations(f);
307 0 : bool result = std::all_of(eqns.begin(), eqns.end(),
308 0 : [&](auto& eqn) { return data::is_pattern_matching_rule(m_datamgr, eqn); });
309 0 : m_is_pattern_matching.insert_or_assign(f, result);
310 0 : return result;
311 0 : }
312 :
313 0 : data::data_expression unfolded_expr(const data::function_symbol& f, const data::data_expression_vector& args)
314 : {
315 0 : data::data_equation new_eqn;
316 0 : auto find_result = m_new_eqns.find(f);
317 0 : if (find_result != m_new_eqns.end())
318 : {
319 0 : new_eqn = find_result->second;
320 : }
321 : else
322 : {
323 0 : new_eqn = data::unfold_pattern_matching(f, find_equations(f), m_datamgr, m_repgen, m_datamgr.id_gen());
324 0 : m_new_eqns.emplace(f, new_eqn);
325 : }
326 :
327 0 : std::map<data::variable, data::data_expression> sigma;
328 0 : auto it1 = atermpp::down_cast<data::application>(new_eqn.lhs()).begin();
329 0 : auto it2 = args.begin();
330 0 : while (it2 != args.end())
331 : {
332 0 : sigma[atermpp::down_cast<data::variable>(*it1++)] = *it2++;
333 : }
334 0 : data::map_substitution sigma1(sigma);
335 :
336 :
337 0 : return data::replace_all_variables(new_eqn.rhs(), sigma1);
338 0 : }
339 :
340 : public:
341 1 : pattern_match_unfolder(unfold_data_manager& datamgr)
342 1 : : m_datamgr(datamgr)
343 1 : , m_repgen(datamgr.dataspec())
344 1 : {}
345 :
346 0 : bool is_constructor(const data::function_symbol& f)
347 : {
348 0 : return m_datamgr.is_constructor(f);
349 : }
350 :
351 : /// @brief Checks whether expr is of the shape Det(h(a1,...,an)) or pi(h(a1,...,an)),
352 : /// where h is defined by patter matching, and, if so, unfolds h(a1,...,an).
353 2 : bool is_det_or_pi(const data::application& expr) const
354 : {
355 : using utilities::detail::contains;
356 :
357 2 : const data::function_symbol f = data::detail::get_top_fs(expr);
358 : // If f is not unary, then it is certainly unequal to Det or pi
359 2 : if (f == data::function_symbol() || expr.size() != 1)
360 : {
361 2 : return false;
362 : }
363 0 : const data::sort_expression& arg_sort = *atermpp::down_cast<data::function_sort>(f.sort()).domain().begin();
364 : // The argument of f must be of an unfolded sort
365 0 : if (!m_datamgr.is_cached(arg_sort))
366 : {
367 0 : return false;
368 : }
369 0 : const unfold_cache_element& cache_elem = m_datamgr.get_cache_element(arg_sort);
370 0 : if (f != cache_elem.determine_function && !contains(cache_elem.projection_functions, f))
371 : {
372 0 : return false;
373 : }
374 :
375 0 : return true;
376 2 : }
377 :
378 0 : bool can_unfold(const data::data_expression& x)
379 : {
380 0 : if (!data::is_application(x))
381 : {
382 0 : return false;
383 : }
384 :
385 0 : const data::function_symbol f = data::detail::get_top_fs(atermpp::down_cast<data::application>(x));
386 0 : if (f == data::function_symbol() || !is_pattern_matching(f))
387 : {
388 0 : return false;
389 : }
390 0 : auto udm = m_datamgr.dataspec().mappings();
391 0 : const data::data_specification& dataspec = m_datamgr.dataspec();
392 0 : if (std::find_if(udm.begin(), udm.end(),
393 0 : [&](const auto& f2){ return f.name() == f2.name() && dataspec.equal_sorts(f.sort(), f2.sort()); }) == udm.end())
394 : {
395 : // f is not a mapping, but likely a constructor
396 0 : return false;
397 : }
398 0 : if (!matches_only_known_sorts(f))
399 : {
400 0 : return false;
401 : }
402 0 : return true;
403 0 : }
404 :
405 0 : std::vector<std::size_t> pattern_matching_args(const data::function_symbol& f)
406 : {
407 0 : std::vector<std::size_t> result;
408 0 : if (!data::is_function_sort(f.sort()))
409 : {
410 0 : return result;
411 : }
412 0 : data::data_equation_vector eqns = find_equations(f);
413 :
414 0 : std::size_t f_num_args = atermpp::down_cast<data::function_sort>(f.sort()).domain().size();
415 0 : for (std::size_t arg = 0; arg < f_num_args; arg++)
416 : {
417 0 : for (const data::data_equation& eq: eqns)
418 : {
419 0 : const data::application& lhs_appl = atermpp::down_cast<data::application>(eq.lhs());
420 0 : if (!data::is_variable(lhs_appl[arg]))
421 : {
422 0 : result.push_back(arg);
423 0 : break;
424 : }
425 : }
426 : }
427 0 : return result;
428 0 : }
429 :
430 : /// @brief Determines whether f pattern matches on argument arg
431 : /// @pre this->can_unfold(f)
432 0 : bool matches_only_known_sorts(const data::function_symbol& f)
433 : {
434 0 : if (!data::is_function_sort(f.sort()))
435 : {
436 0 : return true;
437 : }
438 :
439 0 : const data::sort_expression_list& domain = atermpp::down_cast<data::function_sort>(f.sort()).domain();
440 0 : const data::sort_expression_vector domain_vec{domain.begin(), domain.end()};
441 0 : for (const std::size_t i: pattern_matching_args(f))
442 : {
443 0 : if (!m_datamgr.is_cached(domain_vec[i]))
444 : {
445 0 : return false;
446 : }
447 0 : }
448 0 : return true;
449 0 : }
450 :
451 : /// @brief Unfolds expr if it is of the shape h(a1,...,an) and h is defined by pattern matching
452 : /// @pre this->can_unfold(x)
453 : template <class T>
454 0 : void operator()(T& result, const data::application& x)
455 : {
456 0 : const data::data_expression_vector args(x.begin(), x.end());
457 0 : result = unfolded_expr(data::detail::get_top_fs(x), args);
458 0 : }
459 : };
460 :
461 :
462 : template <template <class> class Builder>
463 : struct replace_pattern_match_builder: public Builder<replace_pattern_match_builder<Builder> >
464 : {
465 : typedef Builder<replace_pattern_match_builder<Builder> > super;
466 : using super::enter;
467 : using super::leave;
468 : using super::apply;
469 : using super::update;
470 :
471 : pattern_match_unfolder& m_unfolder;
472 : bool m_currently_recursing = false;
473 : std::size_t m_current_depth = 0;
474 :
475 3 : replace_pattern_match_builder(pattern_match_unfolder& unfolder)
476 3 : : m_unfolder(unfolder)
477 3 : {}
478 :
479 0 : bool is_applied_to_constructor(const data::application& x)
480 : {
481 : using utilities::detail::contains;
482 0 : const std::vector<std::size_t> pattern_matching_args = m_unfolder.pattern_matching_args(data::detail::get_top_fs(x));
483 0 : for(const std::size_t i: pattern_matching_args)
484 : {
485 0 : if (m_unfolder.is_constructor(data::detail::get_top_fs(x[i])))
486 : {
487 0 : return true;
488 : }
489 : }
490 0 : return false;
491 0 : }
492 :
493 : template <class T>
494 2 : void apply(T& result, const data::application& x)
495 : {
496 2 : if (m_currently_recursing)
497 : {
498 0 : if (m_current_depth >= 3 || m_unfolder.is_constructor(data::detail::get_top_fs(x)))
499 : {
500 : // Stop recursing after unfolding three times or when meeting a constructor
501 : // In the latter case, we have done enough to rewrite Det() and pi()
502 0 : result = x;
503 0 : return;
504 : }
505 0 : else if (data::is_if_application(x))
506 : {
507 : // In if-statements, do not traverse the condition
508 0 : data::data_expression branch1;
509 0 : super::apply(branch1, x[1]);
510 0 : data::data_expression branch2;
511 0 : super::apply(branch2, x[2]);
512 :
513 0 : data::make_application(result,
514 : data::if_(x.sort()),
515 : x[0],
516 : branch1,
517 : branch2
518 : );
519 0 : }
520 0 : else if (m_unfolder.can_unfold(x) && is_applied_to_constructor(x))
521 : {
522 0 : data::data_expression intermediate_result;
523 0 : m_unfolder(intermediate_result, x);
524 : // Recursively apply unfolding
525 0 : m_current_depth++;
526 0 : super::apply(result, intermediate_result);
527 0 : m_current_depth--;
528 0 : }
529 : else
530 : {
531 0 : super::apply(result, x);
532 : }
533 : }
534 : else
535 : {
536 : // Determine whether we see Det(f(..)) or pi(f(..))
537 : // If so, unfold and start recursing
538 2 : if (m_unfolder.is_det_or_pi(x) && m_unfolder.can_unfold(x[0]))
539 : {
540 0 : data::data_expression intermediate_result1, intermediate_result2;
541 0 : m_unfolder(intermediate_result1, atermpp::down_cast<data::application>(x[0]));
542 :
543 0 : m_currently_recursing = true;
544 0 : m_current_depth++;
545 0 : super::apply(intermediate_result2, intermediate_result1);
546 0 : m_current_depth--;
547 :
548 0 : mCRL2log(log::debug) << "Unfolded " << x[0] << " into " << intermediate_result2 << std::endl;
549 0 : data::make_application(result, x.head(), intermediate_result2);
550 0 : m_currently_recursing = false;
551 0 : }
552 : else
553 : {
554 2 : super::apply(result, x);
555 : }
556 : }
557 : }
558 : };
559 :
560 : inline
561 3 : data::data_expression unfold_pattern_matching(const data::data_expression& x,
562 : pattern_match_unfolder& unfolder
563 : )
564 : {
565 3 : data::data_expression result;
566 3 : replace_pattern_match_builder<data::data_expression_builder>(unfolder).apply(result, x);
567 3 : return result;
568 0 : }
569 : } // namespace detail
570 :
571 : class lpsparunfold: public detail::lps_algorithm<lps::stochastic_specification>
572 : {
573 : typedef typename detail::lps_algorithm<lps::stochastic_specification> super;
574 :
575 : public:
576 :
577 : // old parameter, case function, determinizing parameter, replacement expressions
578 : typedef std::tuple<data::variable, std::map<data::sort_expression, data::function_symbol>, data::variable, data::data_expression_vector> case_func_replacement;
579 :
580 : /** \brief Constructor for lpsparunfold algorithm.
581 : * \param[in] spec which is a valid mCRL2 process specification.
582 : * \param[in,out] cache Cache to store information for reuse.
583 : * \param[in] alt_case_placement If true, case functions are placed at a higher level.
584 : * \param[in] possibly_inconsistent If true, case functions over Booleans are replaced by a disjunction of conjunctions.
585 : * For this to be correct, the unfolded sort needs to satisfy some restrictions.
586 : * \post The content of mCRL2 process specification analysed for useful information and class variables are set.
587 : **/
588 : lpsparunfold(lps::stochastic_specification& spec,
589 : std::map< data::sort_expression , unfold_cache_element >& cache,
590 : bool alt_case_placement = false,
591 : bool possibly_inconsistent = false,
592 : bool unfold_pattern_matching = true);
593 :
594 : /** \brief Applies lpsparunfold algorithm on a process parameter of an mCRL2 process specification .
595 : * \pre algorithm has not been called before.
596 : * \param[in] parameter_at_index An integer value that represents the index value of an process parameter.
597 : * \post The process parameter at index parameter_at_index is unfolded in the mCRL2 process specification.
598 : **/
599 : void algorithm(const std::size_t parameter_at_index);
600 :
601 : private:
602 : /// \brief set to true when the algorithm has been run once; as the algorithm should
603 : /// run only once...
604 : bool m_run_before;
605 :
606 : /// @brief Bookkeeper for recogniser and projection functions.
607 : detail::unfold_data_manager m_datamgr;
608 : detail::pattern_match_unfolder m_pattern_unfolder;
609 :
610 : /// \brief The process parameter that needs to be unfold.
611 : mcrl2::data::variable m_unfold_parameter;
612 :
613 : /// \brief The process parameters that are inserted.
614 : mcrl2::data::variable_vector m_injected_parameters;
615 :
616 : /// \brief Boolean to indicate if alternative placement of case functions should be used.
617 : bool m_alt_case_placement;
618 :
619 : /// \brief Indicates whether functions defined by pattern matching that occur in the scope of
620 : /// a Det or pi in a state update should be unfolded.
621 : bool m_unfold_pattern_matching;
622 :
623 :
624 : //data::data_expression apply_case_function(const data::data_expression& expr, const case_func_replacement& case_funcs);
625 : case_func_replacement parameter_case_function();
626 :
627 : /** \brief Get the process parameter at given index
628 : * \param index The index of the parameter which must be obtained.
629 : * \return the process parameter at given index.
630 : **/
631 : mcrl2::data::variable process_parameter_at(const std::size_t index);
632 :
633 : /** \brief substitute function for replacing process parameters with unfolded process parameters functions.
634 : * \return substitute function for replacing process parameters with unfolded process parameters functions.
635 : **/
636 : std::map<mcrl2::data::variable, mcrl2::data::data_expression> parameter_substitution();
637 :
638 : data::data_expression apply_function(const data::function_symbol& f, const data::data_expression& de) const;
639 :
640 : /** \brief unfolds a data expression into a vector of process parameters
641 : * \param de the data expression
642 : * \return The following vector: < det(de), pi_0(de), ... ,pi_n(de) >
643 : **/
644 : mcrl2::data::data_expression_vector unfold_constructor(
645 : const mcrl2::data::data_expression& de);
646 :
647 : /** \brief substitute unfold process parameter in the linear process
648 : * \param parameter_at_index the parameter index
649 : * \post the process parameter at given index is unfolded in the the linear process
650 : **/
651 : void update_linear_process(std::size_t parameter_at_index);
652 :
653 : /** \brief substitute unfold process parameter in the initialization of the linear process
654 : * \param parameter_at_index the parameter index
655 : * \post the initialization for the linear process is updated by unfolding the parameter at given index is unfolded
656 : **/
657 : void update_linear_process_initialization(
658 : std::size_t parameter_at_index);
659 :
660 : // Applies 'process unfolding' to a sequence of summands.
661 : void unfold_summands(mcrl2::lps::stochastic_action_summand_vector& summands);
662 : };
663 :
664 :
665 : template <template <class> class Builder, template <template <class> class, class, class> class Binder>
666 : struct parunfold_replacement: public
667 : Binder<Builder, parunfold_replacement<Builder, Binder>, parunfold_replacement<Builder, Binder>>
668 : {
669 : typedef Binder<Builder, parunfold_replacement<Builder, Binder>, parunfold_replacement<Builder, Binder>> super;
670 : using super::enter;
671 : using super::leave;
672 : using super::apply;
673 : using super::update;
674 :
675 : data::detail::capture_avoiding_substitution_updater<parunfold_replacement<Builder, Binder>> sigma1;
676 : lpsparunfold::case_func_replacement case_funcs;
677 : data::data_expression current_replacement;
678 :
679 0 : parunfold_replacement(const lpsparunfold::case_func_replacement& case_funcs,
680 : data::set_identifier_generator& id_generator)
681 0 : : super(sigma1)
682 0 : , sigma1(*this, id_generator)
683 : {
684 0 : this->case_funcs = case_funcs;
685 0 : }
686 :
687 : template <class T>
688 0 : void apply(T& result, const data::application& x)
689 : {
690 0 : if (current_replacement != data::data_expression() || data::is_and(x) || data::is_or(x) || data::is_not(x) || data::is_imp(x) || data::is_if_application(x))
691 : {
692 : // if no placement of case functions is underway, or we are still traversing the regular boolean operators, we continue as usual
693 0 : super::apply(result, x);
694 : }
695 : else
696 : {
697 : // place the case functions here
698 0 : apply_case_function(result, x);
699 : }
700 0 : }
701 :
702 0 : void apply_case_function(data::data_expression& result, const data::application& expr)
703 : {
704 0 : auto& [par, case_f, det_f, replacements] = case_funcs;
705 :
706 0 : if (data::find_free_variables(expr).count(par) == 0)
707 : {
708 : // variable to be replaced does not occur here
709 : // make sure to still apply the substitutions necessary for the capture avoiding tricks
710 : // NB: stack overflow happens if type of second argument is 'data::data_expression'.
711 0 : super::apply(result, expr);
712 : }
713 : else
714 : {
715 0 : data::data_expression_vector args;
716 0 : args.push_back(det_f);
717 :
718 0 : for (const data::data_expression& r : replacements)
719 : {
720 0 : current_replacement = r;
721 0 : data::data_expression arg;
722 0 : super::apply(arg, expr);
723 0 : args.push_back(arg);
724 : }
725 0 : current_replacement = data::data_expression();
726 :
727 0 : if (case_f.find(expr.sort()) == case_f.end())
728 : {
729 0 : throw mcrl2::runtime_error("Case function with target sort " +
730 : data::pp(expr.sort()) + " not declared.");
731 : }
732 0 : result = data::application(case_f[expr.sort()], args);
733 0 : }
734 0 : }
735 :
736 : // Substitution application
737 0 : data::data_expression operator()(const data::variable& x)
738 : {
739 0 : if (current_replacement == data::data_expression())
740 : {
741 0 : return x;
742 : }
743 0 : if (std::get<0>(case_funcs) != x)
744 : {
745 0 : return x;
746 : }
747 0 : return current_replacement;
748 : }
749 : };
750 :
751 : template <template <class> class Builder, template <template <class> class, class, class> class Binder>
752 : parunfold_replacement<Builder, Binder>
753 0 : apply_parunfold_replacement_builder(const lpsparunfold::case_func_replacement& case_funcs,
754 : data::set_identifier_generator& id_generator)
755 : {
756 0 : return parunfold_replacement<Builder, Binder>(case_funcs, id_generator);
757 : }
758 :
759 : template <typename T>
760 0 : void insert_case_functions(T& x,
761 : const lpsparunfold::case_func_replacement& cfv,
762 : data::set_identifier_generator& id_generator,
763 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
764 : )
765 : {
766 0 : apply_parunfold_replacement_builder<lps::data_expression_builder, lps::detail::add_capture_avoiding_replacement>(cfv, id_generator).update(x);
767 0 : }
768 :
769 : template <typename T>
770 : void insert_case_functions(T& x,
771 : const lpsparunfold::case_func_replacement& cfv,
772 : typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
773 : )
774 : {
775 : data::set_identifier_generator id_generator;
776 : id_generator.add_identifiers(lps::find_identifiers(x));
777 : auto& [par, case_f, det_f, replacements] = cfv;
778 :
779 : // assumes all case functions have the same name and that par.sort() is in the map of case functions
780 : id_generator.add_identifier(case_f.find(par.sort())->second.name());
781 : id_generator.add_identifier(det_f.name());
782 : for (const data::data_expression& r: replacements)
783 : {
784 : id_generator.add_identifiers(data::find_identifiers(r));
785 : }
786 :
787 : insert_case_functions(x, cfv, id_generator);
788 : }
789 :
790 : } // namespace mcrl2::lps
791 :
792 :
793 : #endif
|
