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/detail/alphabet_intersection.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_DETAIL_ALPHABET_INTERSECTION_H
      13             : #define MCRL2_PROCESS_DETAIL_ALPHABET_INTERSECTION_H
      14             : 
      15             : #include "mcrl2/process/alphabet.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : namespace detail {
      22             : 
      23             : template <typename Derived, typename Node = alphabet_node>
      24             : struct alphabet_intersection_traverser: public alphabet_traverser<Derived, Node>
      25             : {
      26             :   typedef alphabet_traverser<Derived, Node> super;
      27             :   using super::enter;
      28             :   using super::leave;
      29             :   using super::apply;
      30             :   using super::top;
      31             : 
      32             :   Derived& derived()
      33             :   {
      34             :     return static_cast<Derived&>(*this);
      35             :   }
      36             : 
      37             :   const multi_action_name_set& A;
      38             : 
      39           1 :   alphabet_intersection_traverser(const std::vector<process_equation>& equations, std::set<process_identifier>& W, const multi_action_name_set& A_)
      40           1 :     : super(equations, W), A(A_)
      41           1 :   {}
      42             : 
      43          39 :   void filter()
      44             :   {
      45          39 :     Node& node = top();
      46         429 :     for (multi_action_name_set::iterator i = node.alphabet.begin(); i != node.alphabet.end(); )
      47             :     {
      48         390 :       bool remove = !alphabet_operations::includes(A, *i);
      49         390 :       if (remove)
      50             :       {
      51         172 :         node.alphabet.erase(i++);
      52             :       }
      53             :       else
      54             :       {
      55         218 :         ++i;
      56             :       }
      57             :     }
      58          39 :   }
      59             : 
      60          20 :   void leave(const process::action& x)
      61             :   {
      62          20 :     super::leave(x);
      63          20 :     filter();
      64          20 :   }
      65             : 
      66           0 :   void leave(const process::block& x)
      67             :   {
      68           0 :     throw mcrl2::runtime_error("alphabet_intersection is undefined for expression " + process::pp(x));
      69             :   }
      70             : 
      71           0 :   void leave(const process::hide& x)
      72             :   {
      73           0 :     throw mcrl2::runtime_error("alphabet_intersection is undefined for expression " + process::pp(x));
      74             :   }
      75             : 
      76           0 :   void leave(const process::rename& x)
      77             :   {
      78           0 :     throw mcrl2::runtime_error("alphabet_intersection is undefined for expression " + process::pp(x));
      79             :   }
      80             : 
      81           0 :   void leave(const process::comm& x)
      82             :   {
      83           0 :     throw mcrl2::runtime_error("alphabet_intersection is undefined for expression " + process::pp(x));
      84             :   }
      85             : 
      86           0 :   void leave(const process::allow& x)
      87             :   {
      88           0 :     throw mcrl2::runtime_error("alphabet_intersection is undefined for expression " + process::pp(x));
      89             :   }
      90             : 
      91           0 :   void leave(const process::sync& x)
      92             :   {
      93           0 :     super::leave(x);
      94           0 :     filter();
      95           0 :   }
      96             : 
      97          19 :   void leave(const process::merge& x)
      98             :   {
      99          19 :     super::leave(x);
     100          19 :     filter();
     101          19 :   }
     102             : 
     103           0 :   void leave(const process::left_merge& x)
     104             :   {
     105           0 :     super::leave(x);
     106           0 :     filter();
     107           0 :   }
     108             : };
     109             : 
     110             : struct apply_alphabet_intersection_traverser: public alphabet_intersection_traverser<apply_alphabet_intersection_traverser>
     111             : {
     112             :   typedef alphabet_intersection_traverser<apply_alphabet_intersection_traverser> super;
     113             :   using super::enter;
     114             :   using super::leave;
     115             :   using super::apply;
     116             :   using super::node_stack;
     117             : 
     118           1 :   apply_alphabet_intersection_traverser(const std::vector<process_equation>& equations, std::set<process_identifier>& W, const multi_action_name_set& A)
     119           1 :     : super(equations, W, A)
     120           1 :   {}
     121             : };
     122             : 
     123             : inline
     124           1 : alphabet_node alphabet_intersection(const process_expression& x, const std::vector<process_equation>& equations, std::set<process_identifier>& W, const multi_action_name_set& A)
     125             : {
     126           1 :   apply_alphabet_intersection_traverser f(equations, W, A);
     127           1 :   f.apply(x);
     128           2 :   return f.node_stack.back();
     129           1 : }
     130             : 
     131             : inline
     132           1 : multi_action_name_set alphabet_intersection(const process_expression& x, const std::vector<process_equation>& equations, const multi_action_name_set& A)
     133             : {
     134           1 :   std::set<process_identifier> W;
     135           2 :   return detail::alphabet_intersection(x, equations, W, A).alphabet;
     136           1 : }
     137             : } // namespace detail
     138             : 
     139             : } // namespace process
     140             : 
     141             : } // namespace mcrl2
     142             : 
     143             : #endif // MCRL2_PROCESS_DETAIL_ALPHABET_INTERSECTION_H