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/expand_process_instance_assignments.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_EXPAND_PROCESS_INSTANCE_ASSIGNMENTS_H
      13             : #define MCRL2_PROCESS_EXPAND_PROCESS_INSTANCE_ASSIGNMENTS_H
      14             : 
      15             : #include "mcrl2/process/utility.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : namespace detail {
      22             : 
      23             : struct expand_process_instance_assignments_builder: public process_expression_builder<expand_process_instance_assignments_builder>
      24             : {
      25             :   typedef process_expression_builder<expand_process_instance_assignments_builder> super;
      26             :   using super::enter;
      27             :   using super::leave;
      28             :   using super::apply;
      29             :   using super::update;
      30             : 
      31             :   const std::vector<process_equation>& equations;
      32             : 
      33             :   explicit expand_process_instance_assignments_builder(const std::vector<process_equation>& equations_)
      34             :     : equations(equations_)
      35             :   {}
      36             : 
      37             :   /// \brief Converts a process instance P(e) into p[d := e], where P(d) = p is the equation
      38             :   /// corresponding to P.
      39             :   template <class T>
      40             :   void apply(T& result, const process::process_instance& x)
      41             :   {
      42             :     const process_equation& eqn = find_equation(equations, x.identifier());
      43             :     const process_expression& p = eqn.expression();
      44             :     data::mutable_map_substitution<> sigma;
      45             :     const data::variable_list& d = eqn.formal_parameters();
      46             :     const data::data_expression_list& e = x.actual_parameters();
      47             :     auto di = d.begin();
      48             :     auto ei = e.begin();
      49             :     for (; di != d.end(); ++di, ++ei)
      50             :     {
      51             :       sigma[*di] = *ei;
      52             :     }
      53             :     result = process::replace_variables_capture_avoiding(p, sigma);
      54             :   }
      55             : 
      56             :   /// \brief Converts a process instance assignment P(d = e) into p[d := e], where P(d) = p is the equation
      57             :   /// corresponding to P.
      58             :   template <class T>
      59             :   void apply(T& result, const process::process_instance_assignment& x)
      60             :   {
      61             :     const process_equation& eqn = find_equation(equations, x.identifier());
      62             :     const process_expression& p = eqn.expression();
      63             :     data::mutable_map_substitution<> sigma;
      64             :     for (const auto& a: x.assignments())
      65             :     {
      66             :       sigma[a.lhs()] = a.rhs();
      67             :     }
      68             :     result = process::replace_variables_capture_avoiding(p, sigma);
      69             :   }
      70             : };
      71             : 
      72             : } // namespace detail
      73             : 
      74             : /// \brief Replaces embedded process instances by the right hand sides of the corresponding equations
      75             : inline
      76             : process_expression expand_process_instance_assignments(const process_expression& x, const std::vector<process_equation>& equations)
      77             : {
      78             :   detail::expand_process_instance_assignments_builder f(equations);
      79             :   process_expression result;
      80             :   f.apply(result, x);
      81             :   return result;
      82             : }
      83             : 
      84             : // Converts a process_instance_assignment into a process_instance, by expanding assignments
      85             : inline
      86           0 : process_instance expand_assignments(const process::process_instance_assignment& x, const std::vector<process_equation>& equations)
      87             : {
      88           0 :   const process_equation& eqn = find_equation(equations, x.identifier());
      89           0 :   data::assignment_sequence_substitution sigma(x.assignments());
      90           0 :   std::vector<data::data_expression> e;
      91           0 :   for (const data::variable& v: eqn.formal_parameters())
      92             :   {
      93           0 :     e.push_back(sigma(v));
      94             :   }
      95           0 :   return process_instance(x.identifier(), data::data_expression_list(e.begin(), e.end()));
      96           0 : }
      97             : 
      98             : } // namespace process
      99             : 
     100             : } // namespace mcrl2
     101             : 
     102             : #endif // MCRL2_PROCESS_EXPAND_PROCESS_INSTANCE_ASSIGNMENTS_H