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/is_multi_action.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_IS_MULTI_ACTION_H
      13             : #define MCRL2_PROCESS_IS_MULTI_ACTION_H
      14             : 
      15             : #include "mcrl2/process/multi_action_name.h"
      16             : #include "mcrl2/process/traverser.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace process {
      21             : 
      22             : namespace detail {
      23             : 
      24             : struct sync_multi_action_name_traverser: public process_expression_traverser<sync_multi_action_name_traverser>
      25             : {
      26             :   typedef process_expression_traverser<sync_multi_action_name_traverser> super;
      27             :   using super::enter;
      28             :   using super::leave;
      29             :   using super::apply;
      30             : 
      31             :   multi_action_name result;
      32             : 
      33           0 :   void apply(const process::action& x)
      34             :   {
      35           0 :     result.insert(x.label().name());
      36           0 :   }
      37             : };
      38             : 
      39             : } // namespace detail
      40             : 
      41             : /// \brief Returns true if x is a multi action
      42             : inline
      43           0 : bool is_multi_action(const process_expression& x)
      44             : {
      45           0 :   if (is_action(x))
      46             :   {
      47           0 :     return true;
      48             :   }
      49           0 :   if (is_sync(x))
      50             :   {
      51           0 :     const sync& y = atermpp::down_cast<sync>(x);
      52           0 :     return is_multi_action(y.left()) && is_multi_action(y.right());
      53             :   }
      54           0 :   return false;
      55             : }
      56             : 
      57             : /// Computes a multi action name corresponding to a sync (provided that the sync is a pCRL expression).
      58             : inline
      59           0 : multi_action_name sync_multi_action_name(const sync& x)
      60             : {
      61           0 :   detail::sync_multi_action_name_traverser f;
      62           0 :   f.apply(x);
      63           0 :   return f.result;
      64           0 : }
      65             : 
      66             : } // namespace process
      67             : 
      68             : } // namespace mcrl2
      69             : 
      70             : #endif // MCRL2_PROCESS_IS_MULTI_ACTION_H