Balance term structure for parallel composition operator.

libraries/lps/include/mcrl2/lps/linearise.h

@@ -41,6 +41,8 @@ struct t_lin_options
   bool apply_alphabet_axioms;
   bool balance_summands;      // Used to balance long expressions of the shape p1 + p2 + ... + pn. By default the parser delivers
                               // such expressions in a skewed form, causing stack overflow. 
+  bool balance_merge;      // Used to balance long expressions of the shape p1 || p2 || ... || pn. By default the parser
+                         // delivers such expressions in a skewed form, causing stack overflow. 
   mcrl2::data::rewriter::strategy rewrite_strategy;
 
   t_lin_options()

libraries/lps/source/linearise.cpp

@@ -8211,7 +8211,7 @@ class specification_basic_type
       deadlock_summand_vector resultingDeltaSummands;
       deadlock_summands.swap(resultingDeltaSummands);
 
-      bool inline_allow = is_allow || is_block;
+      const bool inline_allow = is_allow || is_block;
       if (inline_allow)
       {
         // Inline allow is only supported for ignore_time,
@@ -11267,12 +11267,18 @@ mcrl2::lps::stochastic_specification mcrl2::lps::linearise(
   mcrl2::process::process_specification input_process=type_checked_spec;
   data_specification data_spec=input_process.data();
 
-  if (lin_options.balance_summands) // Make a balanced tree of long expressions of the shape p1 + p2 + p3 + ... + p4. 
+  if (lin_options.balance_summands) // Make a balanced tree of long expressions of the shape p1 + p2 + p3 + ... + pn. 
                                     // By default the parser provides a skewed tree, and for very long sequences of summands this overflows the
                                     // stack.
   {
     balance_summands(input_process);
   }
+  if (lin_options.balance_merge) // Make a balanced tree of long expressions of the shape p1 || p2 || p3 || ... || pn. 
+                                 // By default the parser provides a skewed tree, and for very long sequences of summands this overflows the
+                                 // stack.
+  {
+    balance_merge(input_process);
+  }  
 
   if (lin_options.apply_alphabet_axioms) // Apply alphabet reduction if requested. 
   {

libraries/process/include/mcrl2/process/alphabet_operations.h

@@ -166,8 +166,7 @@ inline
 multi_action_name_set block(const core::identifier_string_list& B, const multi_action_name_set& A, bool A_includes_subsets = false)
 {
   multi_action_name_set result;
-  multi_action_name beta(B.begin(), B.end());
-
+
   if (A_includes_subsets)
   {
     for (multi_action_name alpha: A)
@@ -184,6 +183,8 @@ multi_action_name_set block(const core::identifier_string_list& B, const multi_a
   }
   else
   {
+    multi_action_name beta(B.begin(), B.end());
+
     for (const multi_action_name& alpha: A)
     {
       if (utilities::detail::has_empty_intersection(beta.begin(), beta.end(), alpha.begin(), alpha.end()))
@@ -249,7 +250,6 @@ multi_action_name hide(const std::set<core::identifier_string>& I, const multi_a
 template <typename IdentifierContainer>
 multi_action_name_set hide(const IdentifierContainer& I, const multi_action_name_set& A, bool /* A_includes_subsets */ = false)
 {
-  multi_action_name m(I.begin(), I.end());
   multi_action_name_set result;
   for (multi_action_name alpha: A)
   {

libraries/process/include/mcrl2/process/balance_nesting_depth.h

@@ -68,6 +68,50 @@ T balance_summands(const T& x, typename std::enable_if<std::is_base_of<atermpp::
   return result;
 }
 
+namespace detail
+{
+struct balance_merge_builder : public process_expression_builder<balance_merge_builder>
+{
+  typedef process_expression_builder<balance_merge_builder> super;
+  using super::apply;
+
+  template <class T>
+  void apply(T& result, const process::merge& x)
+  {
+    std::vector<process_expression> merges = split_merges(x);
+    process_expression new_merge;
+    for (process_expression& merge : merges)
+    {
+      super::apply(new_merge, merge);
+      merge = new_merge;
+    }
+
+    result = utilities::detail::join_balanced<process_expression>(merges.begin(),
+        merges.end(),
+        [](const process::process_expression& x, const process_expression& y) { return merge(x, y); });
+  }
+};
+
+} // namespace detail
+
+/// \brief Reduces the nesting depth of the merge operator
+template <typename T>
+void balance_merge(T& x, typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr)
+{
+  detail::balance_merge_builder f;
+  f.update(x);
+}
+
+/// \brief Reduces the nesting depth of the choice operator
+template <typename T>
+T balance_merge(const T& x, typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr)
+{
+  T result;
+  detail::balance_merge_builder f;
+  f.apply(result, x);
+  return result;
+}
+
 } // namespace process
 
 } // namespace mcrl2