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/pbes/detail/stategraph_local_algorithm.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_LOCAL_ALGORITHM_H
13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_LOCAL_ALGORITHM_H
14 :
15 : #include "mcrl2/pbes/algorithms.h"
16 : #include "mcrl2/pbes/detail/stategraph_algorithm.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace pbes_system {
21 :
22 : namespace detail {
23 :
24 : struct default_rules_predicate
25 : {
26 : const local_control_flow_graph& V;
27 :
28 11 : default_rules_predicate(const local_control_flow_graph& V_)
29 11 : : V(V_)
30 11 : {}
31 :
32 15 : bool operator()(const core::identifier_string& X, std::size_t i) const
33 : {
34 15 : return V.has_label(X, i);
35 : }
36 : };
37 :
38 : class belongs_relation
39 : {
40 : protected:
41 : typedef std::map<core::identifier_string, std::set<data::variable> > belongs_map;
42 :
43 : belongs_map m_belongs_map;
44 :
45 : public:
46 18 : const std::set<data::variable>& operator[](const core::identifier_string& X) const
47 : {
48 18 : auto i = m_belongs_map.find(X);
49 18 : if (i == m_belongs_map.end())
50 : {
51 0 : throw mcrl2::runtime_error("unknown key encountered in belongs_relation::operator[]");
52 : }
53 18 : return i->second;
54 : }
55 :
56 : belongs_map::iterator begin()
57 : {
58 : return m_belongs_map.begin();
59 : }
60 :
61 6 : belongs_map::const_iterator begin() const
62 : {
63 6 : return m_belongs_map.begin();
64 : }
65 :
66 : belongs_map::iterator end()
67 : {
68 : return m_belongs_map.end();
69 : }
70 :
71 19 : belongs_map::const_iterator end() const
72 : {
73 19 : return m_belongs_map.end();
74 : }
75 :
76 : belongs_map::iterator find(const core::identifier_string& X)
77 : {
78 : return m_belongs_map.find(X);
79 : }
80 :
81 13 : belongs_map::const_iterator find(const core::identifier_string& X) const
82 : {
83 13 : return m_belongs_map.find(X);
84 : }
85 :
86 13 : std::set<data::variable>& operator[](const core::identifier_string& X)
87 : {
88 13 : return m_belongs_map[X];
89 : }
90 :
91 : std::size_t size() const
92 : {
93 : return m_belongs_map.size();
94 : }
95 :
96 : std::string print() const
97 : {
98 : std::ostringstream out;
99 : out << "{";
100 : for (auto i = m_belongs_map.begin(); i != m_belongs_map.end(); ++i)
101 : {
102 : if (i != m_belongs_map.begin())
103 : {
104 : out << ", ";
105 : }
106 : out << i->first << " -> " << core::detail::print_set(i->second);
107 : }
108 : out << "}";
109 : return out.str();
110 : }
111 : };
112 :
113 : /// \brief Algorithm class for the local variant of the stategraph algorithm
114 : class stategraph_local_algorithm: public stategraph_algorithm
115 : {
116 : public:
117 : typedef stategraph_algorithm super;
118 :
119 : protected:
120 : // m_belongs[k] corresponds with m_control_flow_graphs[k]
121 : std::vector<belongs_relation> m_belongs;
122 :
123 : // if true, marking updates will be cached in the nodes of the local CFGs
124 : bool m_cache_marking_updates;
125 :
126 : std::size_t m_marking_rewrite_count;
127 :
128 : std::size_t m_marking_rewrite_cached_count;
129 :
130 : std::vector<core::identifier_string> binding_variable_names() const
131 : {
132 : std::vector<core::identifier_string> result;
133 : auto const& equations = m_pbes.equations();
134 : for (const stategraph_equation& equation: equations)
135 : {
136 : result.push_back(equation.variable().name());
137 : }
138 : return result;
139 : }
140 :
141 : struct vertex_pair
142 : {
143 : const local_control_flow_graph_vertex* u;
144 : const local_control_flow_graph_vertex* v;
145 : std::size_t k; // index of the graph
146 :
147 0 : vertex_pair(const local_control_flow_graph_vertex* u_, const local_control_flow_graph_vertex* v_, std::size_t k_)
148 0 : : u(u_), v(v_), k(k_)
149 0 : {}
150 :
151 0 : bool operator<(const vertex_pair& other) const
152 : {
153 0 : return u < other.u || (u == other.u && v < other.v);
154 : }
155 : };
156 :
157 : struct equation_label_pair
158 : {
159 : const core::identifier_string X;
160 : std::size_t i; // label
161 :
162 0 : equation_label_pair(const core::identifier_string& X_, std::size_t i_)
163 0 : : X(X_), i(i_)
164 0 : {}
165 :
166 0 : bool operator<(const equation_label_pair& other) const
167 : {
168 0 : return X < other.X || (X == other.X && i < other.i);
169 : }
170 : };
171 :
172 : // maps (X, i) to the set of all edges with label i and source vertex with name X
173 : std::map<core::identifier_string, std::map<std::size_t, std::set<vertex_pair> > > m_edge_index;
174 :
175 0 : void compute_edge_index()
176 : {
177 0 : for (std::size_t k = 0; k < m_local_control_flow_graphs.size(); k++)
178 : {
179 0 : auto const& Gk = m_local_control_flow_graphs[k];
180 0 : auto const& vertices = Gk.vertices;
181 0 : for (const auto& u: vertices)
182 : {
183 0 : auto const& X = u.name();
184 0 : auto const& outgoing_edges = u.outgoing_edges();
185 0 : for(const auto& e: outgoing_edges)
186 : {
187 0 : auto const& v = *(e.first);
188 0 : auto const& I = e.second;
189 0 : for (std::size_t i: I)
190 : {
191 0 : m_edge_index[X][i].insert(vertex_pair(&u, &v, k));
192 : }
193 : }
194 : }
195 : }
196 0 : }
197 :
198 0 : std::string print_edge_index()
199 : {
200 0 : mCRL2log(log::debug) << "--- computed marking edge index ---" << std::endl;
201 0 : auto const& equations = m_pbes.equations();
202 0 : std::ostringstream out;
203 :
204 0 : for (const stategraph_equation& eq_X: equations)
205 : {
206 0 : auto const& X = eq_X.variable().name();
207 0 : auto& EX = m_edge_index[X];
208 0 : out << "index for equation " << X << std::endl;
209 0 : for (std::size_t i = 0; i < eq_X.predicate_variables().size(); i++)
210 : {
211 0 : auto& EXi = EX[i];
212 0 : for (const auto& ei: EXi)
213 : {
214 0 : out << " edge " << *ei.u << " --" << i << "--> " << *ei.v << std::endl;
215 : }
216 : }
217 : }
218 0 : return out.str();
219 0 : }
220 :
221 : // prints a belong set
222 0 : std::string print_belong_set(const stategraph_equation& eq, const std::set<std::size_t>& belongs) const
223 : {
224 0 : std::set<data::variable> v;
225 0 : for (std::size_t i: belongs)
226 : {
227 0 : v.insert(eq.parameters()[i]);
228 : }
229 0 : return core::detail::print_set(v);
230 0 : }
231 :
232 : // prints a subset of parameters of the equation corresponding to X
233 : // I is a set of indices of parameters of the equation corresponding to X
234 0 : std::string print_parameters(const core::identifier_string& X, const std::set<std::size_t>& I) const
235 : {
236 0 : auto const& eq_X = *find_equation(m_pbes, X);
237 0 : auto const& param = eq_X.parameters();
238 0 : std::ostringstream out;
239 0 : out << "{";
240 0 : for (auto i = I.begin(); i != I.end(); ++i)
241 : {
242 0 : if (i != I.begin())
243 : {
244 0 : out << ", ";
245 : }
246 0 : out << "(" << *i << ", " << param[*i] << ")";
247 : }
248 0 : out << "}";
249 0 : return out.str();
250 0 : }
251 :
252 : template <typename RulesPredicate>
253 2 : belongs_relation compute_belongs(const local_control_flow_graph& Vk, RulesPredicate rules)
254 : {
255 : using utilities::detail::contains;
256 :
257 2 : std::set<core::identifier_string> Nk; // Nk contains the names of the vertices in Vk
258 6 : for (const auto& v: Vk.vertices)
259 : {
260 4 : Nk.insert(v.name());
261 : }
262 :
263 2 : belongs_relation Bk;
264 2 : auto const& equations = m_pbes.equations();
265 10 : for (const stategraph_equation& eqn: equations)
266 : {
267 4 : auto const& X = eqn.variable().name();
268 4 : if (!contains(Nk, X))
269 : {
270 0 : continue;
271 : }
272 4 : Bk[X]; // force the creation of an empty set corresponding to X
273 4 : auto const& eq_X = *find_equation(m_pbes, X);
274 4 : auto const& dpX = eq_X.data_parameter_indices();
275 4 : std::set<std::size_t> belongs(dpX.begin(), dpX.end());
276 4 : mCRL2log(log::trace) << " initial belong set for equation " << X << " = " << print_belong_set(eq_X, belongs) << std::endl;
277 :
278 4 : auto const& predvars = eq_X.predicate_variables();
279 10 : for (std::size_t i = 0; i < predvars.size(); i++)
280 : {
281 6 : auto const& Ye = predvars[i];
282 12 : for (auto j = belongs.begin(); j != belongs.end(); )
283 : {
284 6 : std::size_t m = *j;
285 6 : if ((contains(Ye.used(), m) || contains(Ye.changed(), m)) && !rules(X, i))
286 : {
287 2 : mCRL2log(log::trace) << " remove (X, i, m) = (" << X << ", " << i << ", " << m << ") variable=" << eq_X.parameters()[m] << " from belongs " << std::endl;
288 2 : mCRL2log(log::trace) << " used = " << print_parameters(Ye.name(), Ye.used()) << " changed = " << print_parameters(Ye.name(), Ye.changed()) << std::endl;
289 2 : belongs.erase(j++);
290 : }
291 : else
292 : {
293 4 : ++j;
294 : }
295 : }
296 : }
297 4 : mCRL2log(log::trace) << " final belong set for equation " << X << " = " << print_belong_set(eq_X, belongs) << std::endl;
298 6 : for (std::size_t i: belongs)
299 : {
300 2 : Bk[X].insert(eq_X.parameters()[i]);
301 : }
302 : }
303 :
304 4 : return Bk;
305 2 : }
306 :
307 1 : void compute_belongs()
308 : {
309 1 : assert(m_local_control_flow_graphs.size() == m_connected_components_values.size());
310 1 : mCRL2log(log::debug) << "=== computing belongs relation ===" << std::endl;
311 3 : for (std::size_t k = 0; k < m_local_control_flow_graphs.size(); k++)
312 : {
313 2 : mCRL2log(log::debug) << "--- compute belongs for graph " << k << " ---" << std::endl;
314 2 : auto const& Vk = m_local_control_flow_graphs[k];
315 2 : belongs_relation Bk = compute_belongs(Vk, default_rules_predicate(Vk));
316 2 : m_belongs.push_back(Bk);
317 2 : }
318 1 : }
319 :
320 2 : std::string print_belongs(const belongs_relation& B) const
321 : {
322 2 : std::ostringstream out;
323 6 : for (const auto& b: B)
324 : {
325 4 : out << b.first << " -> " << core::detail::print_set(b.second) << std::endl;
326 : }
327 4 : return out.str();
328 2 : }
329 :
330 1 : void print_belongs() const
331 : {
332 1 : std::ostringstream out;
333 1 : out << "\n=== belongs relation ===\n";
334 3 : for (std::size_t k = 0; k < m_belongs.size(); k++)
335 : {
336 2 : out << "--- belongs relation for graph " << k << " ---" << std::endl;
337 2 : auto const& Bk = m_belongs[k];
338 2 : out << print_belongs(Bk);
339 : }
340 1 : mCRL2log(log::debug) << out.str() << std::endl;
341 1 : }
342 :
343 6 : std::set<data::variable> significant_variables(const local_control_flow_graph_vertex& u) const
344 : {
345 6 : const core::identifier_string& X = u.name();
346 6 : const pbes_equation& eq_X = *find_equation(m_pbes, X);
347 6 : pbes_expression phi = eq_X.formula();
348 6 : if (u.index() != data::undefined_index())
349 : {
350 2 : data::rewriter::substitution_type sigma;
351 2 : sigma[u.variable()] = u.value();
352 2 : pbes_system::simplify_data_rewriter<data::rewriter> pbesr(m_datar);
353 2 : phi = pbesr(phi, sigma);
354 2 : }
355 12 : return pbes_system::algorithms::significant_variables(phi);
356 6 : }
357 :
358 : // returns the index of variable d in the vector d_Y
359 6 : std::size_t find_parameter_index(const std::vector<data::variable>& d_Y, const data::variable& d) const
360 : {
361 6 : auto i = std::find(d_Y.begin(), d_Y.end(), d);
362 6 : if (i == d_Y.end())
363 : {
364 0 : throw mcrl2::runtime_error("find_parameter_index: variable not found!");
365 : }
366 6 : return i - d_Y.begin();
367 : }
368 :
369 1 : bool belongs_contains(const belongs_relation& B,
370 : const core::identifier_string& X,
371 : const data::variable& d
372 : ) const
373 : {
374 1 : auto i = B.find(X);
375 1 : if (i == B.end())
376 : {
377 0 : return false;
378 : }
379 1 : return utilities::detail::contains(i->second, d);
380 : }
381 :
382 : // returns the intersection of V with { d | (X, d) in B }
383 12 : std::set<data::variable> belongs_intersection(const std::set<data::variable>& V,
384 : const belongs_relation& B,
385 : const core::identifier_string& X
386 : )
387 : {
388 12 : auto i = B.find(X);
389 12 : if (i == B.end())
390 : {
391 0 : return std::set<data::variable>();
392 : }
393 12 : return utilities::detail::set_intersection(V, i->second);
394 : }
395 :
396 : template <typename Substitution>
397 6 : data::data_expression rewr(const data::data_expression& x, Substitution sigma)
398 : {
399 6 : return m_datar(x, sigma);
400 : }
401 :
402 6 : std::set<data::variable> marking_update(const local_control_flow_graph_vertex& u,
403 : std::size_t i,
404 : const data::variable& d,
405 : const data::data_expression_list& e,
406 : const stategraph_equation& eq_Y,
407 : const belongs_relation& B)
408 : {
409 6 : if (m_cache_marking_updates)
410 : {
411 : // check if the update is cached in u
412 0 : std::pair<std::size_t, data::variable> p(i, d);
413 0 : auto const& marking_update = u.marking_update();
414 0 : auto j = marking_update.find(p);
415 0 : if (j != marking_update.end())
416 : {
417 0 : m_marking_rewrite_count++;
418 0 : m_marking_rewrite_cached_count++;
419 0 : return j->second;
420 : }
421 0 : }
422 :
423 : // compute the value
424 6 : auto const& X = u.name();
425 6 : std::size_t l = find_parameter_index(eq_Y.parameters(), d);
426 6 : data::rewriter::substitution_type sigma;
427 6 : sigma[u.variable()] = u.value();
428 12 : auto W = FV(rewr(nth_element(e, l), sigma));
429 6 : std::set<data::variable> V = belongs_intersection(W, B, X);
430 6 : if (m_cache_marking_updates)
431 : {
432 0 : u.set_marking_update(i, d, V);
433 : }
434 6 : m_marking_rewrite_count++;
435 6 : return V;
436 6 : }
437 :
438 1 : void print_marking_statistics()
439 : {
440 1 : mCRL2log(log::verbose) << "--- marking statistics: " << m_marking_rewrite_count << " rewrite calls, from which " << m_marking_rewrite_cached_count << " were cached" << std::endl;
441 1 : }
442 :
443 : // updates u.marking
444 : // returns true if u.marking has changed
445 12 : bool update_marking_rule(const belongs_relation& B,
446 : const local_control_flow_graph_vertex& u,
447 : std::size_t i,
448 : const local_control_flow_graph_vertex& v,
449 : bool check_belongs // false corresponds with rule1, true corresponds with rule2
450 : )
451 : {
452 12 : std::size_t size = u.marking().size();
453 12 : auto const& X = u.name();
454 12 : auto const& eq_X = *find_equation(m_pbes, X);
455 12 : auto const& Y = v.name();
456 12 : auto const& eq_Y = *find_equation(m_pbes, Y);
457 12 : auto const& Ye = eq_X.predicate_variables()[i];
458 12 : auto const& e = Ye.parameters();
459 12 : auto m = v.marking(); // N.B. a copy must be made, to handle the case u == v properly
460 18 : for (const data::variable& d: m)
461 : {
462 6 : if (check_belongs && belongs_contains(B, Y, d))
463 : {
464 0 : continue;
465 : }
466 6 : auto const update = marking_update(u, i, d, e, eq_Y, B);
467 6 : u.extend_marking(update);
468 6 : }
469 24 : return u.marking().size() != size;
470 12 : }
471 :
472 : // returns true if there is a vertex u in V and an edge (u, i, v) in V, such that u.name() == X
473 4 : bool has_incoming_edge(const local_control_flow_graph& /* V */, const local_control_flow_graph_vertex& v, const core::identifier_string& X, std::size_t i) const
474 : {
475 : using utilities::detail::contains;
476 :
477 4 : auto const& incoming_edges = v.incoming_edges();
478 4 : for(const auto& e: incoming_edges)
479 : {
480 2 : auto const& u = *e.first;
481 2 : auto const& I = e.second;
482 2 : if (u.name() == X && contains(I, i))
483 : {
484 2 : return true;
485 : }
486 : }
487 2 : return false;
488 : }
489 :
490 1 : void compute_control_flow_marking()
491 : {
492 1 : mCRL2log(log::debug) << "=== computing control flow marking ===" << std::endl;
493 : using utilities::detail::pick_element;
494 :
495 1 : start_timer("marking initialization");
496 1 : std::size_t J = m_local_control_flow_graphs.size();
497 4 : for (std::size_t j = 0; j < J; j++)
498 : {
499 3 : auto const& Vj = m_local_control_flow_graphs[j];
500 3 : auto const& Bj = m_belongs[j];
501 9 : for (const auto& u : Vj.vertices)
502 : {
503 6 : auto const& X = u.name();
504 6 : u.set_marking(belongs_intersection(significant_variables(u), Bj, X));
505 : }
506 3 : mCRL2log(log::debug) << "--- initial control flow marking for graph " << j << "\n" << Vj.print_marking();
507 : }
508 1 : finish_timer("marking initialization");
509 :
510 1 : start_timer("marking computation");
511 1 : bool stable = false;
512 3 : while (!stable)
513 : {
514 2 : bool stableint = false;
515 4 : while (!stableint)
516 : {
517 2 : stableint = true;
518 8 : for (std::size_t j = 0; j < J; j++)
519 : {
520 6 : auto const& Vj = m_local_control_flow_graphs[j];
521 6 : auto const& Bj = m_belongs[j];
522 6 : std::set<const local_control_flow_graph_vertex*> todo;
523 18 : for (const auto& v: Vj.vertices)
524 : {
525 12 : todo.insert(&v);
526 : }
527 18 : while (!todo.empty())
528 : {
529 12 : auto const& v = *pick_element(todo);
530 :
531 12 : mCRL2log(log::trace) << " extend marking rule1: v = " << v << " marking(v) = " << core::detail::print_set(v.marking()) << std::endl;
532 :
533 12 : auto const& incoming_edges = v.incoming_edges();
534 22 : for (const auto& e: incoming_edges)
535 : {
536 10 : bool changed = false;
537 10 : auto const& u = *e.first;
538 10 : auto const& labels = e.second;
539 20 : for (std::size_t i: labels)
540 : {
541 : // consider edge (u, i, v)
542 10 : bool updated = update_marking_rule(Bj, u, i, v, false);
543 10 : changed = changed || updated;
544 : }
545 10 : if (changed)
546 : {
547 0 : mCRL2log(log::trace) << " marking(u)' = " << core::detail::print_set(u.marking()) << std::endl;
548 0 : todo.insert(&u);
549 0 : stableint = false;
550 : }
551 : }
552 : }
553 6 : }
554 : }
555 :
556 2 : bool stableext = false;
557 5 : while (!stableext)
558 : {
559 3 : stableext = true;
560 12 : for (std::size_t j = 0; j < J; j++)
561 : {
562 9 : auto const& Vj = m_local_control_flow_graphs[j];
563 9 : auto const& Bj = m_belongs[j];
564 27 : for (const auto &u : Vj.vertices)
565 : {
566 18 : auto const& X = u.name();
567 18 : if (u.marking().size() == Bj[X].size())
568 : {
569 17 : continue;
570 : }
571 1 : mCRL2log(log::trace) << " extend marking rule2: u = " << u << " marking(u) = " << core::detail::print_set(u.marking()) << std::endl;
572 :
573 1 : bool changed = false;
574 1 : auto const& eq_X = *find_equation(m_pbes, X); // slow
575 1 : auto const& predvars = eq_X.predicate_variables();
576 1 : auto const& outgoing_edges = u.outgoing_edges();
577 3 : for (const auto& e: outgoing_edges)
578 : {
579 2 : auto const& labels = e.second;
580 4 : for (std::size_t i: labels)
581 : {
582 2 : auto const& Ye = predvars[i];
583 2 : auto const& Y = Ye.name();
584 8 : for (std::size_t k = 0; k < J; k++)
585 : {
586 6 : if (j == k)
587 : {
588 2 : continue;
589 : }
590 4 : auto const& Vk = m_local_control_flow_graphs[k];
591 12 : for (auto vk = Vk.vertices.begin(); vk != Vk.vertices.end(); ++vk)
592 : {
593 8 : auto const& v = *vk;
594 8 : mCRL2log(log::trace) << " v = " << v << " marking(v) = " << core::detail::print_set(v.marking()) << std::endl;
595 8 : if (v.name() != Y)
596 : {
597 4 : continue;
598 : }
599 4 : if (has_incoming_edge(Vk, v, X, i))
600 : {
601 2 : bool updated = update_marking_rule(Bj, u, i, v, true);
602 2 : changed = changed || updated;
603 : }
604 : }
605 : }
606 : }
607 : }
608 1 : if (changed)
609 : {
610 1 : mCRL2log(log::trace) << " marking(u)' = " << core::detail::print_set(u.marking()) << std::endl;
611 1 : stableint = false;
612 1 : stableext = false;
613 : }
614 : }
615 : }
616 : }
617 2 : stable = stableint;
618 : }
619 1 : finish_timer("marking computation");
620 1 : }
621 :
622 : // add (X, i) to todo for each incoming edge u = (X, n, dX[n] = z) --i--> v
623 0 : void add_equation_labels(std::set<equation_label_pair>& todo, const local_control_flow_graph_vertex& v)
624 : {
625 0 : auto const& incoming_edges = v.incoming_edges();
626 0 : for (const auto& e: incoming_edges)
627 : {
628 0 : auto const& u = *e.first;
629 0 : auto const& X = u.name();
630 0 : auto const& labels = e.second;
631 0 : for (std::size_t i: labels)
632 : {
633 0 : todo.insert(equation_label_pair(X, i));
634 : }
635 : }
636 0 : }
637 :
638 : // a more comprehensible version
639 0 : void compute_control_flow_marking_using_edge_index()
640 : {
641 0 : mCRL2log(log::debug) << "=== computing control flow marking ===" << std::endl;
642 : using utilities::detail::pick_element;
643 :
644 0 : start_timer("marking initialization");
645 0 : std::size_t J = m_local_control_flow_graphs.size();
646 0 : std::set<equation_label_pair> todo;
647 0 : for (std::size_t j = 0; j < J; j++)
648 : {
649 0 : auto const& Vj = m_local_control_flow_graphs[j];
650 0 : auto const& Bj = m_belongs[j];
651 0 : for (const auto& v: Vj.vertices)
652 : {
653 0 : auto const& Y = v.name();
654 0 : v.set_marking(belongs_intersection(significant_variables(v), Bj, Y));
655 : // Insert those pairs (X,i) for which some vertex u = (X,n,dX[n]=z) --i--> v and v.marking() != {}
656 0 : if (v.marking().empty())
657 : {
658 0 : continue;
659 : }
660 0 : auto const& incoming_edges = v.incoming_edges();
661 0 : for (const auto& e: incoming_edges)
662 : {
663 0 : auto const& u = *e.first;
664 0 : auto const& X = u.name();
665 0 : auto const& labels = e.second;
666 0 : for (std::size_t i: labels)
667 : {
668 0 : todo.insert(equation_label_pair(X, i));
669 : }
670 : }
671 : }
672 0 : mCRL2log(log::debug) << "--- initial control flow marking for graph " << j << "\n" << Vj.print_marking();
673 : }
674 0 : finish_timer("marking initialization");
675 :
676 0 : start_timer("marking computation");
677 0 : while (!todo.empty())
678 : {
679 0 : auto const& Xi = pick_element(todo);
680 0 : auto const& X = Xi.X;
681 0 : std::size_t i = Xi.i;
682 :
683 0 : mCRL2log(log::trace) << " rule: considering equation " << X << std::endl;
684 0 : mCRL2log(log::trace) << " rule2: considering PVI nr. " << i << std::endl;
685 :
686 0 : auto& EX = m_edge_index[X];
687 0 : auto& EXi = EX[i];
688 0 : for (auto ei = EXi.begin(); ei != EXi.end(); ++ei)
689 : {
690 0 : const local_control_flow_graph_vertex& u = *ei->u;
691 0 : mCRL2log(log::trace) << " extend marking rule2: u = " << u << " marking(u) = " << core::detail::print_set(u.marking()) << std::endl;
692 0 : std::size_t j = ei->k;
693 0 : auto const& Bj = m_belongs[j];
694 0 : for (const auto& ej: EXi)
695 : {
696 0 : const local_control_flow_graph_vertex& u1 = *ej.u;
697 0 : const local_control_flow_graph_vertex& v1 = *ej.v;
698 0 : std::size_t k = ej.k;
699 0 : auto const& Bk = m_belongs[k];
700 0 : bool updated = update_marking_rule(Bk, u1, i, v1, false);
701 0 : if (updated)
702 : {
703 0 : add_equation_labels(todo, u1);
704 : }
705 0 : if (j != k )
706 : {
707 0 : updated = update_marking_rule(Bj, u, i, v1, true);
708 0 : if (updated)
709 : {
710 0 : add_equation_labels(todo, u);
711 : }
712 : }
713 : }
714 : }
715 0 : }
716 0 : finish_timer("marking computation");
717 0 : }
718 :
719 : // an efficient version that uses an edge index
720 0 : void compute_control_flow_marking_efficient()
721 : {
722 0 : mCRL2log(log::debug) << "=== computing control flow marking ===" << std::endl;
723 : using utilities::detail::pick_element;
724 :
725 0 : start_timer("marking initialization");
726 0 : std::size_t J = m_local_control_flow_graphs.size();
727 0 : for (std::size_t j = 0; j < J; j++)
728 : {
729 0 : auto const& Vj = m_local_control_flow_graphs[j];
730 0 : auto const& Bj = m_belongs[j];
731 0 : for (const auto& u: Vj.vertices)
732 : {
733 0 : auto const& X = u.name();
734 0 : u.set_marking(belongs_intersection(significant_variables(u), Bj, X));
735 : }
736 0 : mCRL2log(log::debug) << "--- initial control flow marking for graph " << j << "\n" << Vj.print_marking();
737 : }
738 0 : finish_timer("marking initialization");
739 :
740 0 : start_timer("marking computation");
741 0 : bool stable = false;
742 0 : while (!stable)
743 : {
744 0 : bool stableint = false;
745 0 : while (!stableint)
746 : {
747 0 : stableint = true;
748 0 : for (std::size_t j = 0; j < J; j++)
749 : {
750 0 : auto const& Vj = m_local_control_flow_graphs[j];
751 0 : auto const& Bj = m_belongs[j];
752 0 : std::set<const local_control_flow_graph_vertex*> todo;
753 0 : for (const auto& v: Vj.vertices)
754 : {
755 0 : todo.insert(&v);
756 : }
757 0 : while (!todo.empty())
758 : {
759 0 : auto const& v = *pick_element(todo);
760 :
761 0 : mCRL2log(log::trace) << " extend marking rule1: v = " << v << " marking(v) = " << core::detail::print_set(v.marking()) << std::endl;
762 :
763 0 : auto const& incoming_edges = v.incoming_edges();
764 0 : for (const auto& e: incoming_edges)
765 : {
766 0 : bool changed = false;
767 0 : auto const& u = *e.first;
768 0 : auto const& labels = e.second;
769 0 : for (std::size_t i: labels)
770 : {
771 : // consider edge (u, i, v)
772 0 : bool updated = update_marking_rule(Bj, u, i, v, false);
773 0 : changed = changed || updated;
774 : }
775 0 : if (changed)
776 : {
777 0 : mCRL2log(log::trace) << " marking(u)' = " << core::detail::print_set(u.marking()) << std::endl;
778 0 : todo.insert(&u);
779 0 : stableint = false;
780 : }
781 : }
782 : }
783 0 : }
784 : }
785 :
786 : // stableext := false
787 : // while not stableext do
788 : // stableext := true;
789 : // for X in bnd(E) do
790 : // for i <= npred(phi_X) do
791 : // let E := { ( u, i, v) in E1 union ... union EJ | exists n,z: u = (X,n,dX[n]=z) };
792 : // for (u,i,v) in E do
793 : // let j be such that u in Vj;
794 : // if (marking(u) = {d | (X,d) in Bj}) then continue;
795 : // for (u',i,v') in E do
796 : // let k be such that u' in Vk;
797 : // if (j == k) then continue;
798 : // m := marking(u);
799 : // marking(u) := UpdateMarkingRule2(Bj,u,i,v')
800 : // if not(marking(u) == m) then
801 : // stableint := false;
802 : // stableext := false;
803 : // stable := stableint /\ stableext;
804 0 : bool stableext = false;
805 0 : auto const& equations = m_pbes.equations();
806 0 : while (!stableext)
807 : {
808 0 : stableext = true;
809 0 : for (const auto& eq_X: equations)
810 : {
811 0 : auto const& X = eq_X.variable().name();
812 0 : auto& EX = m_edge_index[X];
813 0 : for (std::size_t i = 0; i < eq_X.predicate_variables().size(); i++)
814 : {
815 0 : auto& EXi = EX[i];
816 0 : for (auto ei = EXi.begin(); ei != EXi.end(); ++ei)
817 : {
818 0 : const local_control_flow_graph_vertex& u = *ei->u;
819 : // const local_control_flow_graph_vertex& v = *ei->v;
820 0 : std::size_t j = ei->k;
821 0 : auto const& Bj = m_belongs[j];
822 0 : if (u.marking().size() == Bj[X].size())
823 : {
824 0 : continue;
825 : }
826 0 : for (const auto& ej: EXi)
827 : {
828 : // const local_control_flow_graph_vertex& u1 = *ej->u;
829 0 : const local_control_flow_graph_vertex& v1 = *ej.v;
830 0 : std::size_t k = ej.k;
831 0 : if (j == k)
832 : {
833 0 : continue;
834 : }
835 0 : bool updated = update_marking_rule(Bj, u, i, v1, true);
836 0 : if (updated)
837 : {
838 0 : stableint = false;
839 0 : stableext = false;
840 : }
841 : }
842 : }
843 : }
844 : }
845 : }
846 0 : stable = stableint;
847 : }
848 0 : finish_timer("marking computation");
849 0 : }
850 :
851 1 : void print_control_flow_marking() const
852 : {
853 1 : std::size_t K = m_local_control_flow_graphs.size();
854 4 : for (std::size_t k = 0; k < K; k++)
855 : {
856 3 : const local_control_flow_graph& Gk = m_local_control_flow_graphs[k];
857 3 : mCRL2log(log::debug) << "--- computed control flow marking for graph " << k << "\n" << Gk.print_marking() << std::endl;
858 : }
859 1 : }
860 :
861 4 : void remove_belongs(std::set<data::variable>& B_X,
862 : const core::identifier_string& X,
863 : const belongs_relation& Bk,
864 : std::size_t k)
865 : {
866 12 : for (const auto& i: Bk)
867 : {
868 8 : if (i.first != X)
869 : {
870 4 : continue;
871 : }
872 4 : auto const& V = i.second;
873 6 : for (const data::variable& v: V)
874 : {
875 2 : auto j = B_X.find(v);
876 2 : if (j != B_X.end())
877 : {
878 2 : mCRL2log(log::debug) << "removing belongs variable " << *j << " in B[" << X << "] , since it already appears in belongs relation " << k << std::endl;
879 2 : B_X.erase(*j);
880 : }
881 : }
882 : }
883 4 : }
884 :
885 1 : void compute_extra_local_control_flow_graph()
886 : {
887 1 : mCRL2log(log::trace) << "--- computing extra local control flow graph" << std::endl;
888 :
889 1 : local_control_flow_graph V;
890 1 : belongs_relation B;
891 :
892 1 : auto const& equations = m_pbes.equations();
893 3 : for (const auto& eq_X: equations)
894 : {
895 2 : auto const& X = eq_X.variable().name();
896 2 : auto const& u = V.insert_vertex(local_control_flow_graph_vertex(X, data::undefined_data_expression()));
897 :
898 2 : auto const& d_X = eq_X.parameters();
899 2 : auto& B_X = B[X]; // N.B. This forces the creation of an empty belong set B[X].
900 2 : auto const& I = eq_X.data_parameter_indices();
901 4 : for (std::size_t i : I)
902 : {
903 2 : B_X.insert(d_X[i]);
904 : }
905 2 : mCRL2log(log::trace) << "initial belongs relation B[" << X << "] = " << core::detail::print_set(B_X) << std::endl;
906 :
907 6 : for (std::size_t k = 0; k < m_belongs.size(); k++)
908 : {
909 4 : auto const& Bk = m_belongs[k];
910 4 : remove_belongs(B_X, X, Bk, k);
911 : }
912 :
913 2 : auto const& predvars = eq_X.predicate_variables();
914 5 : for (std::size_t i = 0; i < predvars.size(); i++)
915 : {
916 3 : auto const& Ye = predvars[i];
917 :
918 3 : bool add_edge = false;
919 :
920 : //if X != Y || exists k: d_X[k] \in B && (used(X, j, k) || changed(X, j, k)) then
921 : // implemented by checking for non-empty intersection
922 3 : if(X != Ye.name())
923 : {
924 1 : add_edge = true;
925 : }
926 : else
927 : {
928 2 : std::set<data::variable> used_or_changed;
929 5 : for (std::size_t j: Ye.changed())
930 : {
931 3 : used_or_changed.insert(d_X[j]);
932 : }
933 5 : for (std::size_t j: Ye.used())
934 : {
935 3 : used_or_changed.insert(d_X[j]);
936 : }
937 :
938 2 : std::set<data::variable>::const_iterator bi = B_X.begin();
939 2 : std::set<data::variable>::const_iterator ui = used_or_changed.begin();
940 2 : while (bi != B_X.end() && ui != used_or_changed.end())
941 : {
942 0 : if (*ui < *bi)
943 : {
944 0 : ++ui;
945 : }
946 0 : else if (*bi < *ui)
947 : {
948 0 : ++bi;
949 : }
950 : else
951 : {
952 0 : add_edge = true;
953 0 : break;
954 : }
955 : }
956 2 : }
957 :
958 3 : if(add_edge)
959 : {
960 1 : auto const& v = V.insert_vertex(local_control_flow_graph_vertex(Ye.name(), data::undefined_data_expression()));
961 1 : V.insert_edge(u, i, v);
962 : }
963 : }
964 : }
965 1 : m_local_control_flow_graphs.push_back(V);
966 1 : m_local_control_flow_graphs.back().compute_index();
967 1 : m_belongs.push_back(B);
968 1 : mCRL2log(log::debug) << "--- extra local control flow graph\n" << m_local_control_flow_graphs.back() << std::endl;
969 1 : mCRL2log(log::debug) << "--- belongs relation for extra graph\n" << print_belongs(B);
970 1 : }
971 :
972 2 : void compute_local_control_flow_graph(const std::set<local_control_flow_graph_vertex>& U, const std::map<core::identifier_string, std::size_t>& C)
973 : {
974 : using utilities::detail::pick_element;
975 :
976 2 : mCRL2log(log::debug) << "--- compute_local_control_flow_graph for vertices " << core::detail::print_set(U) << std::endl;
977 2 : local_control_flow_graph V;
978 2 : std::set<const local_control_flow_graph_vertex*> todo;
979 :
980 5 : for (const local_control_flow_graph_vertex& u: U)
981 : {
982 3 : auto k = V.insert(u);
983 3 : todo.insert(&(*k.first));
984 : }
985 :
986 6 : while (!todo.empty())
987 : {
988 : // u = (X, k, d = e)
989 4 : auto const& u = *pick_element(todo);
990 4 : auto const& X = u.name();
991 4 : const data::variable& d = u.variable();
992 4 : const data::data_expression& e = u.value();
993 4 : mCRL2log(log::trace) << "choose todo element (X, k, d=e) = " << u << std::endl;
994 4 : std::size_t k = u.index();
995 4 : auto const& eq_X = *find_equation(m_pbes, X);
996 4 : auto const& predvars = eq_X.predicate_variables();
997 :
998 10 : for (auto i = predvars.begin(); i != predvars.end(); ++i)
999 : {
1000 6 : std::size_t edge_label = i - predvars.begin();
1001 6 : auto const& Y = i->name();
1002 6 : auto q = C.find(Y);
1003 :
1004 6 : if (d == data::undefined_variable())
1005 : {
1006 : // case 1: (X, ?, ?=?) -> (Y, k', d'=e')
1007 3 : mCRL2log(log::trace) << "case 1" << std::endl;
1008 3 : if (q != C.end()) // (Y, k1) in C
1009 : {
1010 1 : std::size_t k1 = q->second;
1011 1 : auto e1 = i->target(k1);
1012 1 : if (e1 != data::undefined_data_expression())
1013 : {
1014 : // target(X, i, k') = e'
1015 1 : mCRL2log(log::trace) << "case 1: (X, e) -> (Y, d', e') ; target(X, i, k') = e' ; k' = " << print_index(k1) << std::endl;
1016 1 : V.insert_edge(todo, m_pbes, u, Y, k1, e1, edge_label);
1017 : }
1018 1 : }
1019 : // case 2: (X, ?, ?=?) -> (Y, ?, ?=?)
1020 : else
1021 : {
1022 2 : if (X != Y)
1023 : {
1024 0 : mCRL2log(log::trace) << "case 2: (X, ?) -> (Y, ?)" << std::endl;
1025 0 : V.insert_edge(todo, m_pbes, u, Y, data::undefined_index(), data::undefined_data_expression(), edge_label);
1026 : }
1027 : }
1028 : }
1029 : else
1030 : {
1031 : // case 3: (X, d, e) -> (Y, d', e')
1032 3 : if (q != C.end()) // (Y, k') in C
1033 : {
1034 2 : std::size_t k1 = q->second;
1035 2 : if (is_mapped_to(i->source(), k, e))
1036 : {
1037 : // source(X, i, k) = e && target(X, i, k') = e'
1038 2 : auto e1 = i->target(k1);
1039 2 : mCRL2log(log::trace) << "case 3a: (X, d, e) -> (Y, d', e') ; source(X, i, k) = e && target(X, i, k') = e' ; k' = " << print_index(k1) << std::endl;
1040 2 : if (e1 != data::undefined_data_expression())
1041 : {
1042 2 : V.insert_edge(todo, m_pbes, u, Y, k1, e1, edge_label);
1043 : }
1044 2 : }
1045 0 : else if (Y != X && is_undefined(i->source(), k))
1046 : {
1047 : // Y != X && undefined(source(X, i, k)) && target(X, i, k') = e'
1048 0 : auto e1 = i->target(k1);
1049 0 : if (e1 != data::undefined_data_expression())
1050 : {
1051 0 : mCRL2log(log::trace) << "case 3b: (X, d, e) -> (Y, d', e') ; Y != X && undefined(source(X, i, k)) && target(X, i, k') = e' ; k' = " << print_index(k1) << std::endl;
1052 0 : V.insert_edge(todo, m_pbes, u, Y, k1, e1, edge_label);
1053 : }
1054 :
1055 : // Y != X && undefined(source(X, i, k)) && copy(X, i, k) = k'
1056 0 : if (i->copy(k) == k1)
1057 : {
1058 0 : mCRL2log(log::trace) << "case 3c: (X, d, e) -> (Y, d', e') ; Y != X && undefined(source(X, i, k)) && copy(X, i, k) = k' ; k' = " << print_index(k1) << std::endl;
1059 0 : V.insert_edge(todo, m_pbes, u, Y, k1, e, edge_label);
1060 : }
1061 0 : }
1062 : }
1063 : // case 4: (X, d, e) -> (Y, ?)
1064 : else
1065 : {
1066 1 : auto e1 = i->source(k);
1067 1 : if (e1 == e || e1 == data::undefined_data_expression())
1068 : {
1069 1 : std::size_t k1 = data::undefined_index();
1070 1 : mCRL2log(log::trace) << "case 4: (X, d, e) -> (Y, ?)" << std::endl;
1071 1 : V.insert_edge(todo, m_pbes, u, Y, k1, data::undefined_data_expression(), edge_label);
1072 : }
1073 1 : }
1074 : }
1075 : }
1076 : }
1077 : // V.self_check();
1078 2 : m_local_control_flow_graphs.push_back(V);
1079 2 : m_local_control_flow_graphs.back().compute_index();
1080 2 : }
1081 :
1082 : void compute_local_control_flow_graph(const local_control_flow_graph_vertex& u, const std::map<core::identifier_string, std::size_t>& C)
1083 : {
1084 : std::set<local_control_flow_graph_vertex> U;
1085 : U.insert(u);
1086 : compute_local_control_flow_graph(U, C);
1087 : }
1088 :
1089 : // Computes a local control flow graph that corresponds to the given component in m_GCFP_graph.
1090 2 : void compute_local_control_flow_graph(const std::set<std::size_t>& component, const std::set<data::data_expression>& component_values)
1091 : {
1092 2 : mCRL2log(log::debug) << "Compute local control flow graphs for component " << print_connected_component(component) << std::endl;
1093 :
1094 : // preprocessing
1095 2 : std::map<core::identifier_string, std::size_t> C;
1096 4 : for (std::size_t p: component)
1097 : {
1098 2 : const GCFP_vertex& w = m_GCFP_graph.vertex(p);
1099 2 : C[w.name()] = w.index();
1100 : }
1101 :
1102 2 : std::set<local_control_flow_graph_vertex> U;
1103 4 : for (std::size_t p: component)
1104 : {
1105 2 : const GCFP_vertex& u = m_GCFP_graph.vertex(p);
1106 4 : for (const auto& value: component_values)
1107 : {
1108 2 : U.insert(local_control_flow_graph_vertex(u.name(), u.index(), u.variable(), value));
1109 : }
1110 : }
1111 :
1112 : // add a node (Xinit, ?, ?=?)
1113 2 : const core::identifier_string& Xinit = m_pbes.initial_state().name();
1114 2 : if (C.find(Xinit) == C.end())
1115 : {
1116 1 : U.insert(local_control_flow_graph_vertex(Xinit, data::undefined_index(), data::undefined_variable(), data::undefined_data_expression()));
1117 : }
1118 :
1119 2 : compute_local_control_flow_graph(U, C);
1120 2 : }
1121 :
1122 1 : void print_local_control_flow_graphs() const
1123 : {
1124 3 : for (auto i = m_local_control_flow_graphs.begin(); i != m_local_control_flow_graphs.end(); ++i)
1125 : {
1126 2 : mCRL2log(log::debug) << "--- computed local control flow graph " << (i - m_local_control_flow_graphs.begin()) << "\n" << *i << std::endl;
1127 : }
1128 1 : }
1129 :
1130 1 : void compute_local_control_flow_graphs()
1131 : {
1132 3 : for (std::size_t i = 0; i < m_connected_components.size(); i++)
1133 : {
1134 2 : compute_local_control_flow_graph(m_connected_components[i], m_connected_components_values[i]);
1135 : }
1136 1 : }
1137 :
1138 : public:
1139 1 : stategraph_local_algorithm(const pbes& p, const pbesstategraph_options& options)
1140 1 : : stategraph_algorithm(p, options),
1141 1 : m_cache_marking_updates(options.cache_marking_updates),
1142 1 : m_marking_rewrite_count(0),
1143 1 : m_marking_rewrite_cached_count(0)
1144 :
1145 1 : { }
1146 :
1147 : /// \brief Computes the control flow graph
1148 1 : void run() override
1149 : {
1150 1 : super::run();
1151 :
1152 1 : start_timer("compute_local_control_flow_graphs");
1153 1 : compute_local_control_flow_graphs();
1154 1 : finish_timer("compute_local_control_flow_graphs");
1155 1 : print_local_control_flow_graphs();
1156 :
1157 1 : start_timer("compute_belongs");
1158 1 : compute_belongs();
1159 1 : finish_timer("compute_belongs");
1160 1 : print_belongs();
1161 :
1162 1 : start_timer("compute_extra_local_control_flow_graph");
1163 1 : compute_extra_local_control_flow_graph();
1164 1 : finish_timer("compute_extra_local_control_flow_graph");
1165 :
1166 1 : start_timer("compute_control_flow_marking");
1167 1 : switch (m_options.marking_algorithm)
1168 : {
1169 1 : case 0: {
1170 1 : compute_control_flow_marking();
1171 1 : break;
1172 : }
1173 0 : case 1: {
1174 0 : compute_edge_index();
1175 0 : mCRL2log(log::trace) << print_edge_index() << std::endl;
1176 0 : compute_control_flow_marking_using_edge_index();
1177 0 : break;
1178 : }
1179 0 : case 2: {
1180 0 : compute_edge_index();
1181 0 : mCRL2log(log::trace) << print_edge_index() << std::endl;
1182 0 : compute_control_flow_marking_efficient();
1183 0 : break;
1184 : }
1185 0 : default: {
1186 0 : throw mcrl2::runtime_error("unknown value of marking_algorithm");
1187 : }
1188 : }
1189 1 : finish_timer("compute_control_flow_marking");
1190 1 : print_control_flow_marking();
1191 :
1192 1 : print_marking_statistics();
1193 1 : }
1194 :
1195 :
1196 :
1197 : const std::vector<belongs_relation>& belongs() const
1198 : {
1199 : return m_belongs;
1200 : }
1201 : };
1202 :
1203 : } // namespace detail
1204 :
1205 : } // namespace pbes_system
1206 :
1207 : } // namespace mcrl2
1208 :
1209 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_LOCAL_ALGORITHM_H
|
