LCOV - code coverage report
Current view: top level - process/include/mcrl2/process/detail - alphabet_push_allow.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 120 339 35.4 %
Date: 2020-09-22 00:46:14 Functions: 30 70 42.9 %
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_allow.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_ALLOW_H
      13             : #define MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_ALLOW_H
      14             : 
      15             : #include "mcrl2/process/allow_set.h"
      16             : #include "mcrl2/process/alphabet_pcrl.h"
      17             : #include "mcrl2/process/expand_process_instance_assignments.h"
      18             : #include "mcrl2/process/is_multi_action.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace process {
      23             : 
      24             : namespace detail {
      25             : 
      26             : // Returns allow(alphabet, x)
      27             : inline
      28           2 : process_expression construct_allow(const multi_action_name_set& A, const process_expression& x, bool allow_required)
      29             : {
      30             :   // convert alphabet to an action_name_multiset_list v
      31           4 :   std::vector<action_name_multiset> v;
      32           4 :   for (const multi_action_name& alpha: A)
      33             :   {
      34           2 :     if (!alpha.empty()) // exclude tau
      35             :     {
      36           2 :       v.emplace_back(core::identifier_string_list(alpha.begin(), alpha.end()));
      37             :     }
      38             :   }
      39           4 :   action_name_multiset_list B(v.begin(), v.end());
      40           2 :   if (allow_required || !B.empty())
      41             :   {
      42           2 :     return allow(B, x);
      43             :   }
      44           0 :   return x;
      45             : }
      46             : 
      47          20 : struct push_allow_node: public alphabet_node
      48             : {
      49             :   process_expression expression;
      50             : 
      51           0 :   push_allow_node() = default;
      52             : 
      53           4 :   explicit push_allow_node(const multi_action_name_set& alphabet, const process_expression& expression_ = process_expression())
      54           4 :     : alphabet_node(alphabet), expression(expression_)
      55           4 :   {}
      56             : 
      57           2 :   void apply_allow(const allow_set& A, bool allow_required = false)
      58             :   {
      59           4 :     multi_action_name_set restricted_alphabet = A.intersect(alphabet);
      60           2 :     bool needs_allow = allow_required || alphabet.size() != restricted_alphabet.size();
      61           2 :     expression = construct_allow(restricted_alphabet, expression, needs_allow);
      62           2 :   }
      63             : };
      64             : 
      65           2 : struct push_allow_cache
      66             : {
      67             :   // This attribute denotes the status of the alphabet computation.
      68             :   // - unknown: the alphabet computation has not started yet
      69             :   // - busy: the alphabet computation is busy
      70             :   // - finished: the alphabet computation is finished
      71             :   enum alphabet_status { unknown, busy, finished };
      72             : 
      73           6 :   struct alphabet_key
      74             :   {
      75             :     allow_set A;
      76             :     process_identifier P;
      77             : 
      78             :     bool operator==(const alphabet_key& other) const
      79             :     {
      80             :       return P == other.P && A == other.A;
      81             :     }
      82             : 
      83           0 :     bool operator<(const alphabet_key& other) const
      84             :     {
      85           0 :       if (P != other.P)
      86             :       {
      87           0 :         return P < other.P;
      88             :       }
      89           0 :       return A < other.A;
      90             :     }
      91             : 
      92           2 :     alphabet_key(const allow_set& A_, const process_identifier& P_)
      93           2 :      : A(A_), P(P_)
      94           2 :     {}
      95             :   };
      96             : 
      97             :   // Records the alphabet corresponding to an allow set A and a process instance Q.
      98             :   // Each alphabet value has a corresponding equation P = push_allow(A, q), where
      99             :   // q is the right hand side of the equation corresponding to Q.
     100           5 :   struct alphabet_value
     101             :   {
     102             :     multi_action_name_set alphabet;
     103             :     alphabet_status status;
     104             :     process_identifier P;
     105             : 
     106             :     alphabet_value() = default;
     107             : 
     108           1 :     alphabet_value(const multi_action_name_set& alphabet_, alphabet_status status_, const process_identifier& P_)
     109           1 :      : alphabet(alphabet_), status(status_), P(P_)
     110           1 :     {}
     111             :   };
     112             : 
     113           0 :   struct unfinished_value
     114             :   {
     115             :     allow_set A;
     116             :     process_instance P;
     117             : 
     118           0 :     bool operator<(const unfinished_value& other) const
     119             :     {
     120           0 :       if (P != other.P)
     121             :       {
     122           0 :         return P < other.P;
     123             :       }
     124           0 :       return A < other.A;
     125             :     }
     126             : 
     127           0 :     unfinished_value(const allow_set& A_, const process_instance& P_)
     128           0 :      : A(A_), P(P_)
     129           0 :     {}
     130             :   };
     131             : 
     132             :   // An identifier generator that is used for generating new equations
     133             :   data::set_identifier_generator& id_generator;
     134             : 
     135             :   // The cache of alphabet values
     136             :   std::map<alphabet_key, alphabet_value> alphabet_map;
     137             : 
     138             :   // The pairs (A, P(e)) for which an equation needs to be generated
     139             :   std::set<unfinished_value> unfinished;
     140             : 
     141             :   // The push_allow algorithm maintains a set of dependent nodes. It is used
     142             :   // to invalidate alphabet values in the cache.
     143             :   std::set<alphabet_key> dependent_nodes;
     144             : 
     145             :   // Caches the alphabet of pCRL equations
     146             :   std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache;
     147             : 
     148           2 :   push_allow_cache(data::set_identifier_generator& id_generator_, std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache_)
     149           2 :     : id_generator(id_generator_), pcrl_equation_cache(pcrl_equation_cache_)
     150           2 :   {}
     151             : 
     152             :   std::string print_status(alphabet_status status) const
     153             :   {
     154             :     switch(status)
     155             :     {
     156             :       case unknown: return "unknown";
     157             :       case busy: return "busy";
     158             :       case finished: return "finished";
     159             :     }
     160             :     throw mcrl2::runtime_error("unknown status!");
     161             :   }
     162             : 
     163             :   // Returns a reference to the alphabet value corresponding to (A, P).
     164             :   // If such value does is not yet present in the map, it is inserted.
     165           1 :   alphabet_value& alphabet(const allow_set& A, const process_identifier& P)
     166             :   {
     167           2 :     alphabet_key key(A, P);
     168           1 :     auto i = alphabet_map.find(key);
     169           1 :     if (i == alphabet_map.end())
     170             :     {
     171           2 :       core::identifier_string name = id_generator(P.name());
     172           2 :       process_identifier P1(name, P.variables());
     173           2 :       multi_action_name_set empty_set;
     174           2 :       alphabet_value value(empty_set, unknown, P1);
     175           1 :       auto p = alphabet_map.insert(std::make_pair(key, value));
     176           1 :       return p.first->second;
     177             :     }
     178           0 :     return i->second;
     179             :   }
     180             : 
     181             :   // Add (A, x) to the set of unfinished nodes
     182           0 :   void set_unfinished(const allow_set& A, const process_instance& x)
     183             :   {
     184           0 :     unfinished.insert(unfinished_value(A, x));
     185           0 :   }
     186             : 
     187             : /*
     188             :   // For each entry (A, P) -> (alpha, finished, P1) it is checked if
     189             :   // intersection(alphabet(P), A) == alpha.
     190             :   void check_equations(const std::vector<process_equation>& equations) const
     191             :   {
     192             :     for (auto i = alphabet_map.begin(); i != alphabet_map.end(); ++i)
     193             :     {
     194             :       multi_action_name_set alphabet_P = process::alphabet(i->first.P, equations);
     195             :       multi_action_name_set a = i->first.A.intersect(alphabet_P);
     196             :       std::cout << "check (" << i->first.A << ", " << i->first.P << ")";
     197             :       if (a != i->second.alphabet)
     198             :       {
     199             :         std::cout << "Error: left = " << process::pp(a) << " right = " << process::pp(i->second.alphabet);
     200             :       }
     201             :       std::cout << std::endl;
     202             :     }
     203             :   }
     204             : */
     205             : };
     206             : 
     207             : inline
     208           0 : std::ostream& operator<<(std::ostream& out, const push_allow_cache::alphabet_key& x)
     209             : {
     210           0 :   return out << "(" << x.A << ", " << x.P << ")";
     211             : }
     212             : 
     213             : inline
     214           0 : char print_alphabet_status(push_allow_cache::alphabet_status status)
     215             : {
     216           0 :   switch (status)
     217             :   {
     218           0 :     case push_allow_cache::unknown:  { return 'u'; }
     219           0 :     case push_allow_cache::busy:     { return 'b'; }
     220           0 :     case push_allow_cache::finished: { return 'f'; }
     221             :   }
     222           0 :   return '?';
     223             : }
     224             : 
     225             : inline
     226           0 : std::ostream& operator<<(std::ostream& out, const push_allow_cache::alphabet_value& x)
     227             : {
     228           0 :   return out << "(" << process::pp(x.alphabet) << ", " << print_alphabet_status(x.status) << ", " << x.P << ")";
     229             : }
     230             : 
     231             : inline
     232           0 : std::ostream& operator<<(std::ostream& out, const push_allow_cache::unfinished_value& x)
     233             : {
     234           0 :   return out << "(" << x.A << ", " << x.P << ")";
     235             : }
     236             : 
     237             : inline
     238           3 : std::ostream& operator<<(std::ostream& out, const push_allow_cache& W)
     239             : {
     240           3 :   out << "map: {";
     241           3 :   for (auto i = W.alphabet_map.begin(); i != W.alphabet_map.end(); ++i)
     242             :   {
     243           0 :     if (i != W.alphabet_map.begin())
     244             :     {
     245           0 :       out << ", ";
     246             :     }
     247           0 :     out << i->first << " -> " << i->second;
     248             :   }
     249           3 :   out << "}";
     250           3 :   out << " dependent: {";
     251           3 :   for (auto i = W.dependent_nodes.begin(); i != W.dependent_nodes.end(); ++i)
     252             :   {
     253           0 :     if (i != W.dependent_nodes.begin())
     254             :     {
     255           0 :       out << ", ";
     256             :     }
     257           0 :     out << *i;
     258             :   }
     259           3 :   out << "}";
     260           3 :   out << " unfinished: [";
     261           3 :   for (auto i = W.unfinished.begin(); i != W.unfinished.end(); ++i)
     262             :   {
     263           0 :     if (i != W.unfinished.begin())
     264             :     {
     265           0 :       out << ", ";
     266             :     }
     267           0 :     out << *i;
     268             :   }
     269           3 :   out << "]";
     270           3 :   return out;
     271             : }
     272             : 
     273             : inline
     274             : std::ostream& operator<<(std::ostream& out, const push_allow_node& x)
     275             : {
     276             :   return out << "Node(" << pp(x.alphabet) << ", " << process::pp(x.expression) << ")";
     277             : }
     278             : 
     279             : push_allow_node push_allow(const process_expression& x, const allow_set& A, std::vector<process_equation>& equations, push_allow_cache& W, bool generate_missing_equations = false);
     280             : 
     281             : template <typename Derived, typename Node = push_allow_node>
     282           4 : struct push_allow_traverser: public process_expression_traverser<Derived>
     283             : {
     284             :   typedef process_expression_traverser<Derived> super;
     285             :   using super::enter;
     286             :   using super::leave;
     287             :   using super::apply;
     288             : 
     289             :   // used for computing the alphabet
     290             :   std::vector<process_equation>& equations;
     291             :   push_allow_cache& W;
     292             : 
     293             :   // the parameter A
     294             :   const allow_set& A;
     295             : 
     296             :   std::vector<Node> node_stack;
     297             : 
     298           4 :   push_allow_traverser(std::vector<process_equation>& equations_, push_allow_cache& W_, const allow_set& A_)
     299           4 :     : equations(equations_), W(W_), A(A_)
     300           4 :   {}
     301             : 
     302           0 :   Derived& derived()
     303             :   {
     304           0 :     return static_cast<Derived&>(*this);
     305             :   }
     306             : 
     307             :   // Push a node to node_stack
     308           4 :   void push(const Node& node)
     309             :   {
     310           4 :     node_stack.push_back(node);
     311           4 :   }
     312             : 
     313             :   // Pop the top element of node_stack and return it
     314             :   Node pop()
     315             :   {
     316             :     Node result = node_stack.back();
     317             :     node_stack.pop_back();
     318             :     return result;
     319             :   }
     320             : 
     321             :   // Return the top element of node_stack
     322           4 :   Node& top()
     323             :   {
     324           4 :     return node_stack.back();
     325             :   }
     326             : 
     327             :   // Return the top element of node_stack
     328             :   const Node& top() const
     329             :   {
     330             :     return node_stack.back();
     331             :   }
     332             : 
     333           3 :   std::string log_push_result(const process_expression& x, const allow_set& A, const push_allow_cache& W, const push_allow_node& result, const std::string& msg = "", const std::string& text = "")
     334             :   {
     335           6 :     std::ostringstream out;
     336           6 :     std::string text1 = text;
     337           3 :     if (!text1.empty())
     338             :     {
     339           1 :       text1 = text1 + " = ";
     340             :     }
     341           6 :     out << msg << "push_allow(" << A << ", " << process::pp(x) << ") = "
     342             :       << text1
     343           6 :       << process::pp(result.expression) << " with alphabet(" << process::pp(result.expression) << ") = " << pp(result.alphabet) << std::endl
     344           3 :       << " W = " << W << std::endl;
     345           6 :     return out.str();
     346             :   }
     347             : 
     348           3 :   std::string log(const process_expression& x, const std::string& text = "")
     349             :   {
     350           3 :     return log_push_result(x, A, W, top(), "", text);
     351             :   }
     352             : 
     353           2 :   void leave(const process::action& x)
     354             :   {
     355           4 :     multi_action_name alpha;
     356           2 :     alpha.insert(x.label().name());
     357           2 :     if (A.contains(alpha))
     358             :     {
     359           4 :       multi_action_name_set A1;
     360           2 :       A1.insert(alpha);
     361           2 :       push(push_allow_node(A1, x));
     362             :     }
     363             :     else
     364             :     {
     365           0 :       multi_action_name_set A1;
     366           0 :       push(push_allow_node(A1, process::delta()));
     367             :     }
     368           2 :     mCRL2log(log::debug) << log(x);
     369           2 :   }
     370             : 
     371           1 :   void leave(const process::process_instance& x)
     372             :   {
     373           1 :     const process_identifier& P = x.identifier();
     374             : 
     375           1 :     push_allow_cache::alphabet_key key(A, P);
     376           1 :     push_allow_cache::alphabet_value& alpha = W.alphabet(A, P);
     377           1 :     const multi_action_name_set& alphabet = alpha.alphabet;
     378           1 :     push_allow_cache::alphabet_status status = alpha.status;
     379           1 :     const process_identifier& P1 = alpha.P;
     380           1 :     process_instance P1e(P1, x.actual_parameters());
     381             : 
     382             :     // if the node is in the pCRL equation cache, do not go into the recursion
     383           1 :     auto i = W.pcrl_equation_cache.find(P);
     384           1 :     if (i != W.pcrl_equation_cache.end())
     385             :     {
     386           2 :       push_allow_node node(i->second, x);
     387           1 :       node.apply_allow(A);
     388           1 :       push(node);
     389           1 :       alpha.alphabet = node.alphabet;
     390           1 :       alpha.status = push_allow_cache::finished;
     391           1 :       return;
     392             :     }
     393             : 
     394           0 :     if (status == push_allow_cache::finished)
     395             :     {
     396             :       // we already know the result for (A, P)
     397           0 :       push_allow_node node(alphabet, P1e);
     398           0 :       push(node);
     399           0 :       mCRL2log(log::debug) << log(x);
     400           0 :       return;
     401             :     }
     402           0 :     else if (status == push_allow_cache::busy)
     403             :     {
     404             :       // the alphabet of (A, x) is currently being computed; it suffices to return (emptyset, P1e)
     405           0 :       W.dependent_nodes.insert(key);
     406           0 :       multi_action_name_set empty_set;
     407           0 :       push_allow_node node(empty_set, P1e);
     408           0 :       push(node);
     409           0 :       mCRL2log(log::debug) << log(x);
     410           0 :       return;
     411             :     }
     412             : 
     413           0 :     if (status == push_allow_cache::unknown)
     414             :     {
     415           0 :       alpha.status = push_allow_cache::busy;
     416             : 
     417             :       // N.B. A copy is made, because a call to push_allow may invalidate a reference.
     418           0 :       const process_equation& eqn = find_equation(equations, x.identifier());
     419           0 :       const data::variable_list& d = eqn.formal_parameters();
     420           0 :       const process_expression& p = eqn.expression();
     421             : 
     422           0 :       push_allow_node node;
     423             : 
     424             :       // compute the alphabet for (A, P)
     425           0 :       node = push_allow(p, A, equations, W);
     426             : 
     427           0 :       W.dependent_nodes.erase(key);
     428           0 :       if (W.dependent_nodes.empty())
     429             :       {
     430             :         // create a new equation P(d) = p1
     431           0 :         const process_expression& p1 = node.expression;
     432           0 :         process_equation eqn1(P1, d, p1);
     433           0 :         equations.push_back(eqn1);
     434             : 
     435           0 :         alpha.alphabet = node.alphabet;
     436           0 :         alpha.status = push_allow_cache::finished;
     437           0 :         node.apply_allow(A);
     438             :       }
     439             :       else
     440             :       {
     441           0 :         alpha.status = push_allow_cache::unknown;
     442           0 :         W.set_unfinished(A, x);
     443             :       }
     444             : 
     445           0 :       node.expression = P1e;
     446           0 :       push(node);
     447           0 :       mCRL2log(log::debug) << log(x);
     448             :     }
     449             :   }
     450             : 
     451           0 :   void leave(const process::process_instance_assignment& x)
     452             :   {
     453           0 :     process_instance x1 = expand_assignments(x, equations);
     454           0 :     derived().apply(x1);
     455           0 :   }
     456             : 
     457           0 :   void apply_pcrl_node(const process_expression& x)
     458             :   {
     459           0 :     push_allow_node node(process::alphabet_pcrl(x, W.pcrl_equation_cache), x);
     460           0 :     node.apply_allow(A);
     461           0 :     push(node);
     462           0 :   }
     463             : 
     464           0 :   void leave(const process::delta& x)
     465             :   {
     466           0 :     apply_pcrl_node(x);
     467             :     // push(push_allow_node(process::alphabet(x, equations), x));
     468           0 :     mCRL2log(log::debug) << log(x);
     469           0 :   }
     470             : 
     471           0 :   void leave(const process::tau& x)
     472             :   {
     473           0 :     apply_pcrl_node(x);
     474             :     // push(push_allow_node(process::alphabet(x, equations), x));
     475           0 :     mCRL2log(log::debug) << log(x);
     476           0 :   }
     477             : 
     478           0 :   void leave(const process::sum& x)
     479             :   {
     480           0 :     apply_pcrl_node(x);
     481             :     // top().expression = process::sum(x.variables(), top().expression);
     482           0 :     mCRL2log(log::debug) << log(x);
     483           0 :   }
     484             : 
     485           0 :   void leave(const process::at& x)
     486             :   {
     487           0 :     apply_pcrl_node(x);
     488             :     // top().expression = process::at(top().expression, x.time_stamp());
     489           0 :     mCRL2log(log::debug) << log(x);
     490           0 :   }
     491             : 
     492           0 :   void leave(const process::seq& x)
     493             :   {
     494           0 :     apply_pcrl_node(x);
     495             :     // Node right = pop();
     496             :     // Node left = pop();
     497             :     // push(push_allow_node(alphabet_operations::set_union(left.alphabet, right.alphabet), process::seq(left.expression, right.expression)));
     498           0 :     mCRL2log(log::debug) << log(x);
     499           0 :   }
     500             : 
     501           0 :   void leave(const process::if_then& x)
     502             :   {
     503           0 :     apply_pcrl_node(x);
     504             :     // top().expression = process::if_then(x.condition(), top().expression);
     505           0 :     mCRL2log(log::debug) << log(x);
     506           0 :   }
     507             : 
     508           0 :   void leave(const process::if_then_else& x)
     509             :   {
     510           0 :     apply_pcrl_node(x);
     511             :     // Node right = pop();
     512             :     // Node left = pop();
     513             :     // push(push_allow_node(alphabet_operations::set_union(left.alphabet, right.alphabet), process::if_then_else(x.condition(), left.expression, right.expression)));
     514           0 :     mCRL2log(log::debug) << log(x);
     515           0 :   }
     516             : 
     517           0 :   void leave(const process::bounded_init& x)
     518             :   {
     519           0 :     apply_pcrl_node(x);
     520             :     // Node right = pop();
     521             :     // Node left = pop();
     522             :     // push(push_allow_node(alphabet_operations::set_union(left.alphabet, right.alphabet), process::bounded_init(left.expression, right.expression)));
     523           0 :     mCRL2log(log::debug) << log(x);
     524           0 :   }
     525             : 
     526           0 :   void leave(const process::choice& x)
     527             :   {
     528           0 :     apply_pcrl_node(x);
     529             :     // Node right = pop();
     530             :     // Node left = pop();
     531             :     // push(push_allow_node(alphabet_operations::set_union(left.alphabet, right.alphabet), process::choice(left.expression, right.expression)));
     532           0 :     mCRL2log(log::debug) << log(x);
     533           0 :   }
     534             : 
     535           0 :   std::string log_hide(const process::hide& x, const allow_set& A1)
     536             :   {
     537           0 :     std::ostringstream out;
     538           0 :     out << "hide({" << core::pp(x.hide_set()) << "}, push(" << A1 << ", " << process::pp(x.operand()) << "))";
     539           0 :     return out.str();
     540             :   }
     541             : 
     542           0 :   void apply(const process::hide& x)
     543             :   {
     544           0 :     const core::identifier_string_list& I = x.hide_set();
     545           0 :     allow_set A1 = alphabet_operations::hide_inverse(I, A);
     546           0 :     push_allow_node node = push_allow(x.operand(), A1, equations, W);
     547           0 :     push(push_allow_node(alphabet_operations::hide(I, node.alphabet), process::hide(I, node.expression)));
     548           0 :     mCRL2log(log::debug) << log(x, log_hide(x, A1));
     549           0 :   }
     550             : 
     551           0 :   std::string log_block(const process::block& x, const allow_set& A1)
     552             :   {
     553           0 :     std::ostringstream out;
     554           0 :     out << "block({" << core::pp(x.block_set()) << "}, push(" << A1 << ", " << process::pp(x.operand()) << "))";
     555           0 :     return out.str();
     556             :   }
     557             : 
     558           0 :   void apply(const process::block& x)
     559             :   {
     560           0 :     const core::identifier_string_list& B = x.block_set();
     561           0 :     allow_set A1 = alphabet_operations::block(B, A);
     562           0 :     push_allow_node node = push_allow(x.operand(), A1, equations, W);
     563           0 :     push(node);
     564           0 :     mCRL2log(log::debug) << log(x, log_block(x, A1));
     565           0 :   }
     566             : 
     567           0 :   std::string log_rename(const process::rename& x, const allow_set& A1)
     568             :   {
     569           0 :     std::ostringstream out;
     570           0 :     out << "rename({" << process::pp(x.rename_set()) << "}, push(" << A1 << ", " << process::pp(x.operand()) << "))";
     571           0 :     return out.str();
     572             :   }
     573             : 
     574           0 :   void apply(const process::rename& x)
     575             :   {
     576           0 :     const rename_expression_list& R = x.rename_set();
     577           0 :     allow_set A1 = alphabet_operations::rename_inverse(R, A);
     578           0 :     push_allow_node node = push_allow(x.operand(), A1, equations, W);
     579           0 :     push(push_allow_node(alphabet_operations::rename(R, node.alphabet), process::rename(R, node.expression)));
     580           0 :     mCRL2log(log::debug) << log(x, log_rename(x, A1));
     581           0 :   }
     582             : 
     583           0 :   std::string log_comm(const process::comm& x, const allow_set& A, const allow_set& A1)
     584             :   {
     585           0 :     std::ostringstream out;
     586           0 :     out << "allow(" << A << ", comm({" << process::pp(x.comm_set()) << "}, push(" << A1 << ", " << process::pp(x.operand()) << ")))";
     587           0 :     return out.str();
     588             :   }
     589             : 
     590           0 :   void apply(const process::comm& x)
     591             :   {
     592           0 :     const communication_expression_list& C = x.comm_set();
     593           0 :     allow_set A1 = alphabet_operations::comm_inverse(C, A);
     594           0 :     push_allow_node node = push_allow(x.operand(), A1, equations, W);
     595           0 :     communication_expression_list C1 = alphabet_operations::filter_comm_set(C, node.alphabet);
     596           0 :     push(push_allow_node(alphabet_operations::comm(C1, node.alphabet), make_comm(C1, node.expression)));
     597           0 :     top().apply_allow(A);
     598           0 :     mCRL2log(log::debug) << log(x, log_comm(x, A, A1));
     599           0 :   }
     600             : 
     601           0 :   std::string log_allow(const process::allow& x, const allow_set& A1)
     602             :   {
     603           0 :     std::ostringstream out;
     604           0 :     out << "allow({" << process::pp(x.allow_set()) << "}, push(" << A1 << ", " << process::pp(x.operand()) << "))";
     605           0 :     return out.str();
     606             :   }
     607             : 
     608           0 :   void apply(const process::allow& x)
     609             :   {
     610           0 :     const action_name_multiset_list& V = x.allow_set();
     611           0 :     allow_set A1 = alphabet_operations::allow(V, A);
     612           0 :     push_allow_node node = push_allow(x.operand(), A1, equations, W);
     613           0 :     push(node);
     614           0 :     mCRL2log(log::debug) << log(x, log_allow(x, A1));
     615           0 :   }
     616             : 
     617           1 :   std::string log_merge(const process::merge& x, const allow_set& A, const allow_set& A_sub, const allow_set& A_arrow)
     618             :   {
     619           2 :     std::ostringstream out;
     620           1 :     out << "allow(" << A << ", merge(push(" << A_sub << ", " << process::pp(x.left()) << "), push(" << A_arrow << ", " << process::pp(x.right()) << ")))";
     621           2 :     return out.str();
     622             :   }
     623             : 
     624           1 :   void apply(const process::merge& x)
     625             :   {
     626           2 :     allow_set A_sub = alphabet_operations::subsets(A);
     627           2 :     push_allow_node p1 = push_allow(x.left(), A_sub, equations, W);
     628           2 :     allow_set A_arrow = alphabet_operations::left_arrow(A, p1.alphabet);
     629           2 :     push_allow_node q1 = push_allow(x.right(), A_arrow, equations, W);
     630           2 :     auto [Apq, allow_required] = alphabet_operations::bounded_merge(p1.alphabet, q1.alphabet, A);
     631           1 :     push(push_allow_node(Apq, make_merge(p1.expression, q1.expression)));
     632           1 :     top().apply_allow(A, allow_required);
     633           1 :     mCRL2log(log::debug) << log(x, log_merge(x, A, A_sub, A_arrow));
     634           1 :   }
     635             : 
     636           0 :   std::string log_left_merge(const process::left_merge& x, const allow_set& A, const allow_set& A_sub, const allow_set& A_arrow)
     637             :   {
     638           0 :     std::ostringstream out;
     639           0 :     out << "allow(" << A << ", left_merge(push(" << A_sub << ", " << process::pp(x.left()) << "), push(" << A_arrow << ", " << process::pp(x.right()) << ")))";
     640           0 :     return out.str();
     641             :   }
     642             : 
     643           0 :   void apply(const process::left_merge& x)
     644             :   {
     645           0 :     allow_set A_sub = alphabet_operations::subsets(A);
     646           0 :     push_allow_node p1 = push_allow(x.left(), A_sub, equations, W);
     647           0 :     allow_set A_arrow = alphabet_operations::left_arrow(A, p1.alphabet);
     648           0 :     push_allow_node q1 = push_allow(x.right(), A_arrow, equations, W);
     649           0 :     auto [Apq, allow_required] = alphabet_operations::bounded_left_merge(p1.alphabet, q1.alphabet, A);
     650           0 :     push(push_allow_node(Apq, make_left_merge(p1.expression, q1.expression)));
     651           0 :     top().apply_allow(A, allow_required);
     652           0 :     mCRL2log(log::debug) << log(x, log_left_merge(x, A, A_sub, A_arrow));
     653           0 :   }
     654             : 
     655           0 :   std::string log_sync(const process::sync& x, const allow_set& A, const allow_set& A_sub, const allow_set& A_arrow)
     656             :   {
     657           0 :     std::ostringstream out;
     658           0 :     out << "allow(" << A << ", sync(push(" << A_sub << ", " << process::pp(x.left()) << "), push(" << A_arrow << ", " << process::pp(x.right()) << ")))";
     659           0 :     return out.str();
     660             :   }
     661             : 
     662           0 :   void apply(const process::sync& x)
     663             :   {
     664           0 :     if (is_multi_action(x))
     665             :     {
     666             :       // Do not go into the recursion if x is a multi action
     667           0 :       multi_action_name alpha = sync_multi_action_name(x);
     668           0 :       if (A.contains(alpha))
     669             :       {
     670           0 :         push_allow_node node({ alpha }, x);
     671           0 :         push(node);
     672             :       }
     673             :       else
     674             :       {
     675           0 :         push_allow_node node(multi_action_name_set{}, delta());
     676           0 :         push(node);
     677             :       }
     678           0 :       return;
     679             :     }
     680             : 
     681           0 :     allow_set A_sub = alphabet_operations::subsets(A);
     682           0 :     push_allow_node p1 = push_allow(x.left(), A_sub, equations, W);
     683           0 :     allow_set A_arrow = alphabet_operations::left_arrow(A, p1.alphabet);
     684           0 :     push_allow_node q1 = push_allow(x.right(), A_arrow, equations, W);
     685           0 :     auto [Apq, allow_required] = alphabet_operations::bounded_merge(p1.alphabet, q1.alphabet, A);
     686           0 :     push(push_allow_node(Apq, make_sync(p1.expression, q1.expression)));
     687           0 :     top().apply_allow(A, allow_required);
     688           0 :     mCRL2log(log::debug) << log(x, log_sync(x, A, A_sub, A_arrow));
     689             :   }
     690             : };
     691             : 
     692             : template <template <class, class> class Traverser, typename Node = push_allow_node>
     693           4 : struct apply_push_allow_traverser: public Traverser<apply_push_allow_traverser<Traverser, Node>, Node>
     694             : {
     695             :   typedef Traverser<apply_push_allow_traverser<Traverser, Node>, Node> super;
     696             :   using super::enter;
     697             :   using super::leave;
     698             :   using super::apply;
     699             : 
     700           4 :   apply_push_allow_traverser(std::vector<process_equation>& equations, push_allow_cache& W, const allow_set& A)
     701           4 :     : super(equations, W, A)
     702           4 :   {}
     703             : };
     704             : 
     705             : inline
     706           4 : push_allow_node push_allow(const process_expression& x, const allow_set& A, std::vector<process_equation>& equations, push_allow_cache& W, bool generate_missing_equations)
     707             : {
     708           8 :   apply_push_allow_traverser<push_allow_traverser> f(equations, W, A);
     709           4 :   f.apply(x);
     710           4 :   push_allow_node result = f.node_stack.back();
     711             : 
     712           4 :   if (generate_missing_equations)
     713             :   {
     714           1 :     while (!W.unfinished.empty())
     715             :     {
     716           0 :       detail::push_allow_cache::unfinished_value v = *W.unfinished.begin();
     717           0 :       detail::push_allow_cache::alphabet_key key(v.A, v.P.identifier());
     718           0 :       W.unfinished.erase(W.unfinished.begin());
     719           0 :       detail::push_allow_cache::alphabet_value& value = W.alphabet(key.A, key.P);
     720           0 :       if (value.status != detail::push_allow_cache::finished)
     721             :       {
     722           0 :         mCRL2log(log::debug) << "generating unfinished equation for " << key << " -> " << value << std::endl;
     723           0 :         push_allow(v.P, v.A, equations, W);
     724             :       }
     725             :     }
     726             :   }
     727             :   // W.check_equations(equations);
     728             : 
     729           8 :   return result;
     730             : }
     731             : 
     732             : } // namespace detail
     733             : 
     734             : inline
     735             : process_expression push_allow(const process_expression& x,
     736             :                               const action_name_multiset_list& V,
     737             :                               std::vector<process_equation>& equations,
     738             :                               data::set_identifier_generator& id_generator,
     739             :                               std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache
     740             :                             )
     741             : {
     742             :   allow_set A(alphabet_operations::make_name_set(V));
     743             :   detail::push_allow_cache W(id_generator, pcrl_equation_cache);
     744             :   detail::push_allow_node node = detail::push_allow(x, A, equations, W, true);
     745             :   return node.expression;
     746             : }
     747             : 
     748             : } // namespace process
     749             : 
     750             : } // namespace mcrl2
     751             : 
     752             : #endif // MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_ALLOW_H

Generated by: LCOV version 1.13