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.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_ALPHABET_H
      13             : #define MCRL2_PROCESS_ALPHABET_H
      14             : 
      15             : #include "mcrl2/process/alphabet_operations.h"
      16             : #include "mcrl2/process/utility.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace process {
      21             : 
      22             : namespace detail {
      23             : 
      24             : struct alphabet_node
      25             : {
      26             :   multi_action_name_set alphabet;
      27             : 
      28           0 :   alphabet_node()
      29           0 :   {}
      30             : 
      31          74 :   alphabet_node(const multi_action_name_set& alphabet_)
      32          74 :     : alphabet(alphabet_)
      33          74 :   {}
      34             : };
      35             : 
      36             : inline
      37             : std::ostream& operator<<(std::ostream& out, const alphabet_node& x)
      38             : {
      39             :   return out << "alphabet = " << pp(x.alphabet);
      40             : }
      41             : 
      42             : /// \brief Traverser that computes the alphabet of process expressions
      43             : template <typename Derived, typename Node = alphabet_node>
      44             : struct alphabet_traverser: public process_expression_traverser<Derived>
      45             : {
      46             :   typedef process_expression_traverser<Derived> super;
      47             :   using super::enter;
      48             :   using super::leave;
      49             :   using super::apply;
      50             : 
      51           0 :   Derived& derived()
      52             :   {
      53           0 :     return static_cast<Derived&>(*this);
      54             :   }
      55             : 
      56             :   const std::vector<process_equation>& equations;
      57             :   std::set<process_identifier>& W;
      58             :   std::vector<Node> node_stack;
      59             : 
      60          10 :   alphabet_traverser(const std::vector<process_equation>& equations_, std::set<process_identifier>& W_)
      61          10 :     : equations(equations_), W(W_)
      62          10 :   {}
      63             : 
      64             :   // Push a node to node_stack
      65          70 :   void push(const Node& node)
      66             :   {
      67          70 :     mCRL2log(log::trace) << "<push> A = " << pp(node.alphabet) << std::endl;
      68          70 :     node_stack.push_back(node);
      69          70 :   }
      70             : 
      71             :   // Push A to node_stack
      72          70 :   void push(const multi_action_name_set& A)
      73             :   {
      74          70 :     push(Node(A));
      75          70 :   }
      76             : 
      77             :   // Pop the top element of node_stack and return it
      78          60 :   Node pop()
      79             :   {
      80          60 :     Node result = node_stack.back();
      81          60 :     mCRL2log(log::trace) << "<pop> A = " << pp(result.alphabet) << std::endl;
      82          60 :     node_stack.pop_back();
      83          60 :     return result;
      84           0 :   }
      85             : 
      86             :   // Return the top element of node_stack
      87          43 :   Node& top()
      88             :   {
      89          43 :     return node_stack.back();
      90             :   }
      91             : 
      92             :   // Return the top element of node_stack
      93             :   const Node& top() const
      94             :   {
      95             :     return node_stack.back();
      96             :   }
      97             : 
      98             :   // Pops two elements A1 and A2 from the stack, and pushes back union(A1, A2)
      99           6 :   void join()
     100             :   {
     101           6 :     Node right = pop();
     102           6 :     Node left = pop();
     103           6 :     push(alphabet_operations::set_union(left.alphabet, right.alphabet));
     104           6 :   }
     105             : 
     106             :   // Pops two elements A1 and A2 from the stack, and pushes back union(A1, A2, A1 | A2)
     107          22 :   void join_merge()
     108             :   {
     109          22 :     Node right = pop();
     110          22 :     Node left = pop();
     111          22 :     push(alphabet_operations::merge(left.alphabet, right.alphabet));
     112          22 :   }
     113             : 
     114             :   // Pops two elements A1 and A2 from the stack, and pushes back A1 | A2
     115           2 :   void join_sync()
     116             :   {
     117           2 :     Node right = pop();
     118           2 :     Node left = pop();
     119           2 :     push(alphabet_operations::sync(left.alphabet, right.alphabet));
     120           2 :   }
     121             : 
     122          37 :   void leave(const process::action& x)
     123             :   {
     124          37 :     multi_action_name alpha;
     125          37 :     alpha.insert(x.label().name());
     126          37 :     multi_action_name_set A;
     127          37 :     A.insert(alpha);
     128          37 :     push(A);
     129          37 :   }
     130             : 
     131           0 :   void leave(const process::process_instance& x)
     132             :   {
     133             :     using utilities::detail::contains;
     134           0 :     if (!contains(W, x.identifier()))
     135             :     {
     136           0 :       W.insert(x.identifier());
     137           0 :       const process_equation& eqn = find_equation(equations, x.identifier());
     138           0 :       derived().apply(eqn.expression());
     139           0 :       W.erase(x.identifier());
     140             :     }
     141             :     else
     142             :     {
     143           0 :       push(multi_action_name_set());
     144             :     }
     145           0 :   }
     146             : 
     147           0 :   void leave(const process::process_instance_assignment& x)
     148             :   {
     149             :     using utilities::detail::contains;
     150           0 :     if (!contains(W, x.identifier()))
     151             :     {
     152           0 :       W.insert(x.identifier());
     153           0 :       const process_equation& eqn = find_equation(equations, x.identifier());
     154           0 :       derived().apply(eqn.expression());
     155           0 :       W.erase(x.identifier());
     156             :     }
     157             :     else
     158             :     {
     159           0 :       push(multi_action_name_set());
     160             :     }
     161           0 :   }
     162             : 
     163           0 :   void leave(const process::delta& /* x */)
     164             :   {
     165           0 :     push(multi_action_name_set());
     166           0 :   }
     167             : 
     168           1 :   void leave(const process::tau& /* x */)
     169             :   {
     170           1 :     multi_action_name_set A;
     171           1 :     A.insert(multi_action_name()); // A = { tau }
     172           1 :     push(A);
     173           1 :   }
     174             : 
     175           2 :   void leave(const process::sum& /* x */)
     176             :   {
     177           2 :   }
     178             : 
     179           0 :   void leave(const process::block& x)
     180             :   {
     181           0 :     top().alphabet = alphabet_operations::block(x.block_set(), top().alphabet);
     182           0 :   }
     183             : 
     184           0 :   void leave(const process::hide& x)
     185             :   {
     186           0 :     top().alphabet = alphabet_operations::hide(x.hide_set(), top().alphabet);
     187           0 :   }
     188             : 
     189           0 :   void leave(const process::rename& x)
     190             :   {
     191           0 :     top().alphabet = alphabet_operations::rename(x.rename_set(), top().alphabet);
     192           0 :   }
     193             : 
     194           0 :   void leave(const process::comm& x)
     195             :   {
     196           0 :     top().alphabet = alphabet_operations::comm(x.comm_set(), top().alphabet);
     197           0 :   }
     198             : 
     199           2 :   void leave(const process::allow& x)
     200             :   {
     201           2 :     top().alphabet = alphabet_operations::allow(x.allow_set(), top().alphabet);
     202           2 :   }
     203             : 
     204           2 :   void leave(const process::sync& /* x */)
     205             :   {
     206           2 :     join_sync();
     207           2 :   }
     208             : 
     209           0 :   void leave(const process::at& /* x */)
     210             :   {
     211           0 :   }
     212             : 
     213           6 :   void leave(const process::seq& /* x */)
     214             :   {
     215           6 :     join();
     216           6 :   }
     217             : 
     218           0 :   void leave(const process::if_then& /* x */)
     219             :   {
     220           0 :   }
     221             : 
     222           0 :   void leave(const process::if_then_else& /* x */)
     223             :   {
     224           0 :     join();
     225           0 :   }
     226             : 
     227           0 :   void leave(const process::bounded_init& /* x */)
     228             :   {
     229           0 :     join();
     230           0 :   }
     231             : 
     232          22 :   void leave(const process::merge& /* x */)
     233             :   {
     234          22 :     join_merge();
     235          22 :   }
     236             : 
     237           0 :   void leave(const process::left_merge& /* x */)
     238             :   {
     239           0 :     join_merge();
     240           0 :   }
     241             : 
     242           0 :   void leave(const process::choice& /* x */)
     243             :   {
     244           0 :     join();
     245           0 :   }
     246             : };
     247             : 
     248             : struct apply_alphabet_traverser: public alphabet_traverser<apply_alphabet_traverser>
     249             : {
     250             :   typedef alphabet_traverser<apply_alphabet_traverser> super;
     251             :   using super::enter;
     252             :   using super::leave;
     253             :   using super::apply;
     254             :   using super::node_stack;
     255             : 
     256           7 :   apply_alphabet_traverser(const std::vector<process_equation>& equations, std::set<process_identifier>& W)
     257           7 :     : super(equations, W)
     258           7 :   {}
     259             : };
     260             : 
     261             : inline
     262           7 : alphabet_node alphabet(const process_expression& x, const std::vector<process_equation>& equations, std::set<process_identifier>& W)
     263             : {
     264           7 :   detail::apply_alphabet_traverser f(equations, W);
     265           7 :   f.apply(x);
     266          14 :   return f.node_stack.back();
     267           7 : }
     268             : 
     269             : } // namespace detail
     270             : 
     271             : inline
     272           7 : multi_action_name_set alphabet(const process_expression& x, const std::vector<process_equation>& equations)
     273             : {
     274           7 :   std::set<process_identifier> W;
     275          14 :   return detail::alphabet(x, equations, W).alphabet;
     276           7 : }
     277             : 
     278             : } // namespace process
     279             : 
     280             : } // namespace mcrl2
     281             : 
     282             : #endif // MCRL2_PROCESS_ALPHABET_H