Line data    Source code

       1             : // Author(s): 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/process/join.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_JOIN_H
      13             : #define MCRL2_PROCESS_JOIN_H
      14             : 
      15             : #include "mcrl2/process/process_expression.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : /// \brief Splits a choice into a set of operands
      22             : /// Given a process expression of the form p1 + p2 + .... + pn, this will yield a
      23             : /// set of the form { p1, p2, ..., pn }, assuming that pi does not have a + as main
      24             : /// function symbol.
      25             : /// \param x A process expression.
      26             : /// \return A set of process expressions.
      27             : inline
      28           1 : std::vector<process_expression> split_summands(const process_expression& x)
      29             : {
      30           1 :   std::vector<process_expression> result;
      31           1 :   utilities::detail::split(x,
      32             :                            std::back_inserter(result),
      33             :                            is_choice,
      34         100 :                            [](const process_expression& x) { return atermpp::down_cast<choice>(x).left(); },
      35         100 :                            [](const process_expression& x) { return atermpp::down_cast<choice>(x).right(); }
      36             :                           );
      37           1 :   return result;
      38           0 : }
      39             : 
      40             : /// \brief Returns or applied to the sequence of process expressions [first, last).
      41             : /// \param first Start of a sequence of process expressions.
      42             : /// \param last End of a sequence of of process expressions.
      43             : /// \return The choice operator applied to the sequence of process expressions [first, last).
      44             : template<typename FwdIt>
      45             : process_expression join_summands(FwdIt first, FwdIt last)
      46             : {
      47             :   process_expression delta_ = delta();
      48             :   return utilities::detail::join(first, last, [](const process_expression& x, const process_expression& y) {
      49             :       return choice(x, y);
      50             :   }, delta_);
      51             : }
      52             : 
      53             : } // namespace process
      54             : 
      55             : } // namespace mcrl2
      56             : 
      57             : #endif // MCRL2_PROCESS_JOIN_H