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_efficient.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_ALPHABET_EFFICIENT_H
      13             : #define MCRL2_PROCESS_ALPHABET_EFFICIENT_H
      14             : 
      15             : #include "mcrl2/process/alphabet.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : namespace detail {
      22             : 
      23             : /// \brief Traverser that computes the alphabet of process expressions. This version should be more efficient than the default one.
      24             : template <typename Derived, typename Node = alphabet_node>
      25             : struct alphabet_efficient_traverser: public alphabet_traverser<Derived>
      26             : {
      27             :   typedef alphabet_traverser<Derived> super;
      28             :   using super::enter;
      29             :   using super::leave;
      30             :   using super::apply;
      31             :   using super::W;
      32             :   using super::push;
      33             : 
      34           2 :   Derived& derived()
      35             :   {
      36           2 :     return static_cast<Derived&>(*this);
      37             :   }
      38             : 
      39           2 :   alphabet_efficient_traverser(const std::vector<process_equation>& equations, std::set<process_identifier>& W)
      40           2 :     : super(equations, W)
      41           2 :   {}
      42             : 
      43             :   // N.B. In this version no elements from W are removed. This should be fine except for parallel expressions.
      44           4 :   void leave(const process::process_instance& x)
      45             :   {
      46             :     using utilities::detail::contains;
      47           4 :     if (!contains(W, x.identifier()))
      48             :     {
      49           2 :       W.insert(x.identifier());
      50           2 :       const process_equation& eqn = find_equation(super::equations, x.identifier());
      51           2 :       derived().apply(eqn.expression());
      52             :       // W.erase(x.identifier());
      53             :     }
      54             :     else
      55             :     {
      56           2 :       push(multi_action_name_set());
      57             :     }
      58           4 :   }
      59             : 
      60           0 :   void leave(const process::process_instance_assignment& x)
      61             :   {
      62             :     using utilities::detail::contains;
      63           0 :     if (!contains(W, x.identifier()))
      64             :     {
      65           0 :       W.insert(x.identifier());
      66           0 :       const process_equation& eqn = find_equation(super::equations, x.identifier());
      67           0 :       derived().apply(eqn.expression());
      68             :       // W.erase(x.identifier());
      69             :     }
      70             :     else
      71             :     {
      72           0 :       push(multi_action_name_set());
      73             :     }
      74           0 :   }
      75             : 
      76             :   // For parallel expressions, the value of W is reset after finishing the left operand.
      77             :   template <typename T>
      78           0 :   void apply_parallel_operator(const T& x, const process_expression& left, const process_expression& right)
      79             :   {
      80           0 :     derived().enter(x);
      81           0 :     auto Wcopy = W;
      82           0 :     derived().apply(left);
      83           0 :     W = Wcopy;
      84           0 :     derived().apply(right);
      85           0 :     derived().leave(x);
      86           0 :   }
      87             : 
      88           0 :   void apply(const process::merge& x)
      89             :   {
      90           0 :     apply_parallel_operator(x, x.left(), x.right());
      91           0 :   }
      92             : 
      93           0 :   void apply(const process::left_merge& x)
      94             :   {
      95           0 :     apply_parallel_operator(x, x.left(), x.right());
      96           0 :   }
      97             : 
      98           0 :   void apply(const process::sync& x)
      99             :   {
     100           0 :     apply_parallel_operator(x, x.left(), x.right());
     101           0 :   }
     102             : };
     103             : 
     104             : struct apply_alphabet_efficient_traverser: public alphabet_efficient_traverser<apply_alphabet_efficient_traverser>
     105             : {
     106             :   typedef alphabet_efficient_traverser<apply_alphabet_efficient_traverser> super;
     107             :   using super::enter;
     108             :   using super::leave;
     109             :   using super::apply;
     110             :   using super::node_stack;
     111             : 
     112           2 :   apply_alphabet_efficient_traverser(const std::vector<process_equation>& equations, std::set<process_identifier>& W)
     113           2 :     : super(equations, W)
     114           2 :   {}
     115             : };
     116             : 
     117             : inline
     118           2 : alphabet_node alphabet_efficient(const process_expression& x, const std::vector<process_equation>& equations, std::set<process_identifier>& W)
     119             : {
     120           2 :   detail::apply_alphabet_efficient_traverser f(equations, W);
     121           2 :   f.apply(x);
     122           4 :   return f.node_stack.back();
     123           2 : }
     124             : 
     125             : } // namespace detail
     126             : 
     127             : inline
     128           2 : multi_action_name_set alphabet_efficient(const process_expression& x, const std::vector<process_equation>& equations)
     129             : {
     130           2 :   std::set<process_identifier> W;
     131           4 :   return detail::alphabet_efficient(x, equations, W).alphabet;
     132           2 : }
     133             : 
     134             : } // namespace process
     135             : 
     136             : } // namespace mcrl2
     137             : 
     138             : #endif // MCRL2_PROCESS_ALPHABET_EFFICIENT_H