Check whether renamed action becomes empty

Also slightly improved documentation
Fixes #1690

doc/sphinx/user_manual/tools/release/lpsactionrename.rst

@@ -123,7 +123,9 @@ Applying sum elimination will give the following result::
 Regular Expressions
 -------------------
 
-A regular expression has to be provided in the shape ``matching pattern/replacement``.
+Many action labels can be quickly renamed at once with a regular expression.
+This regular expression has to be provided in the shape ``matching pattern/replacement``.
+Note that this does not allow modification of action parameters.
 The replacement pattern follows the standard of ECMAScript. Groups matched with
 parentheses can be substituted in the replacement string using ``$n``, where
 ``n`` is the index of the matched group. See the
@@ -149,9 +151,10 @@ We consider the following process::
            delta;
 
 We can remove the prefix of ``a_out`` and ``c_out`` using the regular expression
-``^([^b])_out$/$1``. It is generally a good idea to write regular expressions in
-the shape ``^expression$`` to ensure the whole action name is matched.
+``^([^b])_out$/$1``. To ensure the whole action name is matched, one may write
+regular expressions in the shape ``^expression$``.
 
 It is also possible to rename actions to delta or to tau. For example, when
 renaming ``a_out`` to ``delta`` using ``^a_out$/delta``, the multi action
-``a_out|c_out`` will become ``delta``.
+``a_out|c_out`` will become ``delta``. When applying the regex ``a_out/tau``,
+the same multi-action becomes ``c_out``.

libraries/lps/include/mcrl2/lps/action_rename.h

@@ -804,6 +804,10 @@ stochastic_specification action_rename(
   for(const process::action_label& act: lps_old_spec.action_labels())
   {
     process::action_label new_action_label(detail::rename_action_label(act, matching_regex, replacing_fmt));
+    if (std::string(new_action_label.name()).empty())
+    {
+      throw mcrl2::runtime_error("After renaming the action " + std::string(act.name()) + " becomes empty, which is not allowed.");
+    }
     if(std::string(new_action_label.name()) != "delta" && std::string(new_action_label.name()) != "tau" &&
         new_actions_set.find(new_action_label) == new_actions_set.end())
     {