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/utility.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_UTILITY_H
      13             : #define MCRL2_PROCESS_UTILITY_H
      14             : 
      15             : #include "mcrl2/data/substitutions/assignment_sequence_substitution.h"
      16             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      17             : #include "mcrl2/process/multi_action_name.h"
      18             : #include "mcrl2/process/print.h"
      19             : #include "mcrl2/process/replace.h"
      20             : #include "mcrl2/utilities/sequence.h"
      21             : 
      22             : namespace mcrl2 {
      23             : 
      24             : namespace process {
      25             : 
      26             : /// \brief Returns true if x is a pCRL expression. N.B. This test depends on the assumption that
      27             : /// in mCRL2 a top level pCRL expression may never contain a non-pCRL expression.
      28             : inline
      29           2 : bool is_pcrl(const process_expression& x)
      30             : {
      31           2 :   return !is_merge(x) && !is_left_merge(x) && !is_sync(x) && !is_hide(x) && !is_rename(x) && !is_block(x) && !is_allow(x) && !is_comm(x);
      32             : }
      33             : 
      34             : inline
      35             : bool contains_tau(const multi_action_name_set& A)
      36             : {
      37             :   multi_action_name tau;
      38             :   return A.find(tau) != A.end();
      39             : }
      40             : 
      41             : inline
      42           0 : process_expression make_sync(const process_expression& x, const process_expression& y)
      43             : {
      44           0 :   if (is_delta(x) || is_delta(y))
      45             :   {
      46           0 :     return delta();
      47             :   }
      48           0 :   return sync(x, y);
      49             : }
      50             : 
      51             : inline
      52           1 : process_expression make_merge(const process_expression& x, const process_expression& y)
      53             : {
      54           1 :   if (is_delta(x) && is_delta(y))
      55             :   {
      56           0 :     return delta();
      57             :   }
      58           1 :   return merge(x, y);
      59             : }
      60             : 
      61             : inline
      62           0 : process_expression make_left_merge(const process_expression& x, const process_expression& y)
      63             : {
      64           0 :   if (is_delta(y))
      65             :   {
      66           0 :     return delta();
      67             :   }
      68           0 :   return left_merge(x, y);
      69             : }
      70             : 
      71             : inline
      72             : process_expression make_allow(const multi_action_name_set& A, const process_expression& x)
      73             : {
      74             :   if (A.empty())
      75             :   {
      76             :     return delta();
      77             :   }
      78             : 
      79             :   // convert A to an action_name_multiset_list B
      80             :   std::vector<action_name_multiset> v;
      81             :   for (const multi_action_name& alpha: A)
      82             :   {
      83             :     if (!alpha.empty()) // exclude tau
      84             :     {
      85             :       v.push_back(action_name_multiset(core::identifier_string_list(alpha.begin(), alpha.end())));
      86             :     }
      87             :   }
      88             :   action_name_multiset_list B(v.begin(), v.end());
      89             : 
      90             :   return B.empty() ? x : allow(B, x);
      91             : }
      92             : 
      93             : inline
      94           0 : process_expression make_comm(const communication_expression_list& C, const process_expression& x)
      95             : {
      96           0 :   if (C.empty())
      97             :   {
      98           0 :     return x;
      99             :   }
     100             :   else
     101             :   {
     102           0 :     return comm(C, x);
     103             :   }
     104             : }
     105             : 
     106             : inline
     107             : process_expression make_hide(const core::identifier_string_list& I, const process_expression& x)
     108             : {
     109             :   if (I.empty())
     110             :   {
     111             :     return x;
     112             :   }
     113             :   else
     114             :   {
     115             :     return hide(I, x);
     116             :   }
     117             : }
     118             : 
     119             : inline
     120           0 : process_expression make_block(const core::identifier_string_list& B, const process_expression& x)
     121             : {
     122           0 :   if (B.empty())
     123             :   {
     124           0 :     return x;
     125             :   }
     126             :   else
     127             :   {
     128           0 :     return block(B, x);
     129             :   }
     130             : }
     131             : 
     132             : } // namespace process
     133             : 
     134             : } // namespace mcrl2
     135             : 
     136             : #endif // MCRL2_PROCESS_UTILITY_H