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/alphabet_pcrl.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_ALPHABET_PCRL_H
      13             : #define MCRL2_PROCESS_ALPHABET_PCRL_H
      14             : 
      15             : #include "mcrl2/process/detail/pcrl_equation_cache.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : namespace detail {
      22             : 
      23             : /// \brief Traverser that computes the alphabet of pCRL process expressions
      24             : struct alphabet_pcrl_traverser: public process_expression_traverser<alphabet_pcrl_traverser>
      25             : {
      26             :   typedef process_expression_traverser<alphabet_pcrl_traverser> super;
      27             :   using super::enter;
      28             :   using super::leave;
      29             :   using super::apply;
      30             : 
      31             :   const std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache;
      32             :   multi_action_name_set result;
      33             : 
      34           0 :   explicit alphabet_pcrl_traverser(const std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache_)
      35           0 :     : pcrl_equation_cache(pcrl_equation_cache_)
      36           0 :   {}
      37             : 
      38           0 :   void error(const process::process_expression& x) const
      39             :   {
      40           0 :     throw mcrl2::runtime_error("encountered a non-pCRL expression " + process::pp(x) + " in the context of a pCRL expression");
      41             :   }
      42             : 
      43           0 :   void leave(const process::action& x)
      44             :   {
      45           0 :     multi_action_name alpha;
      46           0 :     alpha.insert(x.label().name());
      47           0 :     result.insert(alpha);
      48           0 :   }
      49             : 
      50           0 :   void leave(const process::tau& /* x */)
      51             :   {
      52           0 :     result.insert(multi_action_name());
      53           0 :   }
      54             : 
      55           0 :   void leave(const process::process_instance& x)
      56             :   {
      57           0 :     auto i = pcrl_equation_cache.find(x.identifier());
      58           0 :     if (i == pcrl_equation_cache.end())
      59             :     {
      60           0 :       error(x);
      61             :     }
      62             :     else
      63             :     {
      64           0 :       const multi_action_name_set& A = i->second;
      65           0 :       result.insert(A.begin(), A.end());
      66             :     }
      67           0 :   }
      68             : 
      69           0 :   void leave(const process::process_instance_assignment& x)
      70             :   {
      71           0 :     auto i = pcrl_equation_cache.find(x.identifier());
      72           0 :     if (i == pcrl_equation_cache.end())
      73             :     {
      74           0 :       error(x);
      75             :     }
      76             :     else
      77             :     {
      78           0 :       const multi_action_name_set& A = i->second;
      79           0 :       result.insert(A.begin(), A.end());
      80             :     }
      81           0 :   }
      82             : 
      83           0 :   void leave(const process::block& x)
      84             :   {
      85           0 :     error(x);
      86           0 :   }
      87             : 
      88           0 :   void leave(const process::hide& x)
      89             :   {
      90           0 :     error(x);
      91           0 :   }
      92             : 
      93           0 :   void leave(const process::rename& x)
      94             :   {
      95           0 :     error(x);
      96           0 :   }
      97             : 
      98           0 :   void leave(const process::comm& x)
      99             :   {
     100           0 :     error(x);
     101           0 :   }
     102             : 
     103           0 :   void leave(const process::allow& x)
     104             :   {
     105           0 :     error(x);
     106           0 :   }
     107             : 
     108           0 :   void leave(const process::sync& x)
     109             :   {
     110           0 :     error(x);
     111           0 :   }
     112             : 
     113           0 :   void leave(const process::merge& x)
     114             :   {
     115           0 :     error(x);
     116           0 :   }
     117             : 
     118           0 :   void leave(const process::left_merge& x)
     119             :   {
     120           0 :     error(x);
     121           0 :   }
     122             : };
     123             : 
     124             : } // namespace detail
     125             : 
     126             : /// \brief Computes the alphabet of a pCRL expression x, using a pCRL equation cache
     127             : inline
     128           0 : multi_action_name_set alphabet_pcrl(const process_expression& x, const std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache)
     129             : {
     130           0 :   detail::alphabet_pcrl_traverser f(pcrl_equation_cache);
     131           0 :   f.apply(x);
     132           0 :   return f.result;
     133           0 : }
     134             : 
     135             : } // namespace process
     136             : 
     137             : } // namespace mcrl2
     138             : 
     139             : #endif // MCRL2_PROCESS_ALPHABET_PCRL_H