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: 58 141 41.1 %
Date: 2020-09-22 00:46:14 Functions: 14 35 40.0 %
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           2 : 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             : }
      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             : }
      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             :     }
      67             :     else
      68             :     {
      69           0 :       result.insert(i);
      70             :     }
      71             :   }
      72           0 :   return result;
      73             : }
      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           2 :     std::ostringstream out;
     101           3 :     out << "push_block(" << print(B) << ", " << print(x) << ") = "
     102           3 :         << "push_allow(" << A1 << ", " << print(x.operand()) << ")" << std::endl;
     103           2 :     return out.str();
     104             :   }
     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             :   }
     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             :   }
     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             :   }
     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             :   }
     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           1 :   process::process_expression apply(const process::action& x)
     188             :   {
     189             :     using utilities::detail::contains;
     190           1 :     if (contains(B, x.label().name()))
     191             :     {
     192           0 :       return delta();
     193             :     }
     194             :     else
     195             :     {
     196           1 :       return x;
     197             :     }
     198             :   }
     199             : 
     200           2 :   process::process_expression apply(const process::process_instance& x)
     201             :   {
     202             :     // Let x = P(e)
     203             :     // The corresponding equation is P(d) = p
     204           2 :     auto i = W.equation_cache.find(x);
     205           2 :     if (i != W.equation_cache.end())
     206             :     {
     207           1 :       const std::vector<std::pair<std::set<core::identifier_string>, process_instance> >& v = i->second;
     208           1 :       for (const auto& j: v)
     209             :       {
     210           1 :         if (B == j.first)
     211             :         {
     212           1 :           return j.second;
     213             :         }
     214             :       }
     215             :     }
     216             : 
     217           1 :     const process_equation& eqn = find_equation(equations, x.identifier());
     218           1 :     const data::variable_list& d = eqn.formal_parameters();
     219           2 :     core::identifier_string name = id_generator(x.identifier().name());
     220           2 :     process_identifier P1(name, x.identifier().variables());
     221           1 :     const process_expression& p = eqn.expression();
     222             : 
     223             :     // Add (P(e), B, P1(e)) to W
     224           1 :     W.equation_cache[x].push_back(std::make_pair(B, process_instance(P1, x.actual_parameters())));
     225             : 
     226           2 :     process_expression p1 = push_block(B, p, equations, W, id_generator);
     227             : 
     228             :     // create a new equation P1(d) = p1
     229           2 :     process_equation eqn1(P1, d, p1);
     230           1 :     equations.push_back(eqn1);
     231             : 
     232           2 :     process_instance result(P1, x.actual_parameters());
     233           1 :     return workaround::return_std_move(result);
     234             :   }
     235             : 
     236           0 :   process::process_expression apply(const process::process_instance_assignment& x)
     237             :   {
     238           0 :     process_instance x1 = expand_assignments(x, equations);
     239           0 :     return derived().apply(x1);
     240             :   }
     241             : 
     242           0 :   process::process_expression apply(const process::block& x)
     243             :   {
     244           0 :     std::set<core::identifier_string> B1 = block_operations::set_union(B, x.block_set());
     245           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
     246           0 :     return push_block(B1, x.operand(), equations, W, id_generator);
     247             :   }
     248             : 
     249           0 :   process::process_expression apply(const process::hide& x)
     250             :   {
     251           0 :     const core::identifier_string_list& I = x.hide_set();
     252           0 :     std::set<core::identifier_string> B1 = block_operations::set_difference(B, I);
     253           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
     254           0 :     return make_hide(I, push_block(B1, x.operand(), equations, W, id_generator));
     255             :   }
     256             : 
     257           0 :   process::process_expression apply(const process::rename& x)
     258             :   {
     259           0 :     const rename_expression_list& R = x.rename_set();
     260           0 :     std::set<core::identifier_string> B1 = block_operations::rename_inverse(R, B);
     261           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
     262           0 :     return process::rename(R, push_block(B1, x.operand(), equations, W, id_generator));
     263             :   }
     264             : 
     265           0 :   bool restrict_(const core::identifier_string& b, const std::set<core::identifier_string>& B, const communication_expression_list& C) const
     266             :   {
     267             :     using utilities::detail::contains;
     268           0 :     for (const communication_expression& i: C)
     269             :     {
     270           0 :       core::identifier_string_list gamma = i.action_name().names();
     271           0 :       const core::identifier_string& c = i.name();
     272           0 :       if (contains(gamma, b) && !contains(B, c))
     273             :       {
     274           0 :         return true;
     275             :       }
     276             :     }
     277           0 :     return false;
     278             :   }
     279             : 
     280           0 :   std::set<core::identifier_string> restrict_block(const std::set<core::identifier_string>& B, const communication_expression_list& C) const
     281             :   {
     282           0 :     std::set<core::identifier_string> result;
     283           0 :     for (auto i = B.begin(); i != B.end(); ++i)
     284             :     {
     285           0 :       if (!restrict_(*i, B, C))
     286             :       {
     287           0 :         result.insert(*i);
     288             :       }
     289             :     }
     290           0 :     return result;
     291             :   }
     292             : 
     293           0 :   process::process_expression apply(const process::comm& x)
     294             :   {
     295           0 :     std::set<core::identifier_string> B1 = restrict_block(B, x.comm_set());
     296           0 :     process_expression y = push_block(B1, x.operand(), equations, W, id_generator);
     297           0 :     process_expression result = make_block(core::identifier_string_list(B.begin(), B.end()), make_comm(x.comm_set(), y));
     298           0 :     mCRL2log(log::debug) << push_block_printer(B).print(x, result);
     299           0 :     return result;
     300             :   }
     301             : 
     302           1 :   process::process_expression apply(const process::allow& x)
     303             :   {
     304           2 :     allow_set A(alphabet_operations::make_name_set(x.allow_set()));
     305           2 :     core::identifier_string_list B1(B.begin(), B.end());
     306           2 :     allow_set A1(alphabet_operations::block(B1, A.A));
     307           2 :     detail::push_allow_cache W_allow(id_generator, W.pcrl_equation_cache);
     308           2 :     detail::push_allow_node node = detail::push_allow(x.operand(), A1, equations, W_allow, true);
     309           1 :     mCRL2log(log::debug) << push_block_printer(B).print(x, A1);
     310           2 :     return node.expression;
     311             :   }
     312             : 
     313             :   // This function is needed because the linearization algorithm does not handle the case 'delta | delta'.
     314           0 :   process::process_expression apply(const process::sync& x)
     315             :   {
     316           0 :     process_expression left = derived().apply(x.left());
     317           0 :     process_expression right = derived().apply(x.right());
     318           0 :     return make_sync(left, right);
     319             :   }
     320             : };
     321             : 
     322             : template <template <class> class Traverser>
     323             : struct apply_push_block_builder: public Traverser<apply_push_block_builder<Traverser> >
     324             : {
     325             :   typedef Traverser<apply_push_block_builder<Traverser> > super;
     326             :   using super::enter;
     327             :   using super::leave;
     328             :   using super::apply;
     329             :   using super::update;
     330             : 
     331           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)
     332           3 :     : super(equations, W, B, id_generator)
     333           3 :   {}
     334             : };
     335             : 
     336             : inline
     337           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)
     338             : {
     339           3 :   apply_push_block_builder<push_block_builder> f(equations, W, B, id_generator);
     340           3 :   return f.apply(x);
     341             : }
     342             : 
     343             : } // namespace detail
     344             : 
     345             : inline
     346           2 : process_expression push_block(const core::identifier_string_list& B,
     347             :                               const process_expression& x,
     348             :                               std::vector<process_equation>& equations,
     349             :                               data::set_identifier_generator& id_generator,
     350             :                               std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache
     351             :                              )
     352             : {
     353           4 :   std::set<core::identifier_string> B1(B.begin(), B.end());
     354           4 :   push_block_cache W(pcrl_equation_cache);
     355           4 :   return detail::push_block(B1, x, equations, W, id_generator);
     356             : }
     357             : 
     358             : } // namespace process
     359             : 
     360             : } // namespace mcrl2
     361             : 
     362             : #endif // MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_BLOCK_H

Generated by: LCOV version 1.13