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/allow_set.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PROCESS_ALLOW_SET_H
13 : #define MCRL2_PROCESS_ALLOW_SET_H
14 :
15 : #include "mcrl2/process/alphabet_operations.h"
16 : #include "mcrl2/process/utility.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace process {
21 :
22 : struct allow_set;
23 : std::ostream& operator<<(std::ostream& out, const allow_set& x);
24 :
25 : /// \brief Represents the set AI*. If the attribute A_includes_subsets is true, also subsets of the elements are included.
26 : /// An invariant of the allow_set is that elements of A do not contain elements of I. This invariant will be
27 : /// established during construction.
28 : struct allow_set
29 : {
30 : multi_action_name_set A;
31 : bool A_includes_subsets;
32 : std::set<core::identifier_string> I;
33 :
34 : bool is_empty() const
35 : {
36 : return A.empty() && I.empty();
37 : }
38 :
39 : multi_action_name pick_element() const
40 : {
41 : if (!A.empty())
42 : {
43 : return *A.begin();
44 : }
45 : if (!I.empty())
46 : {
47 : multi_action_name alpha;
48 : alpha.insert(*I.begin());
49 : return alpha;
50 : }
51 : throw mcrl2::runtime_error("cannot pick element from empty allow_set!");
52 : }
53 :
54 2 : void establish_invariant()
55 : {
56 2 : multi_action_name_set A1;
57 4 : for (const multi_action_name& i : A)
58 : {
59 2 : A1.insert(alphabet_operations::hide(I, i));
60 : }
61 2 : std::swap(A, A1);
62 2 : assert(check_invariant());
63 2 : }
64 :
65 2 : bool check_invariant() const
66 : {
67 : using utilities::detail::contains;
68 2 : if (I.empty())
69 : {
70 2 : return true;
71 : }
72 0 : for (const multi_action_name& alpha: A)
73 : {
74 0 : for (const core::identifier_string& j: alpha)
75 : {
76 0 : if (contains(I, j))
77 : {
78 0 : return false;
79 : }
80 : }
81 : }
82 0 : return true;
83 : }
84 :
85 : allow_set()
86 : {}
87 :
88 27 : explicit allow_set(const multi_action_name_set& A_, bool A_includes_subsets_ = false, const std::set<core::identifier_string>& I_ = std::set<core::identifier_string>())
89 27 : : A_includes_subsets(A_includes_subsets_), I(I_)
90 : {
91 80 : for (const multi_action_name& i: A_)
92 : {
93 53 : A.insert(alphabet_operations::hide(I_, i));
94 : }
95 27 : }
96 :
97 : /// \brief Returns true if the allow set contains the multi action name alpha.
98 5 : bool contains(const multi_action_name& alpha) const
99 : {
100 5 : multi_action_name beta = alphabet_operations::hide(I, alpha);
101 10 : return beta.empty() || (A_includes_subsets ? alphabet_operations::includes(A, beta) : alphabet_operations::contains(A, beta));
102 5 : }
103 :
104 : /// \brief Returns the intersection of the allow set with alphabet.
105 2 : multi_action_name_set intersect(const multi_action_name_set& alphabet) const
106 : {
107 2 : multi_action_name_set result;
108 4 : for (const multi_action_name& alpha: alphabet)
109 : {
110 2 : if (contains(alpha))
111 : {
112 2 : result.insert(alpha);
113 : }
114 : }
115 2 : multi_action_name tau;
116 2 : if (alphabet.find(tau) != alphabet.end())
117 : {
118 0 : result.insert(tau);
119 : }
120 4 : return result;
121 2 : }
122 :
123 : bool operator==(const allow_set& other) const
124 : {
125 : return A == other.A && A_includes_subsets == other.A_includes_subsets && I == other.I;
126 : }
127 :
128 0 : bool operator<(const allow_set& other) const
129 : {
130 0 : if (A_includes_subsets != other.A_includes_subsets)
131 : {
132 0 : return A_includes_subsets < other.A_includes_subsets;
133 : }
134 0 : if (A.size() != other.A.size())
135 : {
136 0 : return A.size() < other.A.size();
137 : }
138 0 : if (I.size() != other.I.size())
139 : {
140 0 : return I.size() < other.I.size();
141 : }
142 0 : auto m = std::mismatch(A.begin(), A.end(), other.A.begin());
143 0 : if (m.first != A.end())
144 : {
145 0 : return *m.first < *m.second;
146 : }
147 0 : return I < other.I;
148 : }
149 : };
150 :
151 : inline
152 7 : std::ostream& operator<<(std::ostream& out, const allow_set& x)
153 : {
154 7 : if (!x.A.empty())
155 : {
156 7 : out << pp(x.A) << (x.A_includes_subsets ? "@" : "");
157 : }
158 7 : if (!x.I.empty())
159 : {
160 0 : out << "{" << core::pp(x.I) << "}*";
161 : }
162 7 : if (x.A.empty() && x.I.empty())
163 : {
164 0 : out << "{}";
165 : }
166 7 : return out;
167 : }
168 :
169 : // operations on allow_set
170 :
171 : namespace alphabet_operations {
172 :
173 : // Returns true if there is a beta in A that includes alpha
174 : inline
175 : bool subset_includes(const allow_set& A, const multi_action_name& alpha)
176 : {
177 : multi_action_name alpha1 = alphabet_operations::hide(A.I, alpha);
178 : for (const multi_action_name& beta: A.A)
179 : {
180 : if (includes(beta, alpha1))
181 : {
182 : return true;
183 : }
184 : }
185 : return false;
186 : }
187 :
188 : // Returns the intersection of A1 and A
189 : inline
190 : multi_action_name_set set_intersection(const allow_set& A1, const multi_action_name_set& A)
191 : {
192 : multi_action_name_set result;
193 : for (const multi_action_name& alpha: A)
194 : {
195 : if ((A1.A_includes_subsets && subset_includes(A1.A, alpha)) || (!A1.A_includes_subsets && includes(A1.A, alpha)))
196 : {
197 : result.insert(alpha);
198 : }
199 : }
200 : return result;
201 : }
202 :
203 : // Returns the intersection of concat(A1, A2) and A, and a boolean indicating if the intersection actually removed some elements.
204 : inline
205 1 : std::pair<multi_action_name_set, bool> bounded_concat(const multi_action_name_set& A1, const multi_action_name_set& A2, const allow_set& A)
206 : {
207 1 : bool removed = false;
208 1 : multi_action_name_set result;
209 2 : for (const multi_action_name& i: A1)
210 : {
211 2 : for (const multi_action_name& j: A2)
212 : {
213 1 : multi_action_name alpha = multiset_union(i, j);
214 1 : if (A.contains(alpha))
215 : {
216 0 : result.insert(alpha);
217 : }
218 : else
219 : {
220 1 : removed = true;
221 : }
222 1 : }
223 : }
224 2 : return { result, removed };
225 1 : }
226 :
227 : // Returns the intersection of merge(A1, A2) and A
228 : inline
229 1 : std::pair<multi_action_name_set, bool> bounded_merge(const multi_action_name_set& A1, const multi_action_name_set& A2, const allow_set& A)
230 : {
231 1 : std::pair<multi_action_name_set, bool> A1A2 = bounded_concat(A1, A2, A);
232 2 : return { alphabet_operations::set_union(alphabet_operations::set_union(A1, A2), A1A2.first), A1A2.second };
233 1 : }
234 :
235 : // Returns the intersection of left_merge(A1, A2) and A
236 : inline
237 0 : std::pair<multi_action_name_set, bool> bounded_left_merge(const multi_action_name_set& A1, const multi_action_name_set& A2, const allow_set& A)
238 : {
239 0 : return bounded_merge(A1, A2, A);
240 : }
241 :
242 : // Returns the intersection of sync(A1, A2) and A
243 : inline
244 : std::pair<multi_action_name_set, bool> bounded_sync(const multi_action_name_set& A1, const multi_action_name_set& A2, const allow_set& A)
245 : {
246 : return bounded_concat(A1, A2, A);
247 : }
248 :
249 : inline
250 2 : allow_set block(const core::identifier_string_list& B, const allow_set& x)
251 : {
252 2 : if (x.A_includes_subsets)
253 : {
254 2 : return allow_set(alphabet_operations::hide(B, x.A), x.A_includes_subsets, alphabet_operations::hide(B, x.I));
255 : }
256 : else
257 : {
258 2 : return allow_set(alphabet_operations::block(B, x.A), x.A_includes_subsets, alphabet_operations::hide(B, x.I));
259 : }
260 : }
261 :
262 : inline
263 0 : allow_set hide_inverse(const core::identifier_string_list& I, const allow_set& x)
264 : {
265 0 : allow_set result = x;
266 0 : result.A = alphabet_operations::hide_inverse(I, result.A, result.A_includes_subsets);
267 0 : result.I.insert(I.begin(), I.end());
268 0 : result.establish_invariant();
269 0 : return result;
270 0 : }
271 :
272 : inline
273 2 : allow_set allow(const action_name_multiset_list& V, const allow_set& x)
274 : {
275 2 : multi_action_name_set A;
276 8 : for (const action_name_multiset& v: V)
277 : {
278 6 : const core::identifier_string_list& names = v.names();
279 6 : multi_action_name beta(names.begin(), names.end());
280 6 : bool add = x.A_includes_subsets ? alphabet_operations::includes(x.A, alphabet_operations::hide(x.I, beta)) : alphabet_operations::contains(x.A, alphabet_operations::hide(x.I, beta));
281 6 : if (add)
282 : {
283 4 : A.insert(beta);
284 : }
285 6 : }
286 4 : return allow_set(A);
287 2 : }
288 :
289 : inline
290 6 : allow_set rename_inverse(const rename_expression_list& R, const allow_set& x)
291 : {
292 12 : allow_set result(alphabet_operations::rename_inverse(R, x.A, x.A_includes_subsets), x.A_includes_subsets, rename_inverse(R, x.I));
293 6 : mCRL2log(log::trace) << "rename_inverse(" << R << ", " << x << ") = " << result << std::endl;
294 6 : return result;
295 0 : }
296 :
297 : inline
298 2 : allow_set comm_inverse(const communication_expression_list& C, const allow_set& x)
299 : {
300 4 : allow_set result(comm_inverse1(C, x.A), x.A_includes_subsets, comm_inverse(C, x.I));
301 2 : mCRL2log(log::trace) << "comm_inverse(" << C << ", " << x << ") = " << result << std::endl;
302 2 : return result;
303 0 : }
304 :
305 : inline
306 1 : allow_set left_arrow(const allow_set& x, const multi_action_name_set& A)
307 : {
308 1 : allow_set result = x;
309 1 : if (!x.A_includes_subsets)
310 : {
311 1 : result.A = left_arrow2(x.A, x.I, A);
312 : }
313 1 : result.establish_invariant();
314 1 : mCRL2log(log::trace) << "left_arrow(" << x << ", " << process::pp(A) << ") = " << result << std::endl;
315 1 : return result;
316 0 : }
317 :
318 : inline
319 1 : allow_set subsets(const allow_set& x)
320 : {
321 1 : allow_set result = x;
322 1 : result.A_includes_subsets = true;
323 1 : if (result.A.size() <= 1000)
324 : {
325 1 : result.A = alphabet_operations::remove_subsets(result.A);
326 : }
327 : else
328 : {
329 0 : mCRL2log(log::debug) << "allow_set::subsets: skipped remove_subsets on a set of " << result.A.size() << " elements." << std::endl;
330 : }
331 1 : result.establish_invariant();
332 1 : return result;
333 0 : }
334 :
335 : } // namespace alphabet_operations
336 :
337 : } // namespace process
338 :
339 : } // namespace mcrl2
340 :
341 : #endif // MCRL2_PROCESS_ALLOW_SET_H
|
