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 2 : 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 2 : 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 2 : }
46 :
47 : 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 2 : 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 : 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 : 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 : 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 : 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 1 : alphabet_key key(A, P);
168 1 : auto i = alphabet_map.find(key);
169 1 : if (i == alphabet_map.end())
170 : {
171 1 : core::identifier_string name = id_generator(P.name());
172 1 : process_identifier P1(name, P.variables());
173 1 : multi_action_name_set empty_set;
174 1 : 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 1 : }
178 0 : return i->second;
179 1 : }
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 : 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 3 : std::ostringstream out;
336 3 : std::string text1 = text;
337 3 : if (!text1.empty())
338 : {
339 1 : text1 = text1 + " = ";
340 : }
341 3 : 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 3 : }
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 2 : multi_action_name alpha;
356 2 : alpha.insert(x.label().name());
357 2 : if (A.contains(alpha))
358 : {
359 2 : multi_action_name_set A1;
360 2 : A1.insert(alpha);
361 2 : push(push_allow_node(A1, x));
362 2 : }
363 : else
364 : {
365 0 : multi_action_name_set A1;
366 0 : push(push_allow_node(A1, process::delta()));
367 0 : }
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 1 : 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 1 : }
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 0 : }
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 0 : }
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 0 : }
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 0 : }
449 2 : }
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 0 : }
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 0 : }
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 0 : }
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 0 : }
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 0 : }
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 1 : 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 1 : }
623 :
624 1 : void apply(const process::merge& x)
625 : {
626 1 : allow_set A_sub = alphabet_operations::subsets(A);
627 1 : push_allow_node p1 = push_allow(x.left(), A_sub, equations, W);
628 1 : allow_set A_arrow = alphabet_operations::left_arrow(A, p1.alphabet);
629 1 : push_allow_node q1 = push_allow(x.right(), A_arrow, equations, W);
630 1 : 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 0 : }
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 0 : }
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 0 : }
673 : else
674 : {
675 0 : push_allow_node node(multi_action_name_set{}, delta());
676 0 : push(node);
677 0 : }
678 0 : return;
679 0 : }
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 0 : }
690 : };
691 :
692 : template <template <class, class> class Traverser, typename Node = push_allow_node>
693 : 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 4 : 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 0 : }
726 : }
727 : // W.check_equations(equations);
728 :
729 8 : return result;
730 4 : }
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
|
