Include file:

#include "mcrl2/lps/action_rename.h"

Action rename specifications.


lps::stochastic_specification mcrl2::lps::action_rename(const action_rename_specification &action_rename_spec, const lps::stochastic_specification &lps_old_spec)

Rename the actions in a linear specification using a given action_rename_spec.

The actions in a linear specification are renamed according to a given action rename specification. Note that the rules are applied in the order they appear in the specification. This yield quite elaborate conditions in the resulting lps, as a latter rule can only be applied if an earlier rule is not applicable. Note also that there is always a default summand, where the action is not renamed. Using sum elimination and rewriting a substantial reduction of the conditions that are generated can be obtained, often allowing many summands to be removed.


  • action_rename_spec The action_rename_specification to be used.
  • lps_old_spec The input linear specification.

Returns: The lps_old_spec where all actions have been renamed according to action_rename_spec.

stochastic_specification mcrl2::lps::action_rename(const std::regex &matching_regex, const std::string &replacing_fmt, const stochastic_specification &lps_old_spec)

Rename actions in given specification based on a regular expression and a string that specifies how the replacement should be formatted.

atermpp::aterm_appl mcrl2::lps::action_rename_rule_to_aterm(const action_rename_rule &rule)
atermpp::aterm_appl mcrl2::lps::action_rename_specification_to_aterm(const action_rename_specification &spec)


process::action_label mcrl2::lps::detail::rename_action_label(const process::action_label &act, const std::regex &matching_regex, const std::string &replacing_fmt)