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/alphabet_operations.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PROCESS_ALPHABET_OPERATIONS_H
13 : #define MCRL2_PROCESS_ALPHABET_OPERATIONS_H
14 :
15 : #include "mcrl2/process/communication_expression.h"
16 : #include "mcrl2/process/multi_action_name.h"
17 : #include "mcrl2/process/rename_expression.h"
18 : #include "mcrl2/utilities/sequence.h"
19 :
20 : namespace mcrl2 {
21 :
22 : namespace process {
23 :
24 : namespace alphabet_operations {
25 :
26 : //-----------------------------------------------------//
27 : // multi_action_name operations
28 : //-----------------------------------------------------//
29 :
30 : // Returns true if the multiset y is contained in x
31 : inline
32 6092 : bool includes(const multi_action_name& x, const multi_action_name& y)
33 : {
34 6092 : return std::includes(x.begin(), x.end(), y.begin(), y.end());
35 : }
36 :
37 : inline
38 : bool contains(const multi_action_name& alpha, const core::identifier_string& a)
39 : {
40 : return alpha.find(a) != alpha.end();
41 : }
42 :
43 : // Returns alpha \ beta
44 : inline
45 9 : multi_action_name multiset_difference(const multi_action_name& alpha, const multi_action_name& beta)
46 : {
47 9 : multi_action_name result = alpha;
48 19 : for (const core::identifier_string& i: beta)
49 : {
50 10 : multi_action_name::iterator j = result.find(i);
51 10 : if (j != result.end())
52 : {
53 10 : result.erase(j);
54 : }
55 : }
56 9 : return result;
57 0 : }
58 :
59 : inline
60 187 : multi_action_name multiset_union(const multi_action_name& alpha, const multi_action_name& beta)
61 : {
62 187 : multi_action_name result;
63 187 : std::merge(alpha.begin(), alpha.end(), beta.begin(), beta.end(), std::inserter(result, result.end()));
64 187 : return result;
65 0 : }
66 :
67 : //-----------------------------------------------------//
68 : // multi_action_name_set operations
69 : //-----------------------------------------------------//
70 :
71 : inline
72 1 : multi_action_name_set make_name_set(const action_name_multiset_list& v)
73 : {
74 1 : multi_action_name_set result;
75 2 : for (const action_name_multiset& i: v)
76 : {
77 1 : const core::identifier_string_list& names = i.names();
78 1 : result.insert(multi_action_name(names.begin(), names.end()));
79 : }
80 1 : return result;
81 0 : }
82 :
83 : inline
84 7 : bool contains(const multi_action_name_set& A, const multi_action_name& a)
85 : {
86 : // note that A implicitly contains the empty multi_action_name
87 7 : return a.empty() || A.find(a) != A.end();
88 : }
89 :
90 : inline
91 : // Returns true if A contains an x such that includes(x, y)
92 395 : bool includes(const multi_action_name_set& A, const multi_action_name& y)
93 : {
94 : // degenerate case
95 395 : if (A.empty() && y.empty())
96 : {
97 0 : return true;
98 : }
99 6232 : for (const multi_action_name& alpha: A)
100 : {
101 6058 : if (includes(alpha, y))
102 : {
103 221 : return true;
104 : }
105 : }
106 174 : return false;
107 : }
108 :
109 : inline
110 : bool subset_includes(const multi_action_name_set& A, const multi_action_name& x)
111 : {
112 : for (const multi_action_name& a: A)
113 : {
114 : if (includes(a, x))
115 : {
116 : return true;
117 : }
118 : }
119 : return false;
120 : }
121 :
122 : inline
123 : multi_action_name_set set_difference(const multi_action_name_set& A1, const multi_action_name_set& A2)
124 : {
125 : multi_action_name_set result;
126 : std::set_difference(A1.begin(), A1.end(), A2.begin(), A2.end(), std::inserter(result, result.end()));
127 : return result;
128 : }
129 :
130 : inline
131 52 : multi_action_name_set set_union(const multi_action_name_set& A1, const multi_action_name_set& A2)
132 : {
133 52 : multi_action_name_set result;
134 52 : std::set_union(A1.begin(), A1.end(), A2.begin(), A2.end(), std::inserter(result, result.end()));
135 52 : return result;
136 0 : }
137 :
138 : inline
139 : multi_action_name_set set_intersection(const multi_action_name_set& A1, const multi_action_name_set& A2)
140 : {
141 : multi_action_name_set result;
142 : std::set_intersection(A1.begin(), A1.end(), A2.begin(), A2.end(), std::inserter(result, result.end()));
143 : return result;
144 : }
145 :
146 : // Removes elements of A that are a subset of another element.
147 : inline
148 1 : multi_action_name_set remove_subsets(const multi_action_name_set& A)
149 : {
150 1 : multi_action_name_set result;
151 2 : for (const multi_action_name& alpha: A)
152 : {
153 1 : if (!includes(result, alpha))
154 : {
155 1 : result.insert(alpha);
156 : }
157 : }
158 1 : return result;
159 0 : }
160 :
161 : //-----------------------------------------------------//
162 : // block operations
163 : //-----------------------------------------------------//
164 :
165 : inline
166 5 : multi_action_name_set block(const core::identifier_string_list& B, const multi_action_name_set& A, bool A_includes_subsets = false)
167 : {
168 5 : multi_action_name_set result;
169 5 : multi_action_name beta(B.begin(), B.end());
170 :
171 5 : if (A_includes_subsets)
172 : {
173 4 : for (multi_action_name alpha: A)
174 : {
175 6 : for (const core::identifier_string& b: B)
176 : {
177 3 : alpha.erase(b);
178 : }
179 3 : if (!alpha.empty())
180 : {
181 3 : result.insert(alpha);
182 : }
183 3 : }
184 : }
185 : else
186 : {
187 12 : for (const multi_action_name& alpha: A)
188 : {
189 8 : if (utilities::detail::has_empty_intersection(beta.begin(), beta.end(), alpha.begin(), alpha.end()))
190 : {
191 3 : result.insert(alpha);
192 : }
193 : }
194 : }
195 10 : return result;
196 5 : }
197 :
198 : //-----------------------------------------------------//
199 : // hide operations
200 : //-----------------------------------------------------//
201 :
202 : // Hides elements in I from alpha
203 : inline
204 : multi_action_name hide(const multi_action_name& alpha, const std::set<core::identifier_string>& I)
205 : {
206 : using utilities::detail::contains;
207 : multi_action_name result;
208 : for (const core::identifier_string& a: alpha)
209 : {
210 : if (!contains(I, a))
211 : {
212 : result.insert(a);
213 : }
214 : }
215 : return result;
216 : }
217 :
218 : // Hides (or: removes) elements in I from C
219 : inline
220 2 : std::set<core::identifier_string> hide(const core::identifier_string_list& I, const std::set<core::identifier_string>& J)
221 : {
222 : using utilities::detail::contains;
223 2 : std::set<core::identifier_string> result;
224 2 : for (const core::identifier_string& j: J)
225 : {
226 0 : if (!contains(I, j))
227 : {
228 0 : result.insert(j);
229 : }
230 : }
231 2 : return result;
232 0 : }
233 :
234 : inline
235 67 : multi_action_name hide(const std::set<core::identifier_string>& I, const multi_action_name& alpha)
236 : {
237 : using utilities::detail::contains;
238 67 : multi_action_name result;
239 176 : for (const core::identifier_string& i: alpha)
240 : {
241 109 : if (!contains(I, i))
242 : {
243 109 : result.insert(i);
244 : }
245 : }
246 67 : return result;
247 0 : }
248 :
249 : template <typename IdentifierContainer>
250 1 : multi_action_name_set hide(const IdentifierContainer& I, const multi_action_name_set& A, bool /* A_includes_subsets */ = false)
251 : {
252 1 : multi_action_name m(I.begin(), I.end());
253 1 : multi_action_name_set result;
254 4 : for (multi_action_name alpha: A)
255 : {
256 9 : for (const core::identifier_string& i: I)
257 : {
258 3 : alpha.erase(i);
259 : }
260 3 : result.insert(alpha);
261 : }
262 2 : return result;
263 1 : }
264 :
265 : inline
266 1 : multi_action_name_set hide_inverse(const core::identifier_string_list& I, const multi_action_name_set& A, bool A_includes_subsets = false)
267 : {
268 1 : return block(I, A, A_includes_subsets);
269 : }
270 :
271 : //-----------------------------------------------------//
272 : // merge/left_merge/sync operations
273 : //-----------------------------------------------------//
274 :
275 : inline
276 26 : multi_action_name_set concat(const multi_action_name_set& A1, const multi_action_name_set& A2)
277 : {
278 26 : multi_action_name_set result;
279 51 : for (const multi_action_name& i: A1)
280 : {
281 204 : for (const multi_action_name& j: A2)
282 : {
283 179 : result.insert(multiset_union(i, j));
284 : }
285 : }
286 26 : return result;
287 0 : }
288 :
289 : // Returns true if alpha in concat(A1, A2).
290 : // TODO: Make the implementation more inefficient!
291 : inline
292 : bool concat_includes(const multi_action_name_set& A1, const multi_action_name_set& A2, const multi_action_name& alpha)
293 : {
294 : for (const multi_action_name& alpha1: A1)
295 : {
296 : for (const multi_action_name& alpha2: A2)
297 : {
298 : if (alpha == multiset_union(alpha1, alpha2))
299 : {
300 : return true;
301 : }
302 : }
303 : }
304 : return false;
305 : }
306 :
307 : // Returns the intersection of concat(A1, A2) and subsets(A)
308 : inline
309 : multi_action_name_set bounded_concat(const multi_action_name_set& A1, const multi_action_name_set& A2, const multi_action_name_set& A)
310 : {
311 : multi_action_name_set result;
312 : for (const multi_action_name& i: A1)
313 : {
314 : for (const multi_action_name& j: A2)
315 : {
316 : multi_action_name alpha = multiset_union(i, j);
317 : if (subset_includes(A, alpha))
318 : {
319 : result.insert(alpha);
320 : }
321 : }
322 : }
323 : return result;
324 : }
325 :
326 : inline
327 5 : multi_action_name_set left_arrow1(const multi_action_name_set& A1, const multi_action_name_set& A2)
328 : {
329 5 : multi_action_name_set result = A1; // needed because tau is not explicitly stored
330 11 : for (const multi_action_name& beta: A2)
331 : {
332 16 : for (const multi_action_name& gamma: A1)
333 : {
334 10 : if (includes(gamma, beta))
335 : {
336 8 : multi_action_name alpha = multiset_difference(gamma, beta);
337 8 : if (!alpha.empty())
338 : {
339 6 : result.insert(alpha);
340 : }
341 8 : }
342 : }
343 : }
344 5 : return result;
345 0 : }
346 :
347 : inline
348 : multi_action_name_set left_arrow(const multi_action_name_set& A1, bool A1_includes_subsets, const multi_action_name_set& A2)
349 : {
350 : multi_action_name_set result;
351 : if (A1_includes_subsets)
352 : {
353 : result = A1;
354 : }
355 : else
356 : {
357 : result = set_union(A1, left_arrow1(A1, A2));
358 : }
359 : return result;
360 : }
361 :
362 : // returns left_arrow(A I*, A2)
363 : inline
364 1 : multi_action_name_set left_arrow2(const multi_action_name_set& A, const std::set<core::identifier_string>& I, const multi_action_name_set& A2)
365 : {
366 1 : multi_action_name_set result = A; // needed because tau is not explicitly stored
367 2 : for (const multi_action_name& alpha2: A2)
368 : {
369 1 : multi_action_name beta = hide(I, alpha2);
370 2 : for (const multi_action_name& alpha: A)
371 : {
372 1 : if (includes(alpha, beta))
373 : {
374 1 : multi_action_name gamma = multiset_difference(alpha, beta);
375 1 : if (!gamma.empty())
376 : {
377 0 : result.insert(hide(I, gamma));
378 : }
379 1 : }
380 : }
381 1 : }
382 1 : return result;
383 0 : }
384 :
385 : inline
386 22 : multi_action_name_set merge(const multi_action_name_set& A1, const multi_action_name_set& A2)
387 : {
388 44 : return set_union(set_union(A1, A2), concat(A1, A2));
389 : }
390 :
391 : // Returns the intersection of merge(A1, A2) and subsets(A)
392 : inline
393 : multi_action_name_set bounded_merge(const multi_action_name_set& A1, const multi_action_name_set& A2, const multi_action_name_set& A)
394 : {
395 : return set_union(set_union(A1, A2), bounded_concat(A1, A2, A));
396 : }
397 :
398 : inline
399 : multi_action_name_set left_merge(const multi_action_name_set& A1, const multi_action_name_set& A2)
400 : {
401 : return merge(A1, A2);
402 : }
403 :
404 : inline
405 2 : multi_action_name_set sync(const multi_action_name_set& A1, const multi_action_name_set& A2)
406 : {
407 2 : return concat(A1, A2);
408 : }
409 :
410 : // Returns the intersection of sync(A1, A2) and subsets(A)
411 : inline
412 : multi_action_name_set bounded_sync(const multi_action_name_set& A1, const multi_action_name_set& A2, const multi_action_name_set& A)
413 : {
414 : return bounded_concat(A1, A2, A);
415 : }
416 :
417 : //-----------------------------------------------------//
418 : // comm operations
419 : //-----------------------------------------------------//
420 :
421 : inline
422 4 : std::pair<multi_action_name, multi_action_name> apply_comm_inverse(const communication_expression& x, const multi_action_name& alpha1, const multi_action_name& alpha2)
423 : {
424 4 : const core::identifier_string& c = x.name();
425 4 : core::identifier_string_list lhs = x.action_name().names();
426 4 : std::pair<multi_action_name, multi_action_name> result;
427 4 : result.first = alpha1;
428 4 : result.second = alpha2;
429 4 : result.first.erase(result.first.find(c));
430 4 : result.second.insert(lhs.begin(), lhs.end());
431 8 : return result;
432 4 : }
433 :
434 : // Add inverse communication to A
435 : inline
436 2 : void apply_comm_inverse(const communication_expression& gamma, multi_action_name_set& A)
437 : {
438 2 : std::vector<multi_action_name> to_be_added;
439 2 : const core::identifier_string& c = gamma.name();
440 2 : core::identifier_string_list lhs = gamma.action_name().names();
441 :
442 5 : for (const multi_action_name& alpha: A)
443 : {
444 3 : std::size_t n = alpha.count(c);
445 3 : if (n > 0)
446 : {
447 3 : multi_action_name beta = alpha;
448 7 : for (std::size_t k = 0; k < n; k++)
449 : {
450 4 : beta.erase(beta.find(c));
451 4 : beta.insert(lhs.begin(), lhs.end());
452 4 : to_be_added.push_back(beta);
453 : }
454 3 : }
455 : }
456 2 : A.insert(to_be_added.begin(), to_be_added.end());
457 2 : }
458 :
459 : inline
460 7 : void comm_inverse(const communication_expression_list& C, const multi_action_name& alpha1, const multi_action_name& alpha2, multi_action_name_set& result)
461 : {
462 : using utilities::detail::contains;
463 7 : result.insert(alphabet_operations::multiset_union(alpha1, alpha2));
464 14 : for (const communication_expression& c: C)
465 : {
466 7 : if (contains(alpha1, c.name()))
467 : {
468 4 : std::pair<multi_action_name, multi_action_name> beta = apply_comm_inverse(c, alpha1, alpha2);
469 4 : comm_inverse(C, beta.first, beta.second, result);
470 4 : }
471 : }
472 7 : }
473 :
474 : inline
475 2 : multi_action_name_set comm_inverse1(const communication_expression_list& C, const multi_action_name_set& A)
476 : {
477 2 : multi_action_name_set result;
478 2 : multi_action_name empty;
479 5 : for (const multi_action_name& alpha: A)
480 : {
481 3 : comm_inverse(C, alpha, empty, result);
482 : }
483 4 : return result;
484 2 : }
485 :
486 : inline
487 2 : multi_action_name_set comm_inverse(const communication_expression_list& C, const multi_action_name_set& A, bool /* A_includes_subsets */ = false)
488 : {
489 2 : multi_action_name_set result = A;
490 4 : for (const communication_expression& c: C)
491 : {
492 2 : apply_comm_inverse(c, result);
493 : }
494 2 : return result;
495 0 : }
496 :
497 : // Note that the result is flattened.
498 : inline
499 2 : std::set<core::identifier_string> comm_inverse(const communication_expression_list& C, const std::set<core::identifier_string>& I)
500 : {
501 2 : std::set<core::identifier_string> result = I;
502 2 : for (const core::identifier_string& i: I)
503 : {
504 0 : for (const communication_expression& j: C)
505 : {
506 0 : if (i == j.name())
507 : {
508 0 : core::identifier_string_list lhs = j.action_name().names();
509 0 : result.insert(lhs.begin(), lhs.end());
510 0 : }
511 : }
512 : }
513 2 : return result;
514 0 : }
515 :
516 : inline
517 2 : void apply_comm(const communication_expression& c, multi_action_name_set& A)
518 : {
519 2 : core::identifier_string_list names = c.action_name().names();
520 2 : const core::identifier_string& a = c.name();
521 2 : multi_action_name alpha(names.begin(), names.end());
522 : // c == alpha -> a
523 :
524 2 : multi_action_name_set to_be_added;
525 10 : for (multi_action_name beta: A)
526 : {
527 18 : while (includes(beta, alpha))
528 : {
529 30 : for (const core::identifier_string& a: alpha)
530 : {
531 20 : beta.erase(beta.find(a));
532 : }
533 10 : beta.insert(a);
534 10 : to_be_added.insert(beta);
535 : }
536 8 : }
537 2 : A.insert(to_be_added.begin(), to_be_added.end());
538 2 : }
539 :
540 : inline
541 2 : multi_action_name_set comm(const communication_expression_list& C, const multi_action_name_set& A, bool /* A_includes_subsets */ = false)
542 : {
543 2 : multi_action_name_set result = A;
544 :
545 : // sequentially apply the communication rules to result
546 4 : for (const communication_expression& c: C)
547 : {
548 2 : apply_comm(c, result);
549 : }
550 :
551 2 : return result;
552 0 : }
553 :
554 : inline
555 0 : communication_expression_list filter_comm_set(const communication_expression_list& C, const multi_action_name_set& alphabet)
556 : {
557 0 : std::vector<communication_expression> result;
558 0 : for (const communication_expression& c: C)
559 : {
560 0 : core::identifier_string_list lhs = c.action_name().names();
561 0 : multi_action_name alpha(lhs.begin(), lhs.end());
562 0 : if (includes(alphabet, alpha))
563 : {
564 0 : result.push_back(c);
565 : }
566 0 : }
567 0 : return communication_expression_list(result.begin(), result.end());
568 0 : }
569 :
570 : //-----------------------------------------------------//
571 : // rename operations
572 : //-----------------------------------------------------//
573 :
574 : // returns true if x is a source of one of the rename rules in R
575 : inline
576 21 : bool is_source(const rename_expression_list& R, const core::identifier_string& x)
577 : {
578 48 : for (const rename_expression& r: R)
579 : {
580 27 : if (r.source() == x)
581 : {
582 0 : return true;
583 : }
584 : }
585 21 : return false;
586 : }
587 :
588 : inline
589 12 : core::identifier_string apply_rename(const rename_expression_list& R, const core::identifier_string& x)
590 : {
591 20 : for (const rename_expression& r: R)
592 : {
593 18 : if (x == r.source())
594 : {
595 10 : return r.target();
596 : }
597 : }
598 2 : return x;
599 : }
600 :
601 : inline
602 4 : multi_action_name apply_rename(const rename_expression_list& R, const multi_action_name& a)
603 : {
604 4 : multi_action_name result;
605 16 : for (const core::identifier_string& i: a)
606 : {
607 12 : result.insert(apply_rename(R, i));
608 : }
609 4 : return result;
610 0 : }
611 :
612 : /// \brief Computes R(A)
613 : inline
614 2 : multi_action_name_set rename(const rename_expression_list& R, const multi_action_name_set& A, bool /* A_includes_subsets */ = false)
615 : {
616 2 : multi_action_name_set result;
617 6 : for (const multi_action_name& alpha: A)
618 : {
619 4 : result.insert(apply_rename(R, alpha));
620 : }
621 2 : return result;
622 0 : }
623 :
624 : typedef std::map<core::identifier_string, std::vector<core::identifier_string> > rename_inverse_map;
625 :
626 : // Example: R = {b -> c}, then rename_inverse(R) = {b -> [], c -> [b, c]}
627 : inline
628 18 : rename_inverse_map rename_inverse(const rename_expression_list& R)
629 : {
630 18 : rename_inverse_map Rinverse;
631 39 : for (auto i = R.begin(); i != R.end(); ++i)
632 : {
633 21 : Rinverse[i->target()].push_back(i->source());
634 21 : if (!is_source(R, i->target()))
635 : {
636 21 : Rinverse[i->target()].push_back(i->target());
637 : }
638 21 : Rinverse[i->source()]; // this is to make sure that i->source() is in the map
639 : }
640 18 : return Rinverse;
641 0 : }
642 :
643 : inline
644 : std::string print_rename_inverse_map(const rename_inverse_map& m)
645 : {
646 : std::ostringstream out;
647 : out << "{ ";
648 : for (auto i = m.begin(); i != m.end(); ++i)
649 : {
650 : if (i != m.begin())
651 : {
652 : out << ", ";
653 : }
654 : out << core::pp(i->first) << " -> [";
655 : const std::vector<core::identifier_string>& v = i->second;
656 : for (auto j = v.begin(); j != v.end(); ++j)
657 : {
658 : if (j != v.begin())
659 : {
660 : out << ", ";
661 : }
662 : out << *j;
663 : }
664 : out << "]";
665 : }
666 : out << " }";
667 : return out.str();
668 : }
669 :
670 : struct rename_inverse_apply
671 : {
672 : const multi_action_name& alpha;
673 : const std::vector<core::identifier_string>& beta;
674 : multi_action_name_set& A;
675 :
676 18 : rename_inverse_apply(const multi_action_name& alpha_, const std::vector<core::identifier_string>& beta_, multi_action_name_set& A_)
677 18 : : alpha(alpha_), beta(beta_), A(A_)
678 18 : {}
679 :
680 30 : void operator()()
681 : {
682 30 : multi_action_name gamma = alpha;
683 30 : gamma.insert(beta.begin(), beta.end());
684 30 : A.insert(gamma);
685 30 : }
686 : };
687 :
688 : inline
689 6 : std::set<core::identifier_string> rename_inverse(const rename_expression_list& R, const std::set<core::identifier_string>& I)
690 : {
691 6 : alphabet_operations::rename_inverse_map Rinverse = alphabet_operations::rename_inverse(R);
692 :
693 6 : std::set<core::identifier_string> result;
694 6 : for (const core::identifier_string& i: I)
695 : {
696 0 : auto j = Rinverse.find(i);
697 0 : if (j != Rinverse.end())
698 : {
699 0 : result.insert(j->second.begin(), j->second.end());
700 : }
701 : else
702 : {
703 0 : result.insert(i);
704 : }
705 : }
706 12 : return result;
707 6 : }
708 :
709 : inline
710 18 : void rename_inverse(const rename_inverse_map& Rinverse, const multi_action_name& x, bool x_includes_subsets, multi_action_name_set& result)
711 : {
712 18 : std::vector<std::vector<core::identifier_string> > V;
713 :
714 18 : multi_action_name alpha = x;
715 :
716 : // remove elements that appear in Rinverse, and put the replacements in V
717 52 : for (auto i = alpha.begin(); i != alpha.end(); )
718 : {
719 34 : auto j = Rinverse.find(*i);
720 34 : if (j != Rinverse.end())
721 : {
722 32 : alpha.erase(i++);
723 32 : if (!j->second.empty() || !x_includes_subsets)
724 : {
725 30 : V.push_back(j->second);
726 : }
727 : }
728 : else
729 : {
730 2 : ++i;
731 : }
732 : }
733 :
734 : // v will hold a replacement
735 18 : std::vector<core::identifier_string> v(V.size());
736 :
737 : // generate all permutations of the replacements in V, and put them in result
738 18 : utilities::foreach_sequence(V, v.begin(), rename_inverse_apply(alpha, v, result));
739 18 : }
740 :
741 : /// \brief Computes R^[-1}(A)
742 : inline
743 12 : multi_action_name_set rename_inverse(const rename_expression_list& R, const multi_action_name_set& A, bool A_includes_subsets = false)
744 : {
745 12 : rename_inverse_map Rinverse = rename_inverse(R);
746 :
747 12 : multi_action_name_set result;
748 30 : for (const multi_action_name& alpha: A)
749 : {
750 18 : rename_inverse(Rinverse, alpha, A_includes_subsets, result);
751 : }
752 24 : return result;
753 12 : }
754 :
755 : //-----------------------------------------------------//
756 : // allow operations
757 : //-----------------------------------------------------//
758 :
759 : inline
760 4 : multi_action_name_set allow(const action_name_multiset_list& V, const multi_action_name_set& A, bool A_includes_subsets = false)
761 : {
762 4 : multi_action_name_set result;
763 :
764 13 : for (const action_name_multiset& s: V)
765 : {
766 9 : const core::identifier_string_list& names = s.names();
767 9 : multi_action_name v(names.begin(), names.end());
768 29 : for (const multi_action_name& alpha: A)
769 : {
770 20 : bool keep = A_includes_subsets ? includes(alpha, v) : alpha == v;
771 20 : if (keep)
772 : {
773 7 : result.insert(v);
774 : }
775 : }
776 9 : }
777 4 : return result;
778 0 : }
779 :
780 : } // namespace alphabet_operations
781 :
782 : } // namespace process
783 :
784 : } // namespace mcrl2
785 :
786 : #endif // MCRL2_PROCESS_ALPHABET_OPERATIONS_H
|
