LCOV - code coverage report
Current view: top level - process/include/mcrl2/process/detail - alphabet_push_block.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 64 164 39.0 %
Date: 2024-03-08 02:52:28 Functions: 13 34 38.2 %
Legend: Lines: hit not hit

          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_push_block.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_BLOCK_H
      13             : #define MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_BLOCK_H
      14             : 
      15             : #include "mcrl2/process/detail/alphabet_push_allow.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace process {
      20             : 
      21             : struct push_block_cache
      22             : {
      23             :   std::map<process_instance, std::vector<std::pair<std::set<core::identifier_string>, process_instance> > > equation_cache;
      24             : 
      25             :   // Caches the alphabet of pCRL equations
      26             :   std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache;
      27             : 
      28           2 :   explicit push_block_cache(std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache_)
      29           2 :     : pcrl_equation_cache(pcrl_equation_cache_)
      30           2 :   {}
      31             : };
      32             : 
      33             : namespace block_operations {
      34             : 
      35             : template <typename Container>
      36           0 : std::set<core::identifier_string> set_union(const std::set<core::identifier_string>& S1, const Container& S2)
      37             : {
      38           0 :   std::set<core::identifier_string> result = S1;
      39           0 :   result.insert(S2.begin(), S2.end());
      40           0 :   return result;
      41           0 : }
      42             : 
      43             : template <typename Container>
      44           0 : std::set<core::identifier_string> set_difference(const std::set<core::identifier_string>& S1, const Container& S2)
      45             : {
      46           0 :   std::set<core::identifier_string> result = S1;
      47           0 :   for (typename Container::const_iterator i = S2.begin(); i != S2.end(); ++i)
      48             :   {
      49           0 :     result.erase(*i);
      50             :   }
      51           0 :   return result;
      52           0 : }
      53             : 
      54             : inline
      55           0 : std::set<core::identifier_string> rename_inverse(const rename_expression_list& R, const std::set<core::identifier_string>& B)
      56             : {
      57           0 :   alphabet_operations::rename_inverse_map Rinverse = alphabet_operations::rename_inverse(R);
      58           0 :   std::set<core::identifier_string> result;
      59           0 :   for (const core::identifier_string& i: B)
      60             :   {
      61           0 :     auto j = Rinverse.find(i);
      62           0 :     if (j != Rinverse.end())
      63             :     {
      64           0 :       std::vector<core::identifier_string> s = Rinverse[i];
      65           0 :       result.insert(s.begin(), s.end());
      66           0 :     }
      67             :     else
      68             :     {
      69           0 :       result.insert(i);
      70             :     }
      71             :   }
      72           0 :   return result;
      73           0 : }
      74             : 
      75             : } // namespace block_operations
      76             : 
      77             : namespace detail {
      78             : 
      79             : struct push_block_printer
      80             : {
      81             :   const std::set<core::identifier_string>& B;
      82             : 
      83           1 :   explicit push_block_printer(const std::set<core::identifier_string>& B_)
      84           1 :     : B(B_)
      85           1 :   {}
      86             : 
      87           1 :   std::string print(const std::set<core::identifier_string>& x) const
      88             :   {
      89           1 :     return core::detail::print_set(x);
      90             :   }
      91             : 
      92             :   template <typename T>
      93           2 :   std::string print(const T& x) const
      94             :   {
      95           2 :     return process::pp(x);
      96             :   }
      97             : 
      98           1 :   std::string print(const process::allow& x, const allow_set& A1) const
      99             :   {
     100           1 :     std::ostringstream out;
     101           1 :     out << "push_block(" << print(B) << ", " << print(x) << ") = "
     102           1 :         << "push_allow(" << A1 << ", " << print(x.operand()) << ")" << std::endl;
     103           2 :     return out.str();
     104           1 :   }
     105             : 
     106           0 :   std::string print(const process::comm& x, const process_expression& result) const
     107             :   {
     108           0 :     std::ostringstream out;
     109           0 :     out << "push_block(" << print(B) << ", " << print(x) << ") = "
     110           0 :         << print(result) << std::endl;
     111           0 :     return out.str();
     112           0 :   }
     113             : 
     114           0 :   std::string print(const process::block& x, const std::set<core::identifier_string>& B1) const
     115             :   {
     116           0 :     std::ostringstream out;
     117           0 :     out << "push_block(" << print(B) << ", " << print(x) << ") = "
     118           0 :         << "push_block(" << print(B1) << ", " << print(x.operand()) << ")" << std::endl;
     119           0 :     return out.str();
     120           0 :   }
     121             : 
     122           0 :   std::string print(const process::hide& x, const std::set<core::identifier_string>& B1) const
     123             :   {
     124           0 :     std::ostringstream out;
     125           0 :     out << "push_block(" << print(B) << ", " << print(x) << ") = "
     126           0 :         << "hide(" << print(x.hide_set()) << ", push_block(" << print(B1) << ", " << print(x.operand()) << "))" << std::endl;
     127           0 :     return out.str();
     128           0 :   }
     129             : 
     130           0 :   std::string print(const process::rename& x, const std::set<core::identifier_string>& B1) const
     131             :   {
     132           0 :     std::ostringstream out;
     133           0 :     const auto& R = x.rename_set();
     134           0 :     out << "push_block(" << print(B) << ", rename(" << print(R) << ", " << print(x.operand()) << ")) = "
     135           0 :         << "rename(" << print(R) << ", push_block(" << print(B1) << ", " << print(x.operand()) << "))" << std::endl;
     136           0 :     return out.str();
     137           0 :   }
     138             : };
     139             : 
     140             : inline
     141             : std::string print_B(const std::set<core::identifier_string>& B)
     142             : {
     143             :   std::ostringstream out;
     144             :   out << "{";
     145             :   for (auto i = B.begin(); i != B.end(); ++i)
     146             :   {
     147             :     if (i != B.begin())
     148             :     {
     149             :       out << ", ";
     150             :     }
     151             :     out << *i;
     152             :   }
     153             :   out << "}";
     154             :   return out.str();
     155             : }
     156             : 
     157             : process_expression push_block(const std::set<core::identifier_string>& B, const process_expression& x, std::vector<process_equation>& equations, push_block_cache& W, data::set_identifier_generator& id_generator);
     158             : 
     159             : template <typename Derived>
     160             : struct push_block_builder: public process_expression_builder<Derived>
     161             : {
     162             :   typedef process_expression_builder<Derived> super;
     163             :   using super::enter;
     164             :   using super::leave;
     165             :   using super::apply;
     166             :   using super::update;
     167             : 
     168             :   // used for computing the alphabet
     169             :   std::vector<process_equation>& equations;
     170             :   push_block_cache& W;
     171             : 
     172             :   // the parameter B
     173             :   const std::set<core::identifier_string>& B;
     174             : 
     175             :   // used for generating process identifiers
     176             :   data::set_identifier_generator& id_generator;
     177             : 
     178           3 :   push_block_builder(std::vector<process_equation>& equations_, push_block_cache& W_, const std::set<core::identifier_string>& B_, data::set_identifier_generator& id_generator_)
     179           3 :     : equations(equations_), W(W_), B(B_), id_generator(id_generator_)
     180           3 :   {}
     181             : 
     182           0 :   Derived& derived()
     183             :   {
     184           0 :     return static_cast<Derived&>(*this);
     185             :   }
     186             : 
     187             :   template <class T>
     188           1 :   void apply(T& result, const process::action& x)
     189             :   {
     190             :     using utilities::detail::contains;
     191           1 :     if (contains(B, x.label().name()))
     192             :     {
     193           0 :       result = delta();
     194             :     }
     195             :     else
     196             :     {
     197           1 :       result = x;
     198             :     }
     199           1 :   }
     200             : 
     201             :   template <class T>
     202           2 :   void apply(T& result, const process::process_instance& x)
     203             :   {
     204             :     // Let x = P(e)
     205             :     // The corresponding equation is P(d) = p
     206           2 :     auto i = W.equation_cache.find(x);
     207           2 :     if (i != W.equation_cache.end())
     208             :     {
     209           1 :       const std::vector<std::pair<std::set<core::identifier_string>, process_instance> >& v = i->second;
     210           1 :       for (const auto& j: v)
     211             :       {
     212           1 :         if (B == j.first)
     213             :         {
     214           1 :           result = j.second;
     215           1 :           return;
     216             :         }
     217             :       }
     218             :     }
     219             : 
     220           1 :     const process_equation& eqn = find_equation(equations, x.identifier());
     221           1 :     const data::variable_list& d = eqn.formal_parameters();
     222           1 :     core::identifier_string name = id_generator(x.identifier().name());
     223           1 :     process_identifier P1(name, x.identifier().variables());
     224           1 :     const process_expression& p = eqn.expression();
     225             : 
     226             :     // Add (P(e), B, P1(e)) to W
     227           1 :     W.equation_cache[x].push_back(std::make_pair(B, process_instance(P1, x.actual_parameters())));
     228             : 
     229           1 :     process_expression p1 = push_block(B, p, equations, W, id_generator);
     230             : 
     231             :     // create a new equation P1(d) = p1
     232           1 :     process_equation eqn1(P1, d, p1);
     233           1 :     equations.push_back(eqn1);
     234             : 
     235           1 :     result = process_instance(P1, x.actual_parameters());
     236           1 :   }
     237             : 
     238             :   template <class T>
     239           0 :   void apply(T& result, const process::process_instance_assignment& x)
     240             :   {
     241           0 :     process_instance x1 = expand_assignments(x, equations);
     242           0 :     derived().apply(result, x1);
     243           0 :   }
     244             : 
     245             :   template <class T>
     246           0 :   void apply(T& result, const process::block& x)
     247             :   {
     248           0 :     std::set<core::identifier_string> B1 = block_operations::set_union(B, x.block_set());
     249           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
     250           0 :     result = push_block(B1, x.operand(), equations, W, id_generator);
     251           0 :   }
     252             : 
     253             :   template <class T>
     254           0 :   void apply(T& result, const process::hide& x)
     255             :   {
     256           0 :     const core::identifier_string_list& I = x.hide_set();
     257           0 :     std::set<core::identifier_string> B1 = block_operations::set_difference(B, I);
     258           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
     259           0 :     make_hide(result, I, push_block(B1, x.operand(), equations, W, id_generator));
     260           0 :   }
     261             : 
     262             :   template <class T>
     263           0 :   void apply(T& result, const process::rename& x)
     264             :   {
     265           0 :     const rename_expression_list& R = x.rename_set();
     266           0 :     std::set<core::identifier_string> B1 = block_operations::rename_inverse(R, B);
     267           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
     268           0 :     process::make_rename(result, R, push_block(B1, x.operand(), equations, W, id_generator));
     269           0 :   }
     270             : 
     271           0 :   bool restrict_(const core::identifier_string& b, const std::set<core::identifier_string>& B, const communication_expression_list& C) const
     272             :   {
     273             :     using utilities::detail::contains;
     274           0 :     for (const communication_expression& i: C)
     275             :     {
     276           0 :       core::identifier_string_list gamma = i.action_name().names();
     277           0 :       const core::identifier_string& c = i.name();
     278           0 :       if (contains(gamma, b) && !contains(B, c))
     279             :       {
     280           0 :         return true;
     281             :       }
     282             :     }
     283           0 :     return false;
     284             :   }
     285             : 
     286           0 :   std::set<core::identifier_string> restrict_block(const std::set<core::identifier_string>& B, const communication_expression_list& C) const
     287             :   {
     288           0 :     std::set<core::identifier_string> result;
     289           0 :     for (auto i = B.begin(); i != B.end(); ++i)
     290             :     {
     291           0 :       if (!restrict_(*i, B, C))
     292             :       {
     293           0 :         result.insert(*i);
     294             :       }
     295             :     }
     296           0 :     return result;
     297           0 :   }
     298             : 
     299             :   template <class T>
     300           0 :   void apply(T& result, const process::comm& x)
     301             :   {
     302           0 :     std::set<core::identifier_string> B1 = restrict_block(B, x.comm_set());
     303           0 :     process_expression y = push_block(B1, x.operand(), equations, W, id_generator);
     304           0 :     result = make_block(core::identifier_string_list(B.begin(), B.end()), make_comm(x.comm_set(), y));
     305           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, result);
     306           0 :   }
     307             : 
     308             :   template <class T>
     309           1 :   void apply(T& result, const process::allow& x)
     310             :   {
     311           2 :     allow_set A(alphabet_operations::make_name_set(x.allow_set()));
     312           1 :     core::identifier_string_list B1(B.begin(), B.end());
     313           2 :     allow_set A1(alphabet_operations::block(B1, A.A));
     314           1 :     detail::push_allow_cache W_allow(id_generator, W.pcrl_equation_cache);
     315           1 :     detail::push_allow_node node = detail::push_allow(x.operand(), A1, equations, W_allow, true);
     316           1 :     mCRL2log(log::debug) << push_block_printer(B).print(x, A1);
     317           1 :     result = node.expression;
     318           1 :   }
     319             : 
     320             :   // This function is needed because the linearization algorithm does not handle the case 'delta | delta'.
     321             :   template <class T>
     322           0 :   void apply(T& result, const process::sync& x)
     323             :   {
     324           0 :     process_expression left;
     325           0 :     derived().apply(left, x.left());
     326           0 :     process_expression right;
     327           0 :     derived().apply(right, x.right());
     328           0 :     result = make_sync(left, right);
     329           0 :   }
     330             : };
     331             : 
     332             : template <template <class> class Traverser>
     333             : struct apply_push_block_builder: public Traverser<apply_push_block_builder<Traverser> >
     334             : {
     335             :   typedef Traverser<apply_push_block_builder<Traverser> > super;
     336             :   using super::enter;
     337             :   using super::leave;
     338             :   using super::apply;
     339             :   using super::update;
     340             : 
     341           3 :   apply_push_block_builder(std::vector<process_equation>& equations, push_block_cache& W, const std::set<core::identifier_string>& B, data::set_identifier_generator& id_generator)
     342           3 :     : super(equations, W, B, id_generator)
     343           3 :   {}
     344             : };
     345             : 
     346             : inline
     347           3 : process_expression push_block(const std::set<core::identifier_string>& B, const process_expression& x, std::vector<process_equation>& equations, push_block_cache& W, data::set_identifier_generator& id_generator)
     348             : {
     349           3 :   apply_push_block_builder<push_block_builder> f(equations, W, B, id_generator);
     350           3 :   process_expression result;
     351           3 :   f.apply(result, x);
     352           6 :   return result;
     353           0 : }
     354             : 
     355             : } // namespace detail
     356             : 
     357             : inline
     358           2 : process_expression push_block(const core::identifier_string_list& B,
     359             :                               const process_expression& x,
     360             :                               std::vector<process_equation>& equations,
     361             :                               data::set_identifier_generator& id_generator,
     362             :                               std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache
     363             :                              )
     364             : {
     365           2 :   std::set<core::identifier_string> B1(B.begin(), B.end());
     366           2 :   push_block_cache W(pcrl_equation_cache);
     367           4 :   return detail::push_block(B1, x, equations, W, id_generator);
     368           2 : }
     369             : 
     370             : } // namespace process
     371             : 
     372             : } // namespace mcrl2
     373             : 
     374             : #endif // MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_BLOCK_H

Generated by: LCOV version 1.14