Line data Source code
1 : // Author(s): Jan Friso Groote, 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/action_rename.h
10 : /// \brief Action rename specifications.
11 :
12 : #ifndef MCRL2_LPS_ACTION_RENAME_H
13 : #define MCRL2_LPS_ACTION_RENAME_H
14 :
15 : #include <regex>
16 :
17 : #include "mcrl2/core/parse.h"
18 :
19 : #include "mcrl2/data/rewriter.h"
20 : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
21 :
22 : #include "mcrl2/lps/stochastic_specification.h"
23 : #include "mcrl2/process/normalize_sorts.h"
24 : #include "mcrl2/process/replace.h"
25 : #include "mcrl2/process/translate_user_notation.h"
26 :
27 : // //Action rename rules
28 : // <ActionRenameRules>
29 : // ::= ActionRenameRules(<ActionRenameRule>*)
30 : //
31 : // //Action rename rule
32 : // <ActionRenameRule>
33 : // ::= ActionRenameRule(<DataVarId>*, <DataExprOrNil>,
34 : // <ParamIdOrAction>, <ActionRenameRuleRHS>)
35 : //
36 : // //Right-hand side of an action rename rule
37 : // <ActionRenameRuleRHS>
38 : // ::= <ParamId> [- tc]
39 : // | <Action> [+ tc]
40 : // | Delta
41 : // | Tau
42 : //
43 : // //Action rename action_rename_specification
44 : // <ActionRenameSpec>
45 : // ::= ActionRenameSpec(<DataSpec>, <ActSpec>, <ActionRenameRules>)
46 :
47 : namespace mcrl2
48 : {
49 :
50 : namespace lps
51 : {
52 :
53 : // ::= ActionRenameRule(<DataVarId>*, <DataExprOrNil>,
54 : // <ParamIdOrAction>, <ActionRenameRuleRHS>)
55 :
56 : /// \brief Action rename rule
57 : class action_rename_rule
58 : {
59 : protected:
60 : /// \brief The data variables of the rule
61 : data::variable_list m_variables;
62 :
63 : /// \brief The condition of the rule
64 : data::data_expression m_condition;
65 :
66 : /// \brief The left hand side of the rule
67 : process::action m_lhs;
68 :
69 : /// \brief right hand side of the rule. Can only be an action, tau or delta.
70 : process::process_expression m_rhs;
71 :
72 80 : bool check_that_rhs_is_tau_delta_or_an_action() const
73 : {
74 80 : return is_delta(m_rhs) || is_tau(m_rhs) || process::is_action(m_rhs);
75 : }
76 :
77 : public:
78 : /// \brief Constructor.
79 : action_rename_rule()
80 : { }
81 :
82 : /// \brief Constructor.
83 : /// \param t A term
84 : action_rename_rule(const atermpp::aterm_appl& t)
85 : {
86 : assert(core::detail::check_rule_ActionRenameRule(t));
87 : atermpp::aterm_appl::iterator i = t.begin();
88 : m_variables = atermpp::down_cast<data::variable_list>(*i++);
89 : m_condition = data::data_expression(*i++);
90 : m_lhs = process::action(*i++);
91 : m_rhs = process::process_expression(*i);
92 : assert(check_that_rhs_is_tau_delta_or_an_action());
93 : }
94 :
95 : /// \brief Constructor.
96 : /// \param t1 A term
97 : explicit action_rename_rule(const atermpp::aterm& t1)
98 : {
99 : const atermpp::aterm_appl t=atermpp::down_cast<atermpp::aterm_appl>(t1);
100 : assert(core::detail::check_rule_ActionRenameRule(t));
101 : atermpp::aterm_appl::iterator i = t.begin();
102 : m_variables = atermpp::down_cast<data::variable_list>(*i++);
103 : m_condition = data::data_expression(*i++);
104 : m_lhs = process::action(*i++);
105 : m_rhs = process::process_expression(*i);
106 : assert(check_that_rhs_is_tau_delta_or_an_action());
107 : }
108 :
109 : /// \brief Constructor.
110 40 : action_rename_rule(const data::variable_list& variables,
111 : const data::data_expression& condition,
112 : const process::action& lhs,
113 : const process::process_expression& rhs)
114 40 : : m_variables(variables), m_condition(condition), m_lhs(lhs), m_rhs(rhs)
115 : {
116 40 : assert(check_that_rhs_is_tau_delta_or_an_action());
117 40 : }
118 :
119 : /// \brief Returns the variables of the rule.
120 : /// \return The variables of the rule.
121 30 : const data::variable_list& variables() const
122 : {
123 30 : return m_variables;
124 : }
125 :
126 : /// \brief Returns the variables of the rule.
127 : /// \return The variables of the rule.
128 30 : data::variable_list& variables()
129 : {
130 30 : return m_variables;
131 : }
132 :
133 : /// \brief Returns the condition of the rule.
134 : /// \return The condition of the rule.
135 20 : const data::data_expression& condition() const
136 : {
137 20 : return m_condition;
138 : }
139 :
140 : /// \brief Returns the condition of the rule.
141 : /// \return The condition of the rule.
142 20 : data::data_expression& condition()
143 : {
144 20 : return m_condition;
145 : }
146 :
147 : /// \brief Returns the left hand side of the rule.
148 : /// \return The left hand side of the rule.
149 50 : const process::action& lhs() const // Type should be action, but as it can be a ParamId(identifier_string,data_expression_list),
150 : // which is not accepted by the typechecker, this is a temporary fix, until this option
151 : // is added to an action.
152 : {
153 50 : return m_lhs;
154 : }
155 :
156 : /// \brief Returns the right hand side of the rule.
157 : /// \return The right hand side of the rule.
158 40 : const process::process_expression& rhs() const
159 : {
160 40 : assert(check_that_rhs_is_tau_delta_or_an_action());
161 40 : return m_rhs;
162 : }
163 : };
164 :
165 :
166 : /// \brief Read-only singly linked list of action rename rules
167 : // typedef atermpp::term_list<action_rename_rule> action_rename_rule_list;
168 :
169 : /// \brief Action rename specification
170 : class action_rename_specification
171 : {
172 : protected:
173 :
174 : /// \brief The data specification of the action rename specification
175 : data::data_specification m_data;
176 :
177 : /// \brief The action labels of the action rename specification
178 : process::action_label_list m_action_labels;
179 :
180 : /// \brief The action rename rules of the action rename specification
181 : std::vector <action_rename_rule> m_rules;
182 :
183 : public:
184 : /// \brief Constructor.
185 6 : action_rename_specification()
186 6 : { }
187 :
188 : /// \brief Constructor.
189 : /// \param t A term
190 : action_rename_specification(atermpp::aterm_appl t)
191 : {
192 : assert(core::detail::check_rule_ActionRenameSpec(t));
193 : atermpp::aterm_appl::iterator i = t.begin();
194 : m_data = atermpp::down_cast<atermpp::aterm_appl>(*i++);
195 : m_action_labels = atermpp::down_cast<process::action_label_list>(atermpp::down_cast<atermpp::aterm_appl>(*i++)[0]);
196 :
197 : atermpp::aterm_list rules_list = atermpp::down_cast<atermpp::aterm_list>(atermpp::down_cast<atermpp::aterm_appl>(*i)[0]);
198 : for (const atermpp::aterm& r: rules_list)
199 : {
200 : m_rules.push_back(action_rename_rule(r));
201 : }
202 : }
203 :
204 : /// \brief Constructor.
205 : /// \param data A data specification
206 : /// \param action_labels A sequence of action labels
207 : /// \param rules A sequence of action rename rules
208 6 : action_rename_specification(
209 : const data::data_specification& data,
210 : const process::action_label_list& action_labels,
211 : const std::vector <action_rename_rule>& rules)
212 6 : :
213 6 : m_data(data),
214 6 : m_action_labels(action_labels),
215 6 : m_rules(rules)
216 6 : { }
217 :
218 : /// \brief Returns the data action_rename_specification.
219 : /// \return The data action_rename_specification.
220 12 : const data::data_specification& data() const
221 : {
222 12 : return m_data;
223 : }
224 :
225 : /// \brief Returns the data specification.
226 70 : data::data_specification& data()
227 : {
228 70 : return m_data;
229 : }
230 :
231 : /// \brief Returns the sequence of action labels
232 : /// \return A sequence of action labels containing all action
233 : /// labels occurring in the action_rename_specification (but it can have more).
234 57 : const process::action_label_list& action_labels() const
235 : {
236 57 : return m_action_labels;
237 : }
238 :
239 : /// \brief Returns the sequence of action labels
240 26 : process::action_label_list& action_labels()
241 : {
242 26 : return m_action_labels;
243 : }
244 :
245 : /// \brief Returns the action rename rules.
246 : /// \return The action rename rules.
247 6 : const std::vector<action_rename_rule>& rules() const
248 : {
249 6 : return m_rules;
250 : }
251 :
252 : /// \brief Returns the action rename rules.
253 38 : std::vector<action_rename_rule>& rules()
254 : {
255 38 : return m_rules;
256 : }
257 :
258 : /// \brief Indicates whether the action_rename_specification is well typed.
259 : /// \return Always returns true.
260 : bool is_well_typed() const
261 : {
262 : return true;
263 : }
264 : };
265 :
266 : inline
267 : atermpp::aterm_appl action_rename_rule_to_aterm(const action_rename_rule& rule)
268 : {
269 : return atermpp::aterm_appl(core::detail::function_symbol_ActionRenameRule(), rule.variables(), rule.condition(), rule.lhs(), rule.rhs());
270 : }
271 :
272 : inline
273 : atermpp::aterm_appl action_rename_specification_to_aterm(const action_rename_specification& spec)
274 : {
275 : std::vector<atermpp::aterm_appl> rules;
276 : for (const action_rename_rule& r: spec.rules())
277 : {
278 : rules.push_back(action_rename_rule_to_aterm(r));
279 : }
280 : return atermpp::aterm_appl(core::detail::function_symbol_ActionRenameSpec(),
281 : data::detail::data_specification_to_aterm(spec.data()),
282 : atermpp::aterm_appl(core::detail::function_symbol_ActSpec(), spec.action_labels()),
283 : atermpp::aterm_appl(core::detail::function_symbol_ActionRenameRules(), atermpp::aterm_list(rules.begin(), rules.end()))
284 : );
285 : }
286 :
287 : }
288 : }
289 :
290 :
291 : namespace mcrl2
292 : {
293 :
294 : namespace lps
295 : {
296 :
297 : /// \cond INTERNAL_DOCS
298 : namespace detail
299 : {
300 : // Put the equalities t==u in the replacement map as u:=t.
301 11 : inline void fill_replacement_map(const data::data_expression& equalities_in_conjunction,
302 : std::map<data::data_expression, data::data_expression>& replacement_map)
303 : {
304 11 : if (equalities_in_conjunction==data::sort_bool::true_())
305 : {
306 0 : return;
307 : }
308 11 : if (data::sort_bool::is_and_application(equalities_in_conjunction))
309 : {
310 2 : fill_replacement_map(data::sort_bool::left(equalities_in_conjunction),replacement_map);
311 2 : fill_replacement_map(data::sort_bool::right(equalities_in_conjunction),replacement_map);
312 2 : return;
313 : }
314 9 : if(is_equal_to_application(equalities_in_conjunction))
315 : {
316 6 : const data::application a=atermpp::down_cast<data::application>(equalities_in_conjunction);
317 6 : if (a[1]!=a[0])
318 : {
319 3 : replacement_map[a[1]]=a[0];
320 : }
321 6 : }
322 : }
323 :
324 : // Replace expressions in e according to the replacement map.
325 : // Assume that e only consists of and, not and equality applied to terms.
326 30 : inline data::data_expression replace_expressions(const data::data_expression& e,
327 : const std::map<data::data_expression, data::data_expression>& replacement_map)
328 : {
329 30 : if (data::sort_bool::is_and_application(e))
330 : {
331 8 : return data::sort_bool::and_(replace_expressions(data::sort_bool::left(e),replacement_map),
332 12 : replace_expressions(data::sort_bool::right(e),replacement_map));
333 : }
334 26 : if (data::sort_bool::is_not_application(e))
335 : {
336 1 : return data::sort_bool::not_(replace_expressions(data::sort_bool::arg(e),replacement_map));
337 : }
338 25 : if (is_equal_to_application(e))
339 : {
340 7 : const data::application a=atermpp::down_cast<data::application>(e);
341 14 : return data::application(a.head(),
342 14 : replace_expressions(a[0],replacement_map),
343 21 : replace_expressions(a[1],replacement_map));
344 7 : }
345 18 : const std::map<data::data_expression, data::data_expression>::const_iterator i=replacement_map.find(e);
346 18 : if (i!=replacement_map.end()) // found;
347 : {
348 0 : return i->second;
349 : }
350 18 : return e;
351 : }
352 :
353 : // Substitute the equalities in equalities_in_conjunction from right to left in e.
354 7 : inline data::data_expression substitute_equalities(const data::data_expression& e, const data::data_expression& equalities_in_conjunction)
355 : {
356 7 : std::map<data::data_expression, data::data_expression> replacement_map;
357 7 : fill_replacement_map(equalities_in_conjunction, replacement_map);
358 14 : return replace_expressions(e,replacement_map);
359 7 : }
360 :
361 : /// \brief Renames variables
362 : /// \param rcond A data expression
363 : /// \param rleft An action
364 : /// \param rright An action
365 : /// \param generator A generator for fresh identifiers
366 : template <typename IdentifierGenerator>
367 10 : void rename_renamerule_variables(data::data_expression& rcond, process::action& rleft, process::action& rright, IdentifierGenerator& generator)
368 : {
369 10 : data::mutable_map_substitution<> renamings;
370 :
371 10 : std::set< data::variable > new_vars = data::find_all_variables(rleft.arguments());
372 :
373 17 : for (const data::variable& v: new_vars)
374 : {
375 7 : mcrl2::core::identifier_string new_name = generator(std::string(v.name()));
376 :
377 7 : if (new_name != v.name())
378 : {
379 2 : renamings[v] = data::variable(new_name, v.sort());
380 : }
381 : }
382 :
383 10 : data::set_identifier_generator id_generator;
384 12 : for (const data::variable& v: data::substitution_variables(renamings))
385 : {
386 2 : id_generator.add_identifier(v.name());
387 : }
388 10 : rcond = data::replace_variables_capture_avoiding(rcond, renamings, id_generator);
389 10 : rleft = process::replace_variables_capture_avoiding(rleft, renamings, id_generator);
390 10 : rright = process::replace_variables_capture_avoiding(rright, renamings, id_generator);
391 10 : }
392 :
393 : /* ------------------------------------------ Normalise sorts ------------------------------------------ */
394 :
395 : inline
396 6 : void normalize_sorts(action_rename_specification& arspec)
397 : {
398 6 : arspec.action_labels()=process::normalize_sorts(arspec.action_labels(), arspec.data());
399 :
400 16 : for (action_rename_rule& rule: arspec.rules())
401 : {
402 20 : rule = action_rename_rule(data::normalize_sorts(rule.variables(), arspec.data()),
403 20 : data::normalize_sorts(rule.condition(), arspec.data()),
404 20 : process::normalize_sorts(rule.lhs(), arspec.data()),
405 30 : process::normalize_sorts(rule.rhs(), arspec.data()));
406 : }
407 6 : }
408 :
409 :
410 : /* ------------------------------------------ Translate user notation ------------------------------------------ */
411 :
412 : inline
413 6 : void translate_user_notation(action_rename_specification& arspec)
414 : {
415 16 : for (action_rename_rule& rule: arspec.rules())
416 : {
417 20 : rule = action_rename_rule(rule.variables(),
418 20 : data::translate_user_notation(rule.condition()),
419 20 : process::translate_user_notation(rule.lhs()),
420 30 : process::translate_user_notation(rule.rhs()));
421 : }
422 6 : }
423 :
424 : } // namespace detail
425 : /// \endcond
426 :
427 : /// \brief Rename the actions in a linear specification using a given action_rename_spec
428 : /// \details The actions in a linear specification are renamed according to a given
429 : /// action rename specification.
430 : /// Note that the rules are applied in the order they appear in the specification.
431 : /// This yield quite elaborate conditions in the resulting lps, as a latter rule
432 : /// can only be applied if an earlier rule is not applicable. Note also that
433 : /// there is always a default summand, where the action is not renamed. Using
434 : /// sum elimination and rewriting a substantial reduction of the conditions that
435 : /// are generated can be obtained, often allowing many summands to be removed.
436 : /// \param action_rename_spec The action_rename_specification to be used.
437 : /// \param lps_old_spec The input linear specification.
438 : /// \param rewr A data rewriter.
439 : /// \return The lps_old_spec where all actions have been renamed according
440 : /// to action_rename_spec.
441 : inline
442 6 : lps::stochastic_specification action_rename(
443 : const action_rename_specification& action_rename_spec,
444 : const lps::stochastic_specification& lps_old_spec,
445 : const data::rewriter& rewr,
446 : const bool enable_rewriting)
447 : {
448 : using namespace mcrl2::core;
449 : using namespace mcrl2::data;
450 : using namespace mcrl2::lps;
451 :
452 6 : const std::vector <action_rename_rule>& rename_rules = action_rename_spec.rules();
453 6 : stochastic_action_summand_vector lps_old_action_summands = lps_old_spec.process().action_summands();
454 6 : deadlock_summand_vector lps_deadlock_summands = lps_old_spec.process().deadlock_summands();
455 6 : process::action_list lps_new_actions;
456 :
457 6 : data::set_identifier_generator generator;
458 6 : generator.add_identifiers(lps::find_identifiers(lps_old_spec));
459 6 : generator.add_identifiers(data::function_and_mapping_identifiers(lps_old_spec.data()));
460 :
461 : //go through the rename rules of the rename file
462 6 : mCRL2log(log::debug) << "Rename rules found: " << rename_rules.size() << "\n";
463 16 : for (const action_rename_rule& r: rename_rules)
464 : {
465 10 : stochastic_action_summand_vector lps_new_action_summands;
466 :
467 10 : data_expression rule_condition = r.condition();
468 10 : process::action rule_old_action = r.lhs();
469 10 : process::action rule_new_action;
470 10 : process::process_expression new_element = r.rhs();
471 10 : if (!is_tau(new_element) && !is_delta(new_element))
472 : {
473 6 : rule_new_action = atermpp::down_cast<process::action>(new_element);
474 : }
475 :
476 10 : const bool to_tau = is_tau(new_element);
477 10 : const bool to_delta = is_delta(new_element);
478 :
479 : // Check here that the arguments of the rule_old_action only consist
480 : // of uniquely occurring variables or closed terms. Furthermore, check that the variables
481 : // in rule_new_action and in rule_condition are a subset of those in
482 : // rule_old_action. This check ought to be done in the static checking
483 : // part of the renaming rules, but as yet it has nog been done. Ultimately
484 : // this check should be moved there.
485 :
486 : // first check that the arguments of rule_old_action are variables or closed
487 : // terms.
488 :
489 22 : for (const data_expression& rule_old_argument_i: rule_old_action.arguments())
490 : {
491 17 : if (!is_variable(rule_old_argument_i) &&
492 17 : (!(data::find_all_variables(rule_old_argument_i).empty())))
493 : {
494 0 : throw mcrl2::runtime_error("The arguments of the lhs " + process::pp(rule_old_action) +
495 0 : " are not variables or closed expressions");
496 : }
497 : }
498 :
499 : // Check whether the variables in rhs are included in the lefthandside.
500 10 : std::set < variable > variables_in_old_rule = process::find_free_variables(rule_old_action);
501 10 : std::set < variable > variables_in_new_rule = process::find_free_variables(rule_new_action);
502 :
503 10 : if (!includes(variables_in_old_rule.begin(),variables_in_old_rule.end(),
504 : variables_in_new_rule.begin(),variables_in_new_rule.end()))
505 : {
506 0 : throw mcrl2::runtime_error("There are variables occurring in rhs " + process::pp(rule_new_action) +
507 0 : " of a rename rule not occurring in lhs " + process::pp(rule_old_action));
508 : }
509 :
510 : // Check whether the variables in condition are included in the lefthandside.
511 10 : std::set < variable > variables_in_condition = data::find_free_variables(rule_condition);
512 10 : if (!includes(variables_in_old_rule.begin(),variables_in_old_rule.end(),
513 : variables_in_condition.begin(),variables_in_condition.end()))
514 : {
515 0 : throw mcrl2::runtime_error("There are variables occurring in the condition " + data::pp(rule_condition) +
516 0 : " of a rename rule not occurring in lhs " + process::pp(rule_old_action));
517 : }
518 :
519 : // check for double occurrences of variables in the lhs. Note that variables_in_old_rule
520 : // is empty at the end.
521 22 : for (const data_expression& d: rule_old_action.arguments())
522 : {
523 12 : if (is_variable(d))
524 : {
525 7 : const variable& v = atermpp::down_cast<variable>(d);
526 7 : if (variables_in_old_rule.find(v)==variables_in_old_rule.end())
527 : {
528 0 : throw mcrl2::runtime_error("Variable " + data::pp(v) + " occurs more than once in lhs " +
529 0 : process::pp(rule_old_action) + " of an action rename rule");
530 : }
531 : else
532 : {
533 7 : variables_in_old_rule.erase(v);
534 : }
535 : }
536 : }
537 10 : assert(variables_in_old_rule.empty());
538 :
539 :
540 : //go through the summands of the old lps
541 10 : mCRL2log(log::debug) << "Action summands found: " << lps_old_action_summands.size() << "\n";
542 35 : for (const stochastic_action_summand& lps_old_action_summand: lps_old_action_summands)
543 : {
544 25 : process::action_list lps_old_actions = lps_old_action_summand.multi_action().actions();
545 :
546 : /* For each individual action in the multi-action, for which the
547 : rename rule applies, two new summands must be made, namely one
548 : where the rule does not match with the parameters of the action,
549 : and one where it actually does. This means that for a multiaction
550 : with k summands 2^k new summands can result. */
551 :
552 : std::vector < variable_list >
553 25 : lps_new_sum_vars(1,lps_old_action_summand.summation_variables());
554 25 : std::vector < data_expression > lps_new_condition(1,lps_old_action_summand.condition());
555 : std::vector < process::action_list >
556 50 : lps_new_actions(1,process::action_list());
557 25 : std::vector < bool > lps_new_actions_is_delta(1,false);
558 :
559 25 : mCRL2log(log::debug) << "Actions in summand found: " << lps_old_actions.size() << "\n";
560 50 : for (const process::action& lps_old_action: lps_old_actions)
561 : {
562 25 : if (equal_signatures(lps_old_action, rule_old_action))
563 : {
564 10 : mCRL2log(log::debug) << "Renaming action " << rule_old_action << "\n";
565 :
566 : //rename all previously used variables.
567 10 : data_expression renamed_rule_condition=rule_condition;
568 10 : process::action renamed_rule_old_action=rule_old_action;
569 10 : process::action renamed_rule_new_action=rule_new_action;
570 10 : detail::rename_renamerule_variables(renamed_rule_condition, renamed_rule_old_action, renamed_rule_new_action, generator);
571 :
572 : //go through the arguments of the action.
573 10 : data_expression_list::iterator lps_old_argument_i = lps_old_action.arguments().begin();
574 10 : data_expression new_equalities_condition=sort_bool::true_();
575 22 : for (const data_expression& rule_old_argument_i: renamed_rule_old_action.arguments())
576 : {
577 12 : if (is_variable(rule_old_argument_i))
578 : {
579 14 : new_equalities_condition=lazy::and_(new_equalities_condition,
580 21 : data::equal_to(rule_old_argument_i, *lps_old_argument_i));
581 : }
582 : else
583 : {
584 5 : assert((data::find_all_variables(rule_old_argument_i).empty())); // the argument must be closed, which is checked above.
585 : renamed_rule_condition=
586 10 : lazy::and_(renamed_rule_condition,
587 15 : data::equal_to(rule_old_argument_i, *lps_old_argument_i));
588 5 : if (enable_rewriting) renamed_rule_condition=rewr(renamed_rule_condition); // Make sure that renamed_rule_condition is as simple as possible.
589 : }
590 12 : lps_old_argument_i++;
591 : }
592 :
593 : /* insert the new equality condition in all the newly generated summands */
594 20 : for (data_expression& d: lps_new_condition)
595 : {
596 10 : d=lazy::and_(d,new_equalities_condition);
597 : }
598 :
599 : /* insert the new sum variables in all the newly generated summands */
600 10 : std::set<variable> new_vars = find_all_variables(renamed_rule_old_action);
601 17 : for (const variable& sdvi: new_vars)
602 : {
603 14 : for (variable_list& l: lps_new_sum_vars)
604 : {
605 7 : l.push_front(sdvi);
606 : }
607 : }
608 :
609 10 : if (enable_rewriting) renamed_rule_condition=rewr(renamed_rule_condition); // Make sure that renamed_rule_condition is as simple as possible.
610 10 : if (renamed_rule_condition==sort_bool::true_())
611 : {
612 3 : if (to_delta)
613 : {
614 0 : std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
615 0 : for (process::action_list& l: lps_new_actions)
616 : {
617 0 : l=process::action_list(); // the action becomes delta
618 0 : *i_is_delta=true;
619 0 : ++i_is_delta;
620 : }
621 : }
622 3 : else if (!to_tau)
623 : {
624 3 : std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
625 6 : for (process::action_list& l: lps_new_actions)
626 : {
627 3 : if (!*i_is_delta) // the action is not delta
628 : {
629 3 : l.push_front(renamed_rule_new_action);
630 : }
631 3 : ++i_is_delta;
632 : }
633 : }
634 : }
635 7 : else if (renamed_rule_condition==sort_bool::false_())
636 : {
637 0 : std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
638 0 : for (process::action_list& l: lps_new_actions)
639 : {
640 0 : if (!*i_is_delta) // The action does not equal delta.
641 : {
642 0 : l.push_front(lps_old_action);
643 : }
644 0 : ++i_is_delta;
645 : }
646 :
647 : }
648 : else
649 : {
650 : /* Duplicate summands, one where the renaming is applied, and one where it is not
651 : applied. */
652 :
653 7 : std::vector < process::action_list > lps_new_actions_temp(lps_new_actions);
654 :
655 7 : if (!to_tau) // if the new element is tau, we do not insert it in the multi-action.
656 : {
657 6 : std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
658 12 : for (process::action_list& l: lps_new_actions)
659 : {
660 6 : if (to_delta)
661 : {
662 3 : l=process::action_list();
663 3 : *i_is_delta=true;
664 : }
665 : else
666 : {
667 3 : l.push_front(renamed_rule_new_action);
668 3 : *i_is_delta=false;
669 : }
670 6 : ++i_is_delta;
671 : }
672 : }
673 :
674 14 : for (process::action_list& l: lps_new_actions_temp)
675 : {
676 7 : lps_new_actions_is_delta.push_back(false); // A non renamed action is not delta;
677 7 : l.push_front(lps_old_action);
678 : }
679 :
680 7 : lps_new_actions.insert(lps_new_actions.end(),
681 : lps_new_actions_temp.begin(),
682 : lps_new_actions_temp.end());
683 7 : assert(lps_new_actions_is_delta.size()==lps_new_actions.size());
684 :
685 : /* lps_new_condition_temp will contain the conditions in conjunction with
686 : the negated new_condition. It will be concatenated to lps_new_condition,
687 : in which the terms will be conjoined with the non-negated new_condition */
688 :
689 7 : std::vector < data_expression > lps_new_condition_temp(lps_new_condition);
690 :
691 14 : for (data_expression& d: lps_new_condition)
692 : {
693 : // substitute the equalities in d in renamed_rule_condition.
694 7 : d=lazy::and_(renamed_rule_condition,detail::substitute_equalities(d,renamed_rule_condition));
695 : }
696 :
697 14 : for (const data_expression& d: lps_new_condition_temp)
698 : {
699 :
700 7 : lps_new_condition.push_back(lazy::and_(d,sort_bool::not_(renamed_rule_condition)));
701 : }
702 :
703 : // Replace lps_new_sum_vars with two consecutive copies of itself.
704 : // The clumsily looking method below is required, to avoid problems with vector reallocation.
705 7 : std::size_t size=lps_new_sum_vars.size();
706 7 : lps_new_sum_vars.reserve(2*size);
707 14 : for(std::size_t i=0; i<size; ++i)
708 : {
709 7 : lps_new_sum_vars.push_back(lps_new_sum_vars[i]);
710 : }
711 7 : }
712 10 : }//end if(equal_signatures(...))
713 : else
714 : {
715 30 : for (process::action_list& l: lps_new_actions)
716 : {
717 15 : l.push_front(lps_old_action);
718 : }
719 : }
720 25 : mCRL2log(log::debug) << "Action done\n";
721 :
722 : } //end of action list iterator
723 :
724 : /* Add the summands to lps_new_action_summands or to the deadlock summands*/
725 :
726 25 : std::vector < process::action_list > :: iterator i_act=lps_new_actions.begin();
727 25 : std::vector < bool > :: iterator i_act_is_delta=lps_new_actions_is_delta.begin();
728 25 : std::vector < variable_list > :: iterator i_sumvars=lps_new_sum_vars.begin();
729 57 : for (const data_expression& cond: lps_new_condition)
730 : {
731 : //create a summand for the new lps
732 32 : if (*i_act_is_delta)
733 : {
734 : // Create a deadlock summand.
735 3 : const deadlock_summand d(*i_sumvars,
736 : cond,
737 9 : deadlock(lps_old_action_summand.multi_action().time()));
738 3 : lps_deadlock_summands.push_back(d);
739 3 : }
740 : else
741 : {
742 : // create an action summand.
743 29 : stochastic_action_summand lps_new_summand(*i_sumvars,
744 : cond,
745 58 : multi_action(reverse(*i_act), lps_old_action_summand.multi_action().time()),
746 : lps_old_action_summand.assignments(),
747 58 : lps_old_action_summand.distribution());
748 29 : lps_new_action_summands.push_back(lps_new_summand);
749 29 : }
750 32 : i_act++;
751 32 : i_sumvars++;
752 32 : ++i_act_is_delta;
753 : }
754 25 : } // end of summand list iterator
755 10 : lps_old_action_summands = lps_new_action_summands;
756 10 : } //end of rename rule iterator
757 :
758 6 : mCRL2log(log::debug) << "Simplifying the result...\n";
759 :
760 6 : stochastic_linear_process new_process(lps_old_spec.process().process_parameters(),
761 : lps_deadlock_summands,
762 6 : lps_old_action_summands);
763 :
764 : // add action_rename_spec.action_labels to action_rename_spec.action_labels without adding duplicates.
765 6 : process::action_label_list all=action_rename_spec.action_labels();
766 21 : for (const process::action_label& a: lps_old_spec.action_labels())
767 : {
768 15 : if (std::find(action_rename_spec.action_labels().begin(),
769 30 : action_rename_spec.action_labels().end(),a)==action_rename_spec.action_labels().end())
770 : {
771 : // Not found;
772 15 : all.push_front(a);
773 : }
774 : }
775 : stochastic_specification lps_new_spec(action_rename_spec.data(), // This contains the data of the lps and the rename file.
776 : all,
777 : lps_old_spec.global_variables(),
778 : new_process,
779 6 : lps_old_spec.initial_process());
780 :
781 6 : mCRL2log(log::debug) << "New lps complete\n";
782 12 : return lps_new_spec;
783 6 : } //end of rename(...)
784 :
785 : namespace detail
786 : {
787 :
788 : inline
789 30 : process::action_label rename_action_label(const process::action_label& act, const std::regex& matching_regex, const std::string& replacing_fmt)
790 : {
791 60 : return process::action_label(std::regex_replace(std::string(act.name()), matching_regex, replacing_fmt), act.sorts());
792 : }
793 :
794 : } // namespace detail
795 :
796 : /**
797 : * \brief Rename actions in given specification based on a regular expression and
798 : * a string that specifies how the replacement should be formatted.
799 : */
800 : inline
801 4 : stochastic_specification action_rename(
802 : const std::regex& matching_regex,
803 : const std::string& replacing_fmt,
804 : const stochastic_specification& lps_old_spec)
805 : {
806 : // Use a set to store the new action labels to avoid duplicates
807 4 : std::set<process::action_label> new_actions_set;
808 4 : process::action_label_list new_actions;
809 21 : for(const process::action_label& act: lps_old_spec.action_labels())
810 : {
811 17 : process::action_label new_action_label(detail::rename_action_label(act, matching_regex, replacing_fmt));
812 17 : if (std::string(new_action_label.name()).empty())
813 : {
814 0 : throw mcrl2::runtime_error("After renaming the action " + std::string(act.name()) + " becomes empty, which is not allowed.");
815 : }
816 48 : if(std::string(new_action_label.name()) != "delta" && std::string(new_action_label.name()) != "tau" &&
817 31 : new_actions_set.find(new_action_label) == new_actions_set.end())
818 : {
819 : // The list of actions should not contain delta and tau actions and also no duplicates.
820 13 : new_actions_set.insert(new_action_label);
821 13 : new_actions.push_front(new_action_label);
822 : }
823 17 : }
824 4 : new_actions = reverse(new_actions);
825 :
826 : // The list of new actions summands is initially empty
827 4 : std::vector<stochastic_action_summand> new_action_summands;
828 : // The list of new deadlock summands is initialised to the existing list, we will only add new deadlock summands
829 4 : std::vector<deadlock_summand> new_deadlock_summands(lps_old_spec.process().deadlock_summands());
830 15 : for(const stochastic_action_summand& as: lps_old_spec.process().action_summands())
831 : {
832 11 : process::action_list new_action_list;
833 11 : bool becomes_deadlock_summand = false;
834 23 : for(const process::action& act: as.multi_action().actions())
835 : {
836 13 : process::action_label new_action_label(detail::rename_action_label(act.label(), matching_regex, replacing_fmt));
837 13 : if(std::string(new_action_label.name()) == "delta")
838 : {
839 : // delta is the absorbing element for multi action concatenation
840 : // Therefore, this summand now becomes a deadlock summand
841 1 : becomes_deadlock_summand = true;
842 1 : break;
843 : }
844 : // tau is the identity for multi action concatenation
845 : // therefore, we should not add it to a multi action
846 12 : if(std::string(new_action_label.name()) != "tau")
847 : {
848 10 : new_action_list.push_front(process::action(new_action_label, act.arguments()));
849 : }
850 13 : }
851 :
852 11 : if(!becomes_deadlock_summand)
853 : {
854 10 : new_action_list = reverse(new_action_list);
855 10 : multi_action new_multi_action(new_action_list, as.multi_action().time());
856 :
857 : // Copy most of the old information, only the multi action has changed
858 10 : stochastic_action_summand new_summand(as.summation_variables(), as.condition(), new_multi_action, as.assignments(), as.distribution());
859 10 : new_action_summands.push_back(new_summand);
860 10 : }
861 : else
862 : {
863 : // Add a new deadlock summand, copying most of the information for the old action summand
864 1 : new_deadlock_summands.push_back(deadlock_summand(as.summation_variables(), as.condition(), deadlock(as.multi_action().time())));
865 : }
866 11 : }
867 :
868 4 : stochastic_linear_process new_process(lps_old_spec.process().process_parameters(),
869 : new_deadlock_summands,
870 4 : new_action_summands);
871 : stochastic_specification lps_new_spec(lps_old_spec.data(),
872 : new_actions,
873 : lps_old_spec.global_variables(),
874 : new_process,
875 4 : lps_old_spec.initial_process());
876 8 : return lps_new_spec;
877 4 : }
878 :
879 : } // namespace lps
880 :
881 : } // namespace mcrl2
882 :
883 : namespace std
884 : {
885 : /// \brief Output an action_rename_rule to ostream.
886 : /// \param out An output stream
887 : /// \return The output stream
888 : // Currently, the variables are not printed. The shape is also not parseable. This may be mended.
889 : inline
890 : std::ostream& operator<<(std::ostream& out, const mcrl2::lps::action_rename_rule& r)
891 : {
892 : return out << "(" << r.condition() << ") -> " << r.lhs() << " => " << r.rhs();
893 : }
894 :
895 : /// \brief Output a action_rename_rule to ostream.
896 : /// \param out An output stream
897 : /// \return The output stream
898 : // Currently, the data declaration and the action declaration are not printed.
899 : inline
900 : std::ostream& operator<<(std::ostream& out, const mcrl2::lps::action_rename_specification& s)
901 : {
902 : for(const mcrl2::lps::action_rename_rule& r: s.rules())
903 : {
904 : out << r << "\n";
905 : }
906 : return out;
907 : }
908 :
909 :
910 : } // end namespace std
911 :
912 :
913 : #endif // MCRL2_LPS_ACTION_RENAME_H
|
