Line data Source code
1 : // Author(s): Wieger Wesselink
2 : // Copyright: see the accompanying file COPYING or copy at
3 : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4 : //
5 : // Distributed under the Boost Software License, Version 1.0.
6 : // (See accompanying file LICENSE_1_0.txt or copy at
7 : // http://www.boost.org/LICENSE_1_0.txt)
8 : //
9 : /// \file mcrl2/process/detail/alphabet_push_block.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_BLOCK_H
13 : #define MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_BLOCK_H
14 :
15 : #include "mcrl2/process/detail/alphabet_push_allow.h"
16 :
17 : namespace mcrl2 {
18 :
19 : namespace process {
20 :
21 : struct push_block_cache
22 : {
23 : std::map<process_instance, std::vector<std::pair<std::set<core::identifier_string>, process_instance> > > equation_cache;
24 :
25 : // Caches the alphabet of pCRL equations
26 : std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache;
27 :
28 2 : explicit push_block_cache(std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache_)
29 2 : : pcrl_equation_cache(pcrl_equation_cache_)
30 2 : {}
31 : };
32 :
33 : namespace block_operations {
34 :
35 : template <typename Container>
36 0 : std::set<core::identifier_string> set_union(const std::set<core::identifier_string>& S1, const Container& S2)
37 : {
38 0 : std::set<core::identifier_string> result = S1;
39 0 : result.insert(S2.begin(), S2.end());
40 0 : return result;
41 0 : }
42 :
43 : template <typename Container>
44 0 : std::set<core::identifier_string> set_difference(const std::set<core::identifier_string>& S1, const Container& S2)
45 : {
46 0 : std::set<core::identifier_string> result = S1;
47 0 : for (typename Container::const_iterator i = S2.begin(); i != S2.end(); ++i)
48 : {
49 0 : result.erase(*i);
50 : }
51 0 : return result;
52 0 : }
53 :
54 : inline
55 0 : std::set<core::identifier_string> rename_inverse(const rename_expression_list& R, const std::set<core::identifier_string>& B)
56 : {
57 0 : alphabet_operations::rename_inverse_map Rinverse = alphabet_operations::rename_inverse(R);
58 0 : std::set<core::identifier_string> result;
59 0 : for (const core::identifier_string& i: B)
60 : {
61 0 : auto j = Rinverse.find(i);
62 0 : if (j != Rinverse.end())
63 : {
64 0 : std::vector<core::identifier_string> s = Rinverse[i];
65 0 : result.insert(s.begin(), s.end());
66 0 : }
67 : else
68 : {
69 0 : result.insert(i);
70 : }
71 : }
72 0 : return result;
73 0 : }
74 :
75 : } // namespace block_operations
76 :
77 : namespace detail {
78 :
79 : struct push_block_printer
80 : {
81 : const std::set<core::identifier_string>& B;
82 :
83 1 : explicit push_block_printer(const std::set<core::identifier_string>& B_)
84 1 : : B(B_)
85 1 : {}
86 :
87 1 : std::string print(const std::set<core::identifier_string>& x) const
88 : {
89 1 : return core::detail::print_set(x);
90 : }
91 :
92 : template <typename T>
93 2 : std::string print(const T& x) const
94 : {
95 2 : return process::pp(x);
96 : }
97 :
98 1 : std::string print(const process::allow& x, const allow_set& A1) const
99 : {
100 1 : std::ostringstream out;
101 1 : out << "push_block(" << print(B) << ", " << print(x) << ") = "
102 1 : << "push_allow(" << A1 << ", " << print(x.operand()) << ")" << std::endl;
103 2 : return out.str();
104 1 : }
105 :
106 0 : std::string print(const process::comm& x, const process_expression& result) const
107 : {
108 0 : std::ostringstream out;
109 0 : out << "push_block(" << print(B) << ", " << print(x) << ") = "
110 0 : << print(result) << std::endl;
111 0 : return out.str();
112 0 : }
113 :
114 0 : std::string print(const process::block& x, const std::set<core::identifier_string>& B1) const
115 : {
116 0 : std::ostringstream out;
117 0 : out << "push_block(" << print(B) << ", " << print(x) << ") = "
118 0 : << "push_block(" << print(B1) << ", " << print(x.operand()) << ")" << std::endl;
119 0 : return out.str();
120 0 : }
121 :
122 0 : std::string print(const process::hide& x, const std::set<core::identifier_string>& B1) const
123 : {
124 0 : std::ostringstream out;
125 0 : out << "push_block(" << print(B) << ", " << print(x) << ") = "
126 0 : << "hide(" << print(x.hide_set()) << ", push_block(" << print(B1) << ", " << print(x.operand()) << "))" << std::endl;
127 0 : return out.str();
128 0 : }
129 :
130 0 : std::string print(const process::rename& x, const std::set<core::identifier_string>& B1) const
131 : {
132 0 : std::ostringstream out;
133 0 : const auto& R = x.rename_set();
134 0 : out << "push_block(" << print(B) << ", rename(" << print(R) << ", " << print(x.operand()) << ")) = "
135 0 : << "rename(" << print(R) << ", push_block(" << print(B1) << ", " << print(x.operand()) << "))" << std::endl;
136 0 : return out.str();
137 0 : }
138 : };
139 :
140 : inline
141 : std::string print_B(const std::set<core::identifier_string>& B)
142 : {
143 : std::ostringstream out;
144 : out << "{";
145 : for (auto i = B.begin(); i != B.end(); ++i)
146 : {
147 : if (i != B.begin())
148 : {
149 : out << ", ";
150 : }
151 : out << *i;
152 : }
153 : out << "}";
154 : return out.str();
155 : }
156 :
157 : process_expression push_block(const std::set<core::identifier_string>& B, const process_expression& x, std::vector<process_equation>& equations, push_block_cache& W, data::set_identifier_generator& id_generator);
158 :
159 : template <typename Derived>
160 : struct push_block_builder: public process_expression_builder<Derived>
161 : {
162 : typedef process_expression_builder<Derived> super;
163 : using super::enter;
164 : using super::leave;
165 : using super::apply;
166 : using super::update;
167 :
168 : // used for computing the alphabet
169 : std::vector<process_equation>& equations;
170 : push_block_cache& W;
171 :
172 : // the parameter B
173 : const std::set<core::identifier_string>& B;
174 :
175 : // used for generating process identifiers
176 : data::set_identifier_generator& id_generator;
177 :
178 3 : push_block_builder(std::vector<process_equation>& equations_, push_block_cache& W_, const std::set<core::identifier_string>& B_, data::set_identifier_generator& id_generator_)
179 3 : : equations(equations_), W(W_), B(B_), id_generator(id_generator_)
180 3 : {}
181 :
182 0 : Derived& derived()
183 : {
184 0 : return static_cast<Derived&>(*this);
185 : }
186 :
187 : template <class T>
188 1 : void apply(T& result, const process::action& x)
189 : {
190 : using utilities::detail::contains;
191 1 : if (contains(B, x.label().name()))
192 : {
193 0 : result = delta();
194 : }
195 : else
196 : {
197 1 : result = x;
198 : }
199 1 : }
200 :
201 : template <class T>
202 2 : void apply(T& result, const process::process_instance& x)
203 : {
204 : // Let x = P(e)
205 : // The corresponding equation is P(d) = p
206 2 : auto i = W.equation_cache.find(x);
207 2 : if (i != W.equation_cache.end())
208 : {
209 1 : const std::vector<std::pair<std::set<core::identifier_string>, process_instance> >& v = i->second;
210 1 : for (const auto& j: v)
211 : {
212 1 : if (B == j.first)
213 : {
214 1 : result = j.second;
215 1 : return;
216 : }
217 : }
218 : }
219 :
220 1 : const process_equation& eqn = find_equation(equations, x.identifier());
221 1 : const data::variable_list& d = eqn.formal_parameters();
222 1 : core::identifier_string name = id_generator(x.identifier().name());
223 1 : process_identifier P1(name, x.identifier().variables());
224 1 : const process_expression& p = eqn.expression();
225 :
226 : // Add (P(e), B, P1(e)) to W
227 1 : W.equation_cache[x].push_back(std::make_pair(B, process_instance(P1, x.actual_parameters())));
228 :
229 1 : process_expression p1 = push_block(B, p, equations, W, id_generator);
230 :
231 : // create a new equation P1(d) = p1
232 1 : process_equation eqn1(P1, d, p1);
233 1 : equations.push_back(eqn1);
234 :
235 1 : result = process_instance(P1, x.actual_parameters());
236 1 : }
237 :
238 : template <class T>
239 0 : void apply(T& result, const process::process_instance_assignment& x)
240 : {
241 0 : process_instance x1 = expand_assignments(x, equations);
242 0 : derived().apply(result, x1);
243 0 : }
244 :
245 : template <class T>
246 0 : void apply(T& result, const process::block& x)
247 : {
248 0 : std::set<core::identifier_string> B1 = block_operations::set_union(B, x.block_set());
249 0 : mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
250 0 : result = push_block(B1, x.operand(), equations, W, id_generator);
251 0 : }
252 :
253 : template <class T>
254 0 : void apply(T& result, const process::hide& x)
255 : {
256 0 : const core::identifier_string_list& I = x.hide_set();
257 0 : std::set<core::identifier_string> B1 = block_operations::set_difference(B, I);
258 0 : mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
259 0 : make_hide(result, I, push_block(B1, x.operand(), equations, W, id_generator));
260 0 : }
261 :
262 : template <class T>
263 0 : void apply(T& result, const process::rename& x)
264 : {
265 0 : const rename_expression_list& R = x.rename_set();
266 0 : std::set<core::identifier_string> B1 = block_operations::rename_inverse(R, B);
267 0 : mCRL2log(log::debug) << push_block_printer(B).print(x, B1);
268 0 : process::make_rename(result, R, push_block(B1, x.operand(), equations, W, id_generator));
269 0 : }
270 :
271 0 : bool restrict_(const core::identifier_string& b, const std::set<core::identifier_string>& B, const communication_expression_list& C) const
272 : {
273 : using utilities::detail::contains;
274 0 : for (const communication_expression& i: C)
275 : {
276 0 : core::identifier_string_list gamma = i.action_name().names();
277 0 : const core::identifier_string& c = i.name();
278 0 : if (contains(gamma, b) && !contains(B, c))
279 : {
280 0 : return true;
281 : }
282 : }
283 0 : return false;
284 : }
285 :
286 0 : std::set<core::identifier_string> restrict_block(const std::set<core::identifier_string>& B, const communication_expression_list& C) const
287 : {
288 0 : std::set<core::identifier_string> result;
289 0 : for (auto i = B.begin(); i != B.end(); ++i)
290 : {
291 0 : if (!restrict_(*i, B, C))
292 : {
293 0 : result.insert(*i);
294 : }
295 : }
296 0 : return result;
297 0 : }
298 :
299 : template <class T>
300 0 : void apply(T& result, const process::comm& x)
301 : {
302 0 : std::set<core::identifier_string> B1 = restrict_block(B, x.comm_set());
303 0 : process_expression y = push_block(B1, x.operand(), equations, W, id_generator);
304 0 : result = make_block(core::identifier_string_list(B.begin(), B.end()), make_comm(x.comm_set(), y));
305 0 : mCRL2log(log::debug) << push_block_printer(B).print(x, result);
306 0 : }
307 :
308 : template <class T>
309 1 : void apply(T& result, const process::allow& x)
310 : {
311 2 : allow_set A(alphabet_operations::make_name_set(x.allow_set()));
312 1 : core::identifier_string_list B1(B.begin(), B.end());
313 2 : allow_set A1(alphabet_operations::block(B1, A.A));
314 1 : detail::push_allow_cache W_allow(id_generator, W.pcrl_equation_cache);
315 1 : detail::push_allow_node node = detail::push_allow(x.operand(), A1, equations, W_allow, true);
316 1 : mCRL2log(log::debug) << push_block_printer(B).print(x, A1);
317 1 : result = node.expression;
318 1 : }
319 :
320 : // This function is needed because the linearization algorithm does not handle the case 'delta | delta'.
321 : template <class T>
322 0 : void apply(T& result, const process::sync& x)
323 : {
324 0 : process_expression left;
325 0 : derived().apply(left, x.left());
326 0 : process_expression right;
327 0 : derived().apply(right, x.right());
328 0 : result = make_sync(left, right);
329 0 : }
330 : };
331 :
332 : template <template <class> class Traverser>
333 : struct apply_push_block_builder: public Traverser<apply_push_block_builder<Traverser> >
334 : {
335 : typedef Traverser<apply_push_block_builder<Traverser> > super;
336 : using super::enter;
337 : using super::leave;
338 : using super::apply;
339 : using super::update;
340 :
341 3 : apply_push_block_builder(std::vector<process_equation>& equations, push_block_cache& W, const std::set<core::identifier_string>& B, data::set_identifier_generator& id_generator)
342 3 : : super(equations, W, B, id_generator)
343 3 : {}
344 : };
345 :
346 : inline
347 3 : process_expression push_block(const std::set<core::identifier_string>& B, const process_expression& x, std::vector<process_equation>& equations, push_block_cache& W, data::set_identifier_generator& id_generator)
348 : {
349 3 : apply_push_block_builder<push_block_builder> f(equations, W, B, id_generator);
350 3 : process_expression result;
351 3 : f.apply(result, x);
352 6 : return result;
353 0 : }
354 :
355 : } // namespace detail
356 :
357 : inline
358 2 : process_expression push_block(const core::identifier_string_list& B,
359 : const process_expression& x,
360 : std::vector<process_equation>& equations,
361 : data::set_identifier_generator& id_generator,
362 : std::map<process_identifier, multi_action_name_set>& pcrl_equation_cache
363 : )
364 : {
365 2 : std::set<core::identifier_string> B1(B.begin(), B.end());
366 2 : push_block_cache W(pcrl_equation_cache);
367 4 : return detail::push_block(B1, x, equations, W, id_generator);
368 2 : }
369 :
370 : } // namespace process
371 :
372 : } // namespace mcrl2
373 :
374 : #endif // MCRL2_PROCESS_DETAIL_ALPHABET_PUSH_BLOCK_H
|