mCRL2
Loading...
Searching...
No Matches
action_rename.h
Go to the documentation of this file.
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//
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"
21
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
47namespace mcrl2
48{
49
50namespace lps
51{
52
53// ::= ActionRenameRule(<DataVarId>*, <DataExprOrNil>,
54// <ParamIdOrAction>, <ActionRenameRuleRHS>)
55
58{
59 protected:
62
65
68
71
73 {
74 return is_delta(m_rhs) || is_tau(m_rhs) || process::is_action(m_rhs);
75 }
76
77 public:
80 { }
81
85 {
88 m_variables = atermpp::down_cast<data::variable_list>(*i++);
90 m_lhs = process::action(*i++);
93 }
94
98 const process::action& lhs,
101 {
103 }
104
108 {
109 return m_variables;
110 }
111
115 {
116 return m_variables;
117 }
118
122 {
123 return m_condition;
124 }
125
129 {
130 return m_condition;
131 }
132
135 const process::action& lhs() const // Type should be action, but as it can be a ParamId(identifier_string,data_expression_list),
136 // which is not accepted by the typechecker, this is a temporary fix, until this option
137 // is added to an action.
138 {
139 return m_lhs;
140 }
141
145 {
147 return m_rhs;
148 }
149};
150
151
153// typedef atermpp::term_list<action_rename_rule> action_rename_rule_list;
154
157{
158 protected:
159
162
165
167 std::vector <action_rename_rule> m_rules;
168
169 public:
172 { }
173
177 {
180 m_data = *i++;
181 m_action_labels = atermpp::down_cast<process::action_label_list>((*i++)[0]);
182
183 atermpp::aterm_list rules_list = atermpp::down_cast<atermpp::aterm_list>((*i)[0]);
184 for (const atermpp::aterm& r: rules_list)
185 {
186 m_rules.push_back(action_rename_rule(r));
187 }
188 }
189
197 const std::vector <action_rename_rule>& rules)
198 :
199 m_data(data),
202 { }
203
207 {
208 return m_data;
209 }
210
213 {
214 return m_data;
215 }
216
221 {
222 return m_action_labels;
223 }
224
227 {
228 return m_action_labels;
229 }
230
233 const std::vector<action_rename_rule>& rules() const
234 {
235 return m_rules;
236 }
237
239 std::vector<action_rename_rule>& rules()
240 {
241 return m_rules;
242 }
243
246 bool is_well_typed() const
247 {
248 return true;
249 }
250};
251
252inline
254{
256}
257
258inline
260{
261 std::vector<atermpp::aterm> rules;
262 for (const action_rename_rule& r: spec.rules())
263 {
264 rules.push_back(action_rename_rule_to_aterm(r));
265 }
270 );
271}
272
273}
274}
275
276
277namespace mcrl2
278{
279
280namespace lps
281{
282
284namespace detail
285{
286// Put the equalities t==u in the replacement map as u:=t.
287inline void fill_replacement_map(const data::data_expression& equalities_in_conjunction,
288 std::map<data::data_expression, data::data_expression>& replacement_map)
289{
290 if (equalities_in_conjunction==data::sort_bool::true_())
291 {
292 return;
293 }
294 if (data::sort_bool::is_and_application(equalities_in_conjunction))
295 {
296 fill_replacement_map(data::sort_bool::left(equalities_in_conjunction),replacement_map);
297 fill_replacement_map(data::sort_bool::right(equalities_in_conjunction),replacement_map);
298 return;
299 }
300 if(is_equal_to_application(equalities_in_conjunction))
301 {
302 const data::application a=atermpp::down_cast<data::application>(equalities_in_conjunction);
303 if (a[1]!=a[0])
304 {
305 replacement_map[a[1]]=a[0];
306 }
307 }
308}
309
310// Replace expressions in e according to the replacement map.
311// Assume that e only consists of and, not and equality applied to terms.
312inline data::data_expression replace_expressions(const data::data_expression& e,
313 const std::map<data::data_expression, data::data_expression>& replacement_map)
314{
316 {
317 return data::sort_bool::and_(replace_expressions(data::sort_bool::left(e),replacement_map),
318 replace_expressions(data::sort_bool::right(e),replacement_map));
319 }
321 {
322 return data::sort_bool::not_(replace_expressions(data::sort_bool::arg(e),replacement_map));
323 }
325 {
326 const data::application a=atermpp::down_cast<data::application>(e);
327 return data::application(a.head(),
328 replace_expressions(a[0],replacement_map),
329 replace_expressions(a[1],replacement_map));
330 }
331 const std::map<data::data_expression, data::data_expression>::const_iterator i=replacement_map.find(e);
332 if (i!=replacement_map.end()) // found;
333 {
334 return i->second;
335 }
336 return e;
337}
338
339// Substitute the equalities in equalities_in_conjunction from right to left in e.
340inline data::data_expression substitute_equalities(const data::data_expression& e, const data::data_expression& equalities_in_conjunction)
341{
342 std::map<data::data_expression, data::data_expression> replacement_map;
343 fill_replacement_map(equalities_in_conjunction, replacement_map);
344 return replace_expressions(e,replacement_map);
345}
346
352template <typename IdentifierGenerator>
353void rename_renamerule_variables(data::data_expression& rcond, process::action& rleft, process::action& rright, IdentifierGenerator& generator)
354{
355 data::mutable_map_substitution<> renamings;
356
357 std::set< data::variable > new_vars = data::find_all_variables(rleft.arguments());
358
359 for (const data::variable& v: new_vars)
360 {
361 mcrl2::core::identifier_string new_name = generator(std::string(v.name()));
362
363 if (new_name != v.name())
364 {
365 renamings[v] = data::variable(new_name, v.sort());
366 }
367 }
368
369 data::set_identifier_generator id_generator;
370 for (const data::variable& v: data::substitution_variables(renamings))
371 {
372 id_generator.add_identifier(v.name());
373 }
374 rcond = data::replace_variables_capture_avoiding(rcond, renamings, id_generator);
375 rleft = process::replace_variables_capture_avoiding(rleft, renamings, id_generator);
376 rright = process::replace_variables_capture_avoiding(rright, renamings, id_generator);
377}
378
379/* ------------------------------------------ Normalise sorts ------------------------------------------ */
380
381inline
382void normalize_sorts(action_rename_specification& arspec)
383{
384 arspec.action_labels()=process::normalize_sorts(arspec.action_labels(), arspec.data());
385
386 for (action_rename_rule& rule: arspec.rules())
387 {
388 rule = action_rename_rule(data::normalize_sorts(rule.variables(), arspec.data()),
389 data::normalize_sorts(rule.condition(), arspec.data()),
390 process::normalize_sorts(rule.lhs(), arspec.data()),
391 process::normalize_sorts(rule.rhs(), arspec.data()));
392 }
393}
394
395
396/* ------------------------------------------ Translate user notation ------------------------------------------ */
397
398inline
399void translate_user_notation(action_rename_specification& arspec)
400{
401 for (action_rename_rule& rule: arspec.rules())
402 {
403 rule = action_rename_rule(rule.variables(),
404 data::translate_user_notation(rule.condition()),
407 }
408}
409
410} // namespace detail
412
427inline
429 const action_rename_specification& action_rename_spec,
430 const lps::stochastic_specification& lps_old_spec,
431 const data::rewriter& rewr,
432 const bool enable_rewriting)
433{
434 using namespace mcrl2::core;
435 using namespace mcrl2::data;
436 using namespace mcrl2::lps;
437
438 const std::vector <action_rename_rule>& rename_rules = action_rename_spec.rules();
439 stochastic_action_summand_vector lps_old_action_summands = lps_old_spec.process().action_summands();
440 deadlock_summand_vector lps_deadlock_summands = lps_old_spec.process().deadlock_summands();
441 process::action_list lps_new_actions;
442
444 generator.add_identifiers(lps::find_identifiers(lps_old_spec));
446
447 //go through the rename rules of the rename file
448 mCRL2log(log::debug) << "Rename rules found: " << rename_rules.size() << "\n";
449 for (const action_rename_rule& r: rename_rules)
450 {
451 stochastic_action_summand_vector lps_new_action_summands;
452
453 data_expression rule_condition = r.condition();
454 process::action rule_old_action = r.lhs();
455 process::action rule_new_action;
456 process::process_expression new_element = r.rhs();
457 if (!is_tau(new_element) && !is_delta(new_element))
458 {
459 rule_new_action = atermpp::down_cast<process::action>(new_element);
460 }
461
462 const bool to_tau = is_tau(new_element);
463 const bool to_delta = is_delta(new_element);
464
465 // Check here that the arguments of the rule_old_action only consist
466 // of uniquely occurring variables or closed terms. Furthermore, check that the variables
467 // in rule_new_action and in rule_condition are a subset of those in
468 // rule_old_action. This check ought to be done in the static checking
469 // part of the renaming rules, but as yet it has nog been done. Ultimately
470 // this check should be moved there.
471
472 // first check that the arguments of rule_old_action are variables or closed
473 // terms.
474
475 for (const data_expression& rule_old_argument_i: rule_old_action.arguments())
476 {
477 if (!is_variable(rule_old_argument_i) &&
478 (!(data::find_all_variables(rule_old_argument_i).empty())))
479 {
480 throw mcrl2::runtime_error("The arguments of the lhs " + process::pp(rule_old_action) +
481 " are not variables or closed expressions");
482 }
483 }
484
485 // Check whether the variables in rhs are included in the lefthandside.
486 std::set < variable > variables_in_old_rule = process::find_free_variables(rule_old_action);
487 std::set < variable > variables_in_new_rule = process::find_free_variables(rule_new_action);
488
489 if (!includes(variables_in_old_rule.begin(),variables_in_old_rule.end(),
490 variables_in_new_rule.begin(),variables_in_new_rule.end()))
491 {
492 throw mcrl2::runtime_error("There are variables occurring in rhs " + process::pp(rule_new_action) +
493 " of a rename rule not occurring in lhs " + process::pp(rule_old_action));
494 }
495
496 // Check whether the variables in condition are included in the lefthandside.
497 std::set < variable > variables_in_condition = data::find_free_variables(rule_condition);
498 if (!includes(variables_in_old_rule.begin(),variables_in_old_rule.end(),
499 variables_in_condition.begin(),variables_in_condition.end()))
500 {
501 throw mcrl2::runtime_error("There are variables occurring in the condition " + data::pp(rule_condition) +
502 " of a rename rule not occurring in lhs " + process::pp(rule_old_action));
503 }
504
505 // check for double occurrences of variables in the lhs. Note that variables_in_old_rule
506 // is empty at the end.
507 for (const data_expression& d: rule_old_action.arguments())
508 {
509 if (is_variable(d))
510 {
511 const variable& v = atermpp::down_cast<variable>(d);
512 if (variables_in_old_rule.find(v)==variables_in_old_rule.end())
513 {
514 throw mcrl2::runtime_error("Variable " + data::pp(v) + " occurs more than once in lhs " +
515 process::pp(rule_old_action) + " of an action rename rule");
516 }
517 else
518 {
519 variables_in_old_rule.erase(v);
520 }
521 }
522 }
523 assert(variables_in_old_rule.empty());
524
525
526 //go through the summands of the old lps
527 mCRL2log(log::debug) << "Action summands found: " << lps_old_action_summands.size() << "\n";
528 for (const stochastic_action_summand& lps_old_action_summand: lps_old_action_summands)
529 {
530 process::action_list lps_old_actions = lps_old_action_summand.multi_action().actions();
531
532 /* For each individual action in the multi-action, for which the
533 rename rule applies, two new summands must be made, namely one
534 where the rule does not match with the parameters of the action,
535 and one where it actually does. This means that for a multiaction
536 with k summands 2^k new summands can result. */
537
538 std::vector < variable_list >
539 lps_new_sum_vars(1,lps_old_action_summand.summation_variables());
540 std::vector < data_expression > lps_new_condition(1,lps_old_action_summand.condition());
541 std::vector < process::action_list >
542 lps_new_actions(1,process::action_list());
543 std::vector < bool > lps_new_actions_is_delta(1,false);
544
545 mCRL2log(log::debug) << "Actions in summand found: " << lps_old_actions.size() << "\n";
546 for (const process::action& lps_old_action: lps_old_actions)
547 {
548 if (equal_signatures(lps_old_action, rule_old_action))
549 {
550 mCRL2log(log::debug) << "Renaming action " << rule_old_action << "\n";
551
552 //rename all previously used variables.
553 data_expression renamed_rule_condition=rule_condition;
554 process::action renamed_rule_old_action=rule_old_action;
555 process::action renamed_rule_new_action=rule_new_action;
556 detail::rename_renamerule_variables(renamed_rule_condition, renamed_rule_old_action, renamed_rule_new_action, generator);
557
558 //go through the arguments of the action.
559 data_expression_list::iterator lps_old_argument_i = lps_old_action.arguments().begin();
560 data_expression new_equalities_condition=sort_bool::true_();
561 for (const data_expression& rule_old_argument_i: renamed_rule_old_action.arguments())
562 {
563 if (is_variable(rule_old_argument_i))
564 {
565 new_equalities_condition=lazy::and_(new_equalities_condition,
566 data::equal_to(rule_old_argument_i, *lps_old_argument_i));
567 }
568 else
569 {
570 assert((data::find_all_variables(rule_old_argument_i).empty())); // the argument must be closed, which is checked above.
571 renamed_rule_condition=
572 lazy::and_(renamed_rule_condition,
573 data::equal_to(rule_old_argument_i, *lps_old_argument_i));
574 if (enable_rewriting) renamed_rule_condition=rewr(renamed_rule_condition); // Make sure that renamed_rule_condition is as simple as possible.
575 }
576 lps_old_argument_i++;
577 }
578
579 /* insert the new equality condition in all the newly generated summands */
580 for (data_expression& d: lps_new_condition)
581 {
582 d=lazy::and_(d,new_equalities_condition);
583 }
584
585 /* insert the new sum variables in all the newly generated summands */
586 std::set<variable> new_vars = find_all_variables(renamed_rule_old_action);
587 for (const variable& sdvi: new_vars)
588 {
589 for (variable_list& l: lps_new_sum_vars)
590 {
591 l.push_front(sdvi);
592 }
593 }
594
595 if (enable_rewriting) renamed_rule_condition=rewr(renamed_rule_condition); // Make sure that renamed_rule_condition is as simple as possible.
596 if (renamed_rule_condition==sort_bool::true_())
597 {
598 if (to_delta)
599 {
600 std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
601 for (process::action_list& l: lps_new_actions)
602 {
603 l=process::action_list(); // the action becomes delta
604 *i_is_delta=true;
605 ++i_is_delta;
606 }
607 }
608 else if (!to_tau)
609 {
610 std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
611 for (process::action_list& l: lps_new_actions)
612 {
613 if (!*i_is_delta) // the action is not delta
614 {
615 l.push_front(renamed_rule_new_action);
616 }
617 ++i_is_delta;
618 }
619 }
620 }
621 else if (renamed_rule_condition==sort_bool::false_())
622 {
623 std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
624 for (process::action_list& l: lps_new_actions)
625 {
626 if (!*i_is_delta) // The action does not equal delta.
627 {
628 l.push_front(lps_old_action);
629 }
630 ++i_is_delta;
631 }
632
633 }
634 else
635 {
636 /* Duplicate summands, one where the renaming is applied, and one where it is not
637 applied. */
638
639 std::vector < process::action_list > lps_new_actions_temp(lps_new_actions);
640
641 if (!to_tau) // if the new element is tau, we do not insert it in the multi-action.
642 {
643 std::vector < bool >::iterator i_is_delta=lps_new_actions_is_delta.begin();
644 for (process::action_list& l: lps_new_actions)
645 {
646 if (to_delta)
647 {
649 *i_is_delta=true;
650 }
651 else
652 {
653 l.push_front(renamed_rule_new_action);
654 *i_is_delta=false;
655 }
656 ++i_is_delta;
657 }
658 }
659
660 for (process::action_list& l: lps_new_actions_temp)
661 {
662 lps_new_actions_is_delta.push_back(false); // A non renamed action is not delta;
663 l.push_front(lps_old_action);
664 }
665
666 lps_new_actions.insert(lps_new_actions.end(),
667 lps_new_actions_temp.begin(),
668 lps_new_actions_temp.end());
669 assert(lps_new_actions_is_delta.size()==lps_new_actions.size());
670
671 /* lps_new_condition_temp will contain the conditions in conjunction with
672 the negated new_condition. It will be concatenated to lps_new_condition,
673 in which the terms will be conjoined with the non-negated new_condition */
674
675 std::vector < data_expression > lps_new_condition_temp(lps_new_condition);
676
677 for (data_expression& d: lps_new_condition)
678 {
679 // substitute the equalities in d in renamed_rule_condition.
680 d=lazy::and_(renamed_rule_condition,detail::substitute_equalities(d,renamed_rule_condition));
681 }
682
683 for (const data_expression& d: lps_new_condition_temp)
684 {
685
686 lps_new_condition.push_back(lazy::and_(d,sort_bool::not_(renamed_rule_condition)));
687 }
688
689 // Replace lps_new_sum_vars with two consecutive copies of itself.
690 // The clumsily looking method below is required, to avoid problems with vector reallocation.
691 std::size_t size=lps_new_sum_vars.size();
692 lps_new_sum_vars.reserve(2*size);
693 for(std::size_t i=0; i<size; ++i)
694 {
695 lps_new_sum_vars.push_back(lps_new_sum_vars[i]);
696 }
697 }
698 }//end if(equal_signatures(...))
699 else
700 {
701 for (process::action_list& l: lps_new_actions)
702 {
703 l.push_front(lps_old_action);
704 }
705 }
706 mCRL2log(log::debug) << "Action done\n";
707
708 } //end of action list iterator
709
710 /* Add the summands to lps_new_action_summands or to the deadlock summands*/
711
712 std::vector < process::action_list > :: iterator i_act=lps_new_actions.begin();
713 std::vector < bool > :: iterator i_act_is_delta=lps_new_actions_is_delta.begin();
714 std::vector < variable_list > :: iterator i_sumvars=lps_new_sum_vars.begin();
715 for (const data_expression& cond: lps_new_condition)
716 {
717 //create a summand for the new lps
718 if (*i_act_is_delta)
719 {
720 // Create a deadlock summand.
721 const deadlock_summand d(*i_sumvars,
722 cond,
723 deadlock(lps_old_action_summand.multi_action().time()));
724 lps_deadlock_summands.push_back(d);
725 }
726 else
727 {
728 // create an action summand.
729 stochastic_action_summand lps_new_summand(*i_sumvars,
730 cond,
731 multi_action(reverse(*i_act), lps_old_action_summand.multi_action().time()),
732 lps_old_action_summand.assignments(),
733 lps_old_action_summand.distribution());
734 lps_new_action_summands.push_back(lps_new_summand);
735 }
736 i_act++;
737 i_sumvars++;
738 ++i_act_is_delta;
739 }
740 } // end of summand list iterator
741 lps_old_action_summands = lps_new_action_summands;
742 } //end of rename rule iterator
743
744 mCRL2log(log::debug) << "Simplifying the result...\n";
745
746 stochastic_linear_process new_process(lps_old_spec.process().process_parameters(),
747 lps_deadlock_summands,
748 lps_old_action_summands);
749
750 // add action_rename_spec.action_labels to action_rename_spec.action_labels without adding duplicates.
751 process::action_label_list all=action_rename_spec.action_labels();
752 for (const process::action_label& a: lps_old_spec.action_labels())
753 {
754 if (std::find(action_rename_spec.action_labels().begin(),
755 action_rename_spec.action_labels().end(),a)==action_rename_spec.action_labels().end())
756 {
757 // Not found;
758 all.push_front(a);
759 }
760 }
761 stochastic_specification lps_new_spec(action_rename_spec.data(), // This contains the data of the lps and the rename file.
762 all,
763 lps_old_spec.global_variables(),
764 new_process,
765 lps_old_spec.initial_process());
766
767 mCRL2log(log::debug) << "New lps complete\n";
768 return lps_new_spec;
769} //end of rename(...)
770
771namespace detail
772{
773
774inline
775process::action_label rename_action_label(const process::action_label& act, const std::regex& matching_regex, const std::string& replacing_fmt)
776{
777 return process::action_label(std::regex_replace(std::string(act.name()), matching_regex, replacing_fmt), act.sorts());
778}
779
780} // namespace detail
781
786inline
788 const std::regex& matching_regex,
789 const std::string& replacing_fmt,
790 const stochastic_specification& lps_old_spec)
791{
792 // Use a set to store the new action labels to avoid duplicates
793 std::set<process::action_label> new_actions_set;
794 process::action_label_list new_actions;
795 for(const process::action_label& act: lps_old_spec.action_labels())
796 {
797 process::action_label new_action_label(detail::rename_action_label(act, matching_regex, replacing_fmt));
798 if (std::string(new_action_label.name()).empty())
799 {
800 throw mcrl2::runtime_error("After renaming the action " + std::string(act.name()) + " becomes empty, which is not allowed.");
801 }
802 if(std::string(new_action_label.name()) != "delta" && std::string(new_action_label.name()) != "tau" &&
803 new_actions_set.find(new_action_label) == new_actions_set.end())
804 {
805 // The list of actions should not contain delta and tau actions and also no duplicates.
806 new_actions_set.insert(new_action_label);
807 new_actions.push_front(new_action_label);
808 }
809 }
810 new_actions = reverse(new_actions);
811
812 // The list of new actions summands is initially empty
813 std::vector<stochastic_action_summand> new_action_summands;
814 // The list of new deadlock summands is initialised to the existing list, we will only add new deadlock summands
815 std::vector<deadlock_summand> new_deadlock_summands(lps_old_spec.process().deadlock_summands());
816 for(const stochastic_action_summand& as: lps_old_spec.process().action_summands())
817 {
818 process::action_list new_action_list;
819 bool becomes_deadlock_summand = false;
820 for(const process::action& act: as.multi_action().actions())
821 {
822 process::action_label new_action_label(detail::rename_action_label(act.label(), matching_regex, replacing_fmt));
823 if(std::string(new_action_label.name()) == "delta")
824 {
825 // delta is the absorbing element for multi action concatenation
826 // Therefore, this summand now becomes a deadlock summand
827 becomes_deadlock_summand = true;
828 break;
829 }
830 // tau is the identity for multi action concatenation
831 // therefore, we should not add it to a multi action
832 if(std::string(new_action_label.name()) != "tau")
833 {
834 new_action_list.push_front(process::action(new_action_label, act.arguments()));
835 }
836 }
837
838 if(!becomes_deadlock_summand)
839 {
840 new_action_list = reverse(new_action_list);
841 multi_action new_multi_action(new_action_list, as.multi_action().time());
842
843 // Copy most of the old information, only the multi action has changed
844 stochastic_action_summand new_summand(as.summation_variables(), as.condition(), new_multi_action, as.assignments(), as.distribution());
845 new_action_summands.push_back(new_summand);
846 }
847 else
848 {
849 // Add a new deadlock summand, copying most of the information for the old action summand
850 new_deadlock_summands.push_back(deadlock_summand(as.summation_variables(), as.condition(), deadlock(as.multi_action().time())));
851 }
852 }
853
854 stochastic_linear_process new_process(lps_old_spec.process().process_parameters(),
855 new_deadlock_summands,
856 new_action_summands);
857 stochastic_specification lps_new_spec(lps_old_spec.data(),
858 new_actions,
859 lps_old_spec.global_variables(),
860 new_process,
861 lps_old_spec.initial_process());
862 return lps_new_spec;
863}
864
865} // namespace lps
866
867} // namespace mcrl2
868
869namespace std
870{
874// Currently, the variables are not printed. The shape is also not parseable. This may be mended.
875inline
876std::ostream& operator<<(std::ostream& out, const mcrl2::lps::action_rename_rule& r)
877{
878 return out << "(" << r.condition() << ") -> " << r.lhs() << " => " << r.rhs();
879}
880
884// Currently, the data declaration and the action declaration are not printed.
885inline
886std::ostream& operator<<(std::ostream& out, const mcrl2::lps::action_rename_specification& s)
887{
888 for(const mcrl2::lps::action_rename_rule& r: s.rules())
889 {
890 out << r << "\n";
891 }
892 return out;
893}
894
895
896} // end namespace std
897
898
899#endif // MCRL2_LPS_ACTION_RENAME_H
Term containing a string.
const_iterator begin() const
Returns an iterator pointing to the first argument.
Definition aterm.h:165
Iterator for term_appl.
Iterator for term_list.
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
void add_identifiers(const std::set< core::identifier_string > &ids)
Add a set of identifiers to the context.
Rewriter that operates on data expressions.
Definition rewriter.h:81
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief A data variable
Definition variable.h:28
const data::data_expression & condition() const
Returns the condition of the rule.
const process::process_expression & rhs() const
Returns the right hand side of the rule.
data::data_expression & condition()
Returns the condition of the rule.
action_rename_rule(const data::variable_list &variables, const data::data_expression &condition, const process::action &lhs, const process::process_expression &rhs)
Constructor.
process::process_expression m_rhs
right hand side of the rule. Can only be an action, tau or delta.
data::variable_list m_variables
The data variables of the rule.
bool check_that_rhs_is_tau_delta_or_an_action() const
data::variable_list & variables()
Returns the variables of the rule.
process::action m_lhs
The left hand side of the rule.
action_rename_rule(const atermpp::aterm &t)
Constructor.
data::data_expression m_condition
The condition of the rule.
const data::variable_list & variables() const
Returns the variables of the rule.
const process::action & lhs() const
Returns the left hand side of the rule.
Read-only singly linked list of action rename rules.
const std::vector< action_rename_rule > & rules() const
Returns the action rename rules.
data::data_specification m_data
The data specification of the action rename specification.
process::action_label_list & action_labels()
Returns the sequence of action labels.
std::vector< action_rename_rule > m_rules
The action rename rules of the action rename specification.
action_rename_specification(const data::data_specification &data, const process::action_label_list &action_labels, const std::vector< action_rename_rule > &rules)
Constructor.
std::vector< action_rename_rule > & rules()
Returns the action rename rules.
data::data_specification & data()
Returns the data specification.
process::action_label_list m_action_labels
The action labels of the action rename specification.
const data::data_specification & data() const
Returns the data action_rename_specification.
const process::action_label_list & action_labels() const
Returns the sequence of action labels.
action_rename_specification(atermpp::aterm t)
Constructor.
bool is_well_typed() const
Indicates whether the action_rename_specification is well typed.
LPS summand containing a deadlock.
Represents a deadlock.
Definition deadlock.h:26
const std::vector< ActionSummand > & action_summands() const
Returns the sequence of action summands.
const deadlock_summand_vector & deadlock_summands() const
Returns the sequence of deadlock summands.
const data::variable_list & process_parameters() const
Returns the sequence of process parameters.
\brief A timed multi-action
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the LPS.
const process::action_label_list & action_labels() const
Returns a sequence of action labels. This sequence contains all action labels occurring in the specif...
const InitialProcessExpression & initial_process() const
Returns the initial process.
const LinearProcess & process() const
Returns the linear process of the specification.
const data::data_specification & data() const
Returns the data specification.
LPS summand containing a multi-action.
\brief An action label
const core::identifier_string & name() const
const data::data_expression_list & arguments() const
\brief A process expression
Standard exception class for reporting runtime errors.
Definition exception.h:27
Parse mCRL2 specifications and expressions.
The class rewriter.
@ act
Definition linearise.cpp:78
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
add your file description here.
bool check_rule_ActionRenameSpec(const Term &t)
const atermpp::function_symbol & function_symbol_ActionRenameRule()
bool check_rule_ActionRenameRule(const Term &t)
const atermpp::function_symbol & function_symbol_ActionRenameRules()
const atermpp::function_symbol & function_symbol_ActSpec()
const atermpp::function_symbol & function_symbol_ActionRenameSpec()
atermpp::aterm data_specification_to_aterm(const data_specification &s)
Definition data_io.cpp:44
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition bool.h:469
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition bool.h:493
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:235
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
Definition bool.h:281
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
Definition bool.h:217
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition bool.h:481
Namespace for all data library functionality.
Definition abstraction.h:22
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:90
std::set< data::variable > find_all_variables(const data::data_expression &x)
Definition data.cpp:94
std::set< data::variable > substitution_variables(const Substitution &)
Returns the variables appearing in the right hand sides of the substitution.
Definition replace.h:161
std::string pp(const abstraction &x)
Definition data.cpp:39
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
std::set< core::identifier_string > function_and_mapping_identifiers(const data_specification &dataspec)
Returns the names of functions and mappings that occur in a data specification.
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
bool is_equal_to_application(const DataExpression &e)
Recogniser for application of ==.
Definition standard.h:155
process::action_label rename_action_label(const process::action_label &act, const std::regex &matching_regex, const std::string &replacing_fmt)
The main namespace for the LPS library.
std::vector< stochastic_action_summand > stochastic_action_summand_vector
\brief vector of stochastic_action_summands
std::vector< deadlock_summand > deadlock_summand_vector
\brief vector of deadlock_summands
lps::stochastic_specification action_rename(const action_rename_specification &action_rename_spec, const lps::stochastic_specification &lps_old_spec, const data::rewriter &rewr, const bool enable_rewriting)
Rename the actions in a linear specification using a given action_rename_spec.
void find_identifiers(const T &x, OutputIterator o)
Definition find.h:96
atermpp::aterm action_rename_specification_to_aterm(const action_rename_specification &spec)
atermpp::aterm action_rename_rule_to_aterm(const action_rename_rule &rule)
std::set< data::variable > find_all_variables(const lps::deadlock &x)
Definition lps.cpp:48
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator, typename std::enable_if<!std::is_base_of< atermpp::aterm, T >::value >::type *=nullptr)
action_label_list normalize_sorts(const action_label_list &x, const data::sort_specification &sortspec)
Definition process.cpp:67
bool is_action(const atermpp::aterm &x)
std::string pp(const action_label &x)
Definition process.cpp:36
atermpp::term_list< action > action_list
\brief list of actions
void find_free_variables(const T &x, OutputIterator o)
Definition find.h:150
action translate_user_notation(const action &x)
Definition process.cpp:70
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
STL namespace.
std::ostream & operator<<(std::ostream &out, const mcrl2::lps::action_rename_rule &r)
Output an action_rename_rule to ostream.
add your file description here.
add your file description here.
add your file description here.