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_algorithm.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_ALGORITHM_H
13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_ALGORITHM_H
14 :
15 : #include "mcrl2/pbes/detail/stategraph_graph.h"
16 : #include "mcrl2/pbes/tools/pbesstategraph_options.h"
17 : #include "mcrl2/utilities/sequence.h"
18 :
19 : namespace mcrl2 {
20 :
21 : namespace pbes_system {
22 :
23 : namespace detail {
24 :
25 : inline
26 0 : std::string print_index(std::size_t index)
27 : {
28 0 : std::ostringstream out;
29 0 : if (index == data::undefined_index())
30 : {
31 0 : out << "undefined";
32 : }
33 : else
34 : {
35 0 : out << index;
36 : }
37 0 : return out.str();
38 0 : }
39 :
40 : /// \brief Algorithm class for the computation of the local and global control flow graphs
41 : class stategraph_algorithm
42 : {
43 : public:
44 : // simplify and rewrite the guards of the pbes p
45 27 : void simplify(stategraph_pbes& p) const
46 : {
47 89 : for (stategraph_equation& equation: p.equations())
48 : {
49 170 : for (predicate_variable& predvar: equation.predicate_variables())
50 : {
51 108 : predvar.simplify_guard();
52 : }
53 : }
54 27 : }
55 :
56 : protected:
57 : // the pbes that is considered
58 : stategraph_pbes m_pbes;
59 :
60 : // a data rewriter
61 : data::rewriter m_datar;
62 :
63 : // determines how local control flow parameters are computed
64 : //
65 : // Keuze uit twee alternatieven voor de berekening van lokale CFPs.
66 : // <default>
67 : // * Een parameter d^X[n] is een LCFP indien voor alle i waarvoor geldt pred(phi_X,i) = X, danwel:
68 : // a. source(X,i,n) and target(X,i,n) zijn beide defined, of
69 : // b. copy(X,i,n) is defined en gelijk aan n.
70 : //
71 : // <alternative>
72 : // * Een parameter d^X[n] is een LCFP indien voor alle i waarvoor geldt pred(phi_X,i) = X, danwel:
73 : // a. copy(X,i,n) is undefined en source(X,i,n) and target(X,i,n) zijn beide defined, of
74 : // b. copy(X,i,n) is defined (en gelijk aan n) en source(X,i,n) en target(X,i,n) zijn beide undefined.
75 : //
76 : // De tweede definieert in feite een exclusive or, terwijl de eerste een standaard or is.
77 : bool m_use_alternative_lcfp_criterion;
78 :
79 : // determines how global control flow parameters are related
80 : //
81 : // Keuze uit twee alternatieven voor het relateren van CFPs.
82 : // <default>
83 : // * Parameters d^X[n] and d^Y[m] zijn gerelateerd als danwel:
84 : // a. er is een i z.d.d. copy(X, i, n) = m, of
85 : // b. er is een i z.d.d. copy(Y, i, m) = n
86 : //
87 : // <alternative>
88 : // * Parameters d^X[n] and d^Y[m] zijn gerelateerd als danwel:
89 : // a. er is een i z.d.d. copy(X, i, n) = m, en target(X, i, m) is ongedefinieerd, of
90 : // b. er is een i z.d.d. copy(Y, i, m) = n en target(Y, i, n) is ongedefinieerd.
91 : // Hier zit het verschil er dus in dat we, in het tweede geval, parameters alleen relateren als er een copy is
92 : // van de een naar de ander EN de target in dat geval ongedefinieerd is.
93 : bool m_use_alternative_gcfp_relation;
94 :
95 : // determines how global control flow parameters are selected
96 : //
97 : // Keuze voor de selectie van globale CFPs (of globale consistentie eisen).
98 : // <default>
99 : // * Een set van CFPs is consistent als voor elke d^X[n], en voor alle Y in bnd(E)\{X} (dus in alle andere vergelijkingen), voor alle i waarvoor geldt pred(phi_Y, i) = X, danwel:
100 : // a. target(Y, i, n) is gedefinieerd, of
101 : // b. copy(Y, i, m) = n voor een of andere globale CFP d^Y[m]
102 : // Deze eis is in principe voldoende om globale CFPs te identificeren. Als we echter een strikte scheiding tussen control flow parameters en data parameters willen bewerkstelligen, dan moet hier optioneel de volgende eis aan toegevoegd worden:
103 : //
104 : // <alternative>
105 : // * Een set van CFPs is consistent als de voorgaande eisen gelden, en bovendien voor elke d^X[n] geldt dat voor alle i waarvoor pred(phi_X, i) = Y != X, als d^X[n] affects data(phi_X, i)[m], dan is d^Y[m] een globale control flow parameter.
106 : // Waar de eerste gemarkeerd is als "detect conflicts for parameters of Y in equations of the form X(d) = ... Y(e)"
107 : // en de tweede als "detect conflicts for parameters of X in equations of the form X(d) = ... Y(e)".
108 : bool m_use_alternative_gcfp_consistency;
109 :
110 : // TODO: remove the three booleans above, since they are also present in m_options
111 : pbesstategraph_options m_options;
112 :
113 : // the local control flow parameters
114 : std::map<core::identifier_string, std::vector<bool> > m_is_LCFP;
115 :
116 : // the global control flow parameters
117 : std::map<core::identifier_string, std::vector<bool> > m_is_GCFP;
118 :
119 : // the vertices of the control flow graph
120 : GCFP_graph m_GCFP_graph;
121 :
122 : // the connected components in the control flow graph; a component contains the indices of vertices in the graph m_GCFP_graph
123 : std::vector<std::set<std::size_t> > m_connected_components;
124 :
125 : // the possible values of the connected components in the control flow graph
126 : std::vector<std::set<data::data_expression> > m_connected_components_values;
127 :
128 : // the local control flow graph(s)
129 : std::vector<local_control_flow_graph> m_local_control_flow_graphs;
130 :
131 : // for readability
132 6 : std::set<data::variable> FV(const data::data_expression& x) const
133 : {
134 6 : return data::find_free_variables(x);
135 : }
136 :
137 142 : void start_timer(const std::string& msg) const
138 : {
139 142 : if (m_options.timing_enabled())
140 : {
141 0 : m_options.timer->start(msg);
142 : }
143 142 : }
144 :
145 142 : void finish_timer(const std::string& msg) const
146 : {
147 142 : if (m_options.timing_enabled())
148 : {
149 0 : m_options.timer->finish(msg);
150 : }
151 142 : }
152 :
153 : public:
154 27 : void compute_control_flow_parameters()
155 : {
156 27 : start_timer("compute_local_control_flow_parameters");
157 27 : compute_local_control_flow_parameters();
158 27 : finish_timer("compute_local_control_flow_parameters");
159 :
160 27 : start_timer("compute_global_control_flow_parameters");
161 27 : compute_global_control_flow_parameters();
162 27 : finish_timer("compute_global_control_flow_parameters");
163 :
164 27 : start_timer("compute_related_GCFP_parameters");
165 27 : compute_related_GCFP_parameters();
166 27 : finish_timer("compute_related_GCFP_parameters");
167 :
168 27 : start_timer("compute_connected_components");
169 27 : compute_connected_components();
170 27 : finish_timer("compute_connected_components");
171 27 : }
172 :
173 : template <typename T>
174 0 : std::string print_control_flow_parameters(const std::string& msg, T& is_CFP)
175 : {
176 0 : std::ostringstream out;
177 0 : out << msg << std::endl;
178 0 : for (const stategraph_equation& equation: m_pbes.equations())
179 : {
180 0 : auto const& X = equation.variable().name();
181 0 : auto const& d_X = equation.parameters();
182 0 : const std::vector<bool>& cf = is_CFP[X];
183 0 : for (std::size_t i = 0; i < cf.size(); ++i)
184 : {
185 0 : if (cf[i])
186 : {
187 0 : out << "(" << X << ", " << i << ", " << d_X[i] << ")" << std::endl;
188 : }
189 : }
190 : }
191 0 : return out.str();
192 0 : }
193 :
194 0 : std::string print_LCFP()
195 : {
196 0 : return print_control_flow_parameters("--- computed LCFP parameters (before removing components) ---", m_is_LCFP);
197 : }
198 :
199 0 : std::string print_GCFP()
200 : {
201 0 : return print_control_flow_parameters("--- computed GCFP parameters ---", m_is_GCFP);
202 : }
203 :
204 : // returns true if m is not a key in the map
205 : template <typename Map>
206 592 : bool is_undefined(const Map& m, const typename Map::key_type& key) const
207 : {
208 592 : return m.find(key) == m.end();
209 : }
210 :
211 : // returns true if the mapping m maps key to value
212 : template <typename Map>
213 90 : bool is_mapped_to(const Map& m, const typename Map::key_type& key, const typename Map::mapped_type& value) const
214 : {
215 90 : auto i = m.find(key);
216 90 : return i != m.end() && i->second == value;
217 : }
218 :
219 243 : bool maps_to_and_is_GFCP(const std::map<std::size_t, std::size_t>& m, std::size_t value, const core::identifier_string& X)
220 : {
221 758 : for (const auto& i: m)
222 : {
223 541 : if (i.second == value && m_is_GCFP[X][i.first])
224 : {
225 26 : return true;
226 : }
227 : }
228 217 : return false;
229 : }
230 :
231 27 : void compute_local_control_flow_parameters()
232 : {
233 27 : mCRL2log(log::debug) << "=== computing local control flow parameters ===" << std::endl;
234 :
235 27 : auto const& equations = m_pbes.equations();
236 :
237 : // initialize all control flow parameters to true
238 89 : for (const stategraph_equation& equation: equations)
239 : {
240 62 : auto const& X = equation.variable().name();
241 62 : auto const& d_X = equation.parameters();
242 62 : m_is_LCFP[X] = std::vector<bool>(d_X.size(), true);
243 : }
244 :
245 89 : for (const stategraph_equation& equation: equations)
246 : {
247 62 : auto const& X = equation.variable().name();
248 62 : auto const& d_X = equation.parameters();
249 62 : auto const& predvars = equation.predicate_variables();
250 170 : for (const predicate_variable& Ye: predvars)
251 : {
252 108 : if (Ye.name() == X)
253 : {
254 164 : for (std::size_t n = 0; n < d_X.size(); n++)
255 : {
256 127 : if (m_use_alternative_lcfp_criterion)
257 : {
258 : // Een parameter d^X[n] is een LCFP indien voor alle i waarvoor geldt pred(phi_X,i) = X, danwel:
259 : // 1. copy(X,i,n) is undefined en source(X,i,n) and target(X,i,n) zijn beide defined, of
260 : // 2. copy(X,i,n) is defined en source(X,i,n) en target(X,i,n) zijn beide undefined.
261 0 : if (Ye.copy().find(n) == Ye.copy().end())
262 : {
263 : // copy(X,i,n) is undefined
264 0 : if (is_undefined(Ye.source(), n) || is_undefined(Ye.target(), n))
265 : {
266 0 : mCRL2log(log::debug) << "parameter " << print_cfp(X, n) << " is not an LCFP because of predicate variable " << Ye << " in equation " << X << " (copy and source/target undefined)" << std::endl;
267 0 : m_is_LCFP[X][n] = false;
268 : }
269 : }
270 : else
271 : {
272 : // copy(X,i,n) is defined
273 0 : if (!is_undefined(Ye.source(), n) || !is_undefined(Ye.target(), n))
274 : {
275 0 : mCRL2log(log::debug) << "parameter " << print_cfp(X, n) << " is not an LCFP because of predicate variable " << Ye << " in equation " << X << " (copy defined and source/target defined)" << std::endl;
276 0 : m_is_LCFP[X][n] = false;
277 : }
278 : }
279 : }
280 : else
281 : {
282 127 : if ((is_undefined(Ye.source(), n) || is_undefined(Ye.target(), n)) && !is_mapped_to(Ye.copy(), n, n))
283 : {
284 43 : mCRL2log(log::debug) << "parameter " << print_cfp(X, n) << " is not an LCFP due to " << Ye << "(source and target undefined, and no copy to self)" << std::endl;
285 43 : m_is_LCFP[X][n] = false;
286 : }
287 : }
288 : }
289 : }
290 : }
291 : }
292 27 : mCRL2log(log::debug) << print_LCFP();
293 27 : }
294 :
295 : // Computes the global control flow parameters. The result is stored in m_is_GCFP.
296 27 : void compute_global_control_flow_parameters()
297 : {
298 27 : mCRL2log(log::debug) << "=== computing global control flow parameters ===" << std::endl;
299 :
300 27 : m_is_GCFP = m_is_LCFP;
301 :
302 27 : auto const& equations = m_pbes.equations();
303 :
304 : bool changed;
305 49 : do
306 : {
307 49 : changed = false;
308 :
309 : // Detect conflicts for parameters of Y in equations of the form X(d) = ... Y(e)
310 164 : for (const stategraph_equation& equation: equations)
311 : {
312 115 : auto const& X = equation.variable().name();
313 115 : auto const& predvars = equation.predicate_variables();
314 316 : for (const predicate_variable& Ye: predvars)
315 : {
316 201 : auto const& Y = Ye.name();
317 201 : if (Y != X)
318 : {
319 134 : auto const& eq_Y = *find_equation(m_pbes, Y);
320 134 : auto const& d_Y = eq_Y.parameters();
321 506 : for (std::size_t n = 0; n < d_Y.size(); n++)
322 : {
323 372 : if (is_undefined(Ye.target(), n) && (!maps_to_and_is_GFCP(Ye.copy(), n, X)))
324 : {
325 217 : if (m_is_GCFP[Y][n])
326 : {
327 64 : m_is_GCFP[Y][n] = false;
328 64 : changed = true;
329 64 : mCRL2log(log::debug) << "parameter " << print_cfp(Y, n) << " is not a GCFP because of predicate variable " << Ye << " in equation " << X << std::endl;
330 : }
331 : }
332 : }
333 : }
334 : }
335 : }
336 :
337 : // Detect conflicts for parameters of X in equations of the form X(d) = ... Y(e)
338 49 : if (m_use_alternative_gcfp_consistency)
339 : {
340 0 : for (const stategraph_equation& equation: equations)
341 : {
342 0 : auto const& X = equation.variable().name();
343 0 : auto const& predvars = equation.predicate_variables();
344 0 : auto const& d_X = equation.parameters();
345 0 : std::size_t M = d_X.size();
346 :
347 0 : for (const predicate_variable& Ye : predvars)
348 : {
349 0 : auto const& Y = Ye.name();
350 0 : if (Y == X)
351 : {
352 0 : continue;
353 : }
354 0 : auto const& e = Ye.parameters();
355 0 : std::size_t n = 0;
356 0 : for (auto ei = e.begin(); ei != e.end(); ++ei, ++n)
357 : {
358 0 : std::set<data::variable> V = FV(*ei);
359 0 : for (std::size_t m = 0; m < M; m++)
360 : {
361 0 : if (m_is_GCFP[X][m] && !m_is_GCFP[Y][n] && (V.find(d_X[m]) != V.end()))
362 : {
363 0 : m_is_GCFP[X][m] = false;
364 0 : changed = true;
365 0 : mCRL2log(log::debug) << "parameter " << print_cfp(X, m) << " is not a GCFP because of predicate variable " << Ye << " in equation " << X << std::endl;
366 : }
367 : }
368 0 : }
369 : }
370 : }
371 : }
372 : }
373 : while (changed);
374 :
375 27 : mCRL2log(log::debug) << print_GCFP();
376 27 : }
377 :
378 : bool is_LCFP_parameter(const core::identifier_string& X, std::size_t i) const
379 : {
380 : auto j = m_is_LCFP.find(X);
381 : assert(j != m_is_LCFP.end());
382 : const std::vector<bool>& cf = j->second;
383 : assert(i < cf.size());
384 : return cf[i];
385 : }
386 :
387 409 : bool is_GCFP_parameter(const core::identifier_string& X, std::size_t i) const
388 : {
389 409 : auto j = m_is_GCFP.find(X);
390 409 : assert(j != m_is_GCFP.end());
391 409 : const std::vector<bool>& cf = j->second;
392 409 : assert(i < cf.size());
393 818 : return cf[i];
394 : }
395 :
396 0 : bool is_global_control_flow_parameter(const core::identifier_string& X, std::size_t i) const
397 : {
398 : using utilities::detail::contains;
399 0 : auto const& eq_X = *find_equation(m_pbes, X);
400 0 : const std::vector<std::size_t>& I = eq_X.control_flow_parameter_indices();
401 0 : return contains(I, i);
402 : }
403 :
404 : // relate (X, n) and (Y, m) in the dependency graph
405 : // \pre: the equation of X has a lower rank than the equation of Y
406 48 : void relate_GCFP_vertices(const core::identifier_string& X, std::size_t n, const core::identifier_string& Y, std::size_t m)
407 : {
408 48 : GCFP_vertex& u = m_GCFP_graph.find_vertex(X, n);
409 48 : GCFP_vertex& v = m_GCFP_graph.find_vertex(Y, m);
410 48 : u.neighbors().insert(&v);
411 48 : v.neighbors().insert(&u);
412 48 : }
413 :
414 0 : std::string print_cfp(const core::identifier_string& X, std::size_t i) const
415 : {
416 0 : auto const& eq_X = *find_equation(m_pbes, X);
417 0 : auto const& d = eq_X.parameters()[i];
418 0 : std::ostringstream out;
419 0 : out << "(" << X << ", " << i << ", " << d << ")";
420 0 : return out.str();
421 0 : }
422 :
423 0 : std::string log_related_parameters(const core::identifier_string& X,
424 : std::size_t n,
425 : const core::identifier_string& Y,
426 : std::size_t m,
427 : const predicate_variable& Ye,
428 : const std::string& reason = ""
429 : ) const
430 : {
431 0 : std::ostringstream out;
432 0 : if (X != Y || n != m)
433 : {
434 0 : out << print_cfp(X, n) << " and " << print_cfp(Y, m) << " are related " << "because of recursion " << Ye << " in the equation for " << X << reason;
435 : }
436 0 : return out.str();
437 0 : }
438 :
439 : // Determines which control flow parameters are related. This is done by assigning neighbors to the
440 : // vertices in m_GCFP_graph.
441 27 : void compute_related_GCFP_parameters()
442 : {
443 27 : mCRL2log(log::debug) << "=== computing related global control flow parameters ===" << std::endl;
444 27 : const std::vector<stategraph_equation>& equations = m_pbes.equations();
445 :
446 : // step 1: create vertices in m_GCFP_graph
447 89 : for (const stategraph_equation& equation: equations)
448 : {
449 62 : auto const& X = equation.variable().name();
450 62 : auto const& d_X = equation.parameters();
451 231 : for (std::size_t n = 0; n < d_X.size(); n++)
452 : {
453 169 : if (is_GCFP_parameter(X, n))
454 : {
455 65 : m_GCFP_graph.add_vertex(GCFP_vertex(X, n, d_X[n]));
456 : }
457 : }
458 : }
459 :
460 : // step 2: create edges between related vertices in m_GCFP_graph
461 89 : for (const stategraph_equation& equation: equations)
462 : {
463 62 : auto const& X = equation.variable().name();
464 62 : auto const& predvars = equation.predicate_variables();
465 170 : for (const predicate_variable& Ye: predvars)
466 : {
467 108 : auto const& Y = Ye.name();
468 108 : auto const& copy = Ye.copy();
469 293 : for (const auto& j: copy)
470 : {
471 185 : std::size_t n = j.first;
472 185 : std::size_t m = j.second;
473 185 : if (is_GCFP_parameter(X, n) && is_GCFP_parameter(Y, m))
474 : {
475 48 : if (m_use_alternative_gcfp_relation)
476 : {
477 : // Twee parameters zijn alleen gerelateerd als er een copy is van de een naar de ander,
478 : // EN dat de target in dat geval ongedefinieerd is (dus we weten echt geen concrete waarde
479 : // voor de parameter op dat punt).
480 0 : if (is_undefined(Ye.target(), m))
481 : {
482 0 : mCRL2log(log::debug) << log_related_parameters(X, n, Y, m, Ye) << std::endl;
483 0 : relate_GCFP_vertices(X, n, Y, m);
484 : }
485 : }
486 : else
487 : {
488 48 : mCRL2log(log::debug) << log_related_parameters(X, n, Y, m, Ye, " (target is undefined)") << std::endl;
489 48 : relate_GCFP_vertices(X, n, Y, m);
490 : }
491 : }
492 : }
493 : }
494 : }
495 27 : }
496 :
497 : // a connected component is valid if it does not contain two nodes (X, n) and (Y, m) with X == Y
498 86 : bool is_valid_connected_component(const std::set<std::size_t>& component) const
499 : {
500 86 : std::set<core::identifier_string> V;
501 243 : for (std::size_t i: component)
502 : {
503 159 : auto const& X = m_GCFP_graph.vertex(i).name();
504 159 : if (V.find(X) != V.end())
505 : {
506 2 : return false;
507 : }
508 157 : V.insert(X);
509 : }
510 84 : return true;
511 86 : }
512 :
513 0 : std::string print_connected_component(const std::set<std::size_t>& component) const
514 : {
515 0 : std::ostringstream out;
516 0 : out << "{";
517 0 : for (auto i = component.begin(); i != component.end(); ++i)
518 : {
519 0 : if (i != component.begin())
520 : {
521 0 : out << ", ";
522 : }
523 0 : out << m_GCFP_graph.vertex(*i);
524 : }
525 0 : out << "}";
526 0 : if (!is_valid_connected_component(component))
527 : {
528 0 : out << " (invalid)";
529 : }
530 0 : return out.str();
531 0 : }
532 :
533 54 : void print_connected_components() const
534 : {
535 123 : for (const std::set<std::size_t>& component: m_connected_components)
536 : {
537 69 : mCRL2log(log::debug) << print_connected_component(component) << std::endl;
538 : }
539 54 : }
540 :
541 : // compute the connected component belonging to vertex i in m_GCFP_graph
542 36 : std::set<std::size_t> compute_connected_component(std::size_t i, std::vector<bool>& done) const
543 : {
544 : using utilities::detail::pick_element;
545 :
546 36 : std::set<std::size_t> todo;
547 36 : std::set<std::size_t> component;
548 :
549 36 : todo.insert(i);
550 101 : while (!todo.empty())
551 : {
552 65 : std::size_t u_index = pick_element(todo);
553 65 : const GCFP_vertex& u = m_GCFP_graph.vertex(u_index);
554 65 : done[u_index] = true;
555 65 : component.insert(u_index);
556 :
557 140 : for (GCFP_vertex* w: u.neighbors())
558 : {
559 75 : std::size_t w_index = m_GCFP_graph.index(*w);
560 75 : if (!done[w_index])
561 : {
562 35 : todo.insert(w_index);
563 : }
564 : }
565 : }
566 72 : return component;
567 36 : }
568 :
569 27 : void compute_connected_components()
570 : {
571 27 : mCRL2log(log::debug) << "=== computing connected components ===" << std::endl;
572 :
573 : // done[i] means that vertex i in m_GCFP_graph has been processed
574 27 : std::vector<bool> done(m_GCFP_graph.vertices().size(), false);
575 :
576 92 : for (std::size_t i = 0; i < done.size(); i++)
577 : {
578 65 : if (done[i])
579 : {
580 29 : continue;
581 : }
582 36 : std::set<std::size_t> component = compute_connected_component(i, done);
583 36 : m_connected_components.push_back(component);
584 36 : }
585 27 : mCRL2log(log::debug) << "--- computed connected components ---" << std::endl;
586 27 : print_connected_components();
587 27 : }
588 :
589 : // removes the connected components V for which !is_valid_connected_component(V)
590 27 : void remove_invalid_connected_components()
591 : {
592 27 : auto i = std::remove_if(m_connected_components.begin(), m_connected_components.end(),
593 36 : [this](const std::set<std::size_t>& component){ return !is_valid_connected_component(component); });
594 27 : m_connected_components.erase(i, m_connected_components.end());
595 27 : }
596 :
597 : // Returns true if d_X[m] is not only copied.
598 : //
599 : // A CFP d_X[m] is not only copied if
600 : // (1) for some i : source(X, i, m) is defined
601 : // or (2) for some Y, i : pred(phi_Y , i) = X and target(Y, i, m) is defined
602 37 : bool is_not_only_copied(const core::identifier_string& X, std::size_t m) const
603 : {
604 : // check (1)
605 37 : auto const& eq_X = *find_equation(m_pbes, X);
606 37 : auto const& predvars = eq_X.predicate_variables();
607 52 : for (const predicate_variable& predvar: predvars)
608 : {
609 40 : if (!is_undefined(predvar.source(), m))
610 : {
611 25 : return true;
612 : }
613 : }
614 :
615 : // check (2)
616 30 : for (const stategraph_equation& equation: m_pbes.equations())
617 : {
618 50 : for (const auto& predvar: equation.predicate_variables())
619 : {
620 32 : if (predvar.name() == X && !is_undefined(predvar.target(), m))
621 : {
622 8 : return true;
623 : }
624 : }
625 : }
626 4 : return false;
627 : }
628 :
629 : // Returns true if all CFPs in component are 'only copied'
630 34 : bool has_only_copied_CFPs(const std::set<std::size_t>& component) const
631 : {
632 38 : for (std::size_t i: component)
633 : {
634 37 : const GCFP_vertex& u = m_GCFP_graph.vertex(i);
635 37 : const auto& X = u.name();
636 37 : auto m = u.index();
637 37 : if (is_not_only_copied(X, m))
638 : {
639 33 : return false;
640 : }
641 : }
642 1 : return true;
643 : }
644 :
645 : // Removes the connected components V that consist of CFPs that are only copied.
646 27 : void remove_only_copy_components()
647 : {
648 27 : auto i = std::remove_if(m_connected_components.begin(),
649 : m_connected_components.end(),
650 34 : [this](const std::set<std::size_t>& component){ return has_only_copied_CFPs(component); });
651 27 : m_connected_components.erase(i, m_connected_components.end());
652 27 : mCRL2log(log::debug) << "--- connected components after removing 'only copy' ones ---" << std::endl;
653 27 : print_connected_components();
654 27 : }
655 :
656 : const std::vector<bool>& is_GCFP(const core::identifier_string& X) const
657 : {
658 : auto i = m_is_GCFP.find(X);
659 : assert (i != m_is_GCFP.end());
660 : return i->second;
661 : }
662 :
663 : // returns the control flow parameters of the propositional variable with name X
664 : std::set<data::variable> control_flow_parameters(const core::identifier_string& X) const
665 : {
666 : std::set<data::variable> result;
667 : const std::vector<bool>& b = is_GCFP(X);
668 : auto const& eq_X = *find_equation(m_pbes, X);
669 : auto const& d_X = eq_X.parameters();
670 : std::size_t index = 0;
671 : for (auto i = d_X.begin(); i != d_X.end(); ++i, index++)
672 : {
673 : if (b[index])
674 : {
675 : result.insert(*i);
676 : }
677 : }
678 : return result;
679 : }
680 :
681 : std::vector<std::size_t> control_flow_parameter_indices(const core::identifier_string& X) const
682 : {
683 : std::vector<std::size_t> result;
684 : auto const& eq_X = *find_equation(m_pbes, X);
685 : auto const& d_X = eq_X.parameters();
686 : for (std::size_t k = 0; k < d_X.size(); k++)
687 : {
688 : if (is_global_control_flow_parameter(X, k))
689 : {
690 : result.push_back(k);
691 : }
692 : }
693 : return result;
694 : }
695 :
696 : std::string print_data_parameters(const core::identifier_string& X, const std::set<std::size_t>& I) const
697 : {
698 : std::ostringstream out;
699 : out << " data parameters for vertex " << X << ":";
700 : for (std::size_t q: I)
701 : {
702 : out << " " << print_cfp(X, q);
703 : }
704 : return out.str();
705 : }
706 :
707 : // set the control flow and data parameter information in p
708 27 : void set_parameters(const stategraph_pbes& p)
709 : {
710 : // set control flow parameters
711 27 : std::map<core::identifier_string, std::set<std::size_t> > CFP; // CFP["X"] is the set of indices of control flow parameters of equation "X"
712 60 : for (const std::set<std::size_t>& component: m_connected_components)
713 : {
714 85 : for (std::size_t j: component)
715 : {
716 52 : const GCFP_vertex& u = m_GCFP_graph.vertex(j);
717 52 : if (u.has_variable())
718 : {
719 52 : CFP[u.name()].insert(u.index());
720 : }
721 : }
722 : }
723 76 : for (auto& i: CFP)
724 : {
725 49 : auto const& X = i.first;
726 49 : auto const& eqn = *find_equation(p, X);
727 49 : eqn.set_control_flow_parameters(i.second);
728 : }
729 :
730 : // set data parameters
731 89 : for (const stategraph_equation& eq_X: m_pbes.equations())
732 : {
733 62 : auto const& X = eq_X.variable().name();
734 62 : std::set<std::size_t> I; // data parameters of equation eq_X
735 231 : for (std::size_t i = 0; i < eq_X.parameters().size(); ++i)
736 : {
737 169 : I.insert(i);
738 : }
739 136 : for (const std::set<std::size_t>& component : m_connected_components)
740 : {
741 200 : for (std::size_t j: component)
742 : {
743 126 : const GCFP_vertex& u = m_GCFP_graph.vertex(j);
744 126 : if (u.name() == X && u.index() != data::undefined_index())
745 : {
746 52 : I.erase(u.index());
747 : }
748 : }
749 : }
750 62 : eq_X.set_data_parameters(I);
751 62 : }
752 27 : }
753 :
754 : // prints all vertices of the connected components
755 27 : void print_final_control_flow_parameters() const
756 : {
757 27 : std::ostringstream out;
758 27 : mCRL2log(log::verbose) << "--- computed control flow parameters ---" << std::endl;
759 :
760 : // collect the control flow points in the map CFP
761 27 : std::map<core::identifier_string, std::set<const GCFP_vertex*> > CFP;
762 60 : for (const std::set<std::size_t>& component: m_connected_components)
763 : {
764 85 : for (std::size_t j: component)
765 : {
766 52 : const GCFP_vertex& u = m_GCFP_graph.vertex(j);
767 52 : if (u.has_variable())
768 : {
769 52 : CFP[u.name()].insert(&u);
770 : }
771 : }
772 : }
773 :
774 : // print the map CFP
775 76 : for (auto i = CFP.begin(); i != CFP.end(); ++i)
776 : {
777 49 : if (i != CFP.begin())
778 : {
779 26 : out << "\n";
780 : }
781 49 : auto const& V = i->second;
782 101 : for (auto j = V.begin(); j != V.end(); ++j)
783 : {
784 52 : if (j != V.begin())
785 : {
786 3 : out << ", ";
787 : }
788 52 : out << **j;
789 : }
790 : }
791 27 : mCRL2log(log::verbose) << out.str() << std::endl;
792 27 : }
793 :
794 : /// \brief Constructor.
795 27 : stategraph_algorithm(const pbes& p, const pbesstategraph_options& options)
796 27 : : m_datar(p.data(), options.rewrite_strategy),
797 27 : m_use_alternative_lcfp_criterion(options.use_alternative_lcfp_criterion),
798 27 : m_use_alternative_gcfp_relation(options.use_alternative_gcfp_relation),
799 27 : m_use_alternative_gcfp_consistency(options.use_alternative_gcfp_consistency),
800 54 : m_options(options)
801 : {
802 27 : m_pbes = stategraph_pbes(p, m_datar);
803 27 : }
804 :
805 : /// \brief Destructor.
806 27 : virtual ~stategraph_algorithm() = default;
807 :
808 : /// \brief Returns the connected components of the global control flow graph.
809 26 : const std::vector<std::set<std::size_t> >& connected_components() const
810 : {
811 26 : return m_connected_components;
812 : }
813 :
814 50 : std::string print(const GCFP_vertex& u) const
815 : {
816 50 : std::ostringstream out;
817 50 : out << '(' << u.name() << ", " << find_equation(m_pbes, u.name())->parameters()[u.index()].name() << ')';
818 100 : return out.str();
819 50 : }
820 :
821 : /// \brief Computes the values that the CFPs in component can attain.
822 33 : std::set<data::data_expression> compute_connected_component_values(const std::set<std::size_t>& component)
823 : {
824 33 : std::set<data::data_expression> result;
825 :
826 : // search for a node that corresponds to a variable in the init of the PBES
827 33 : const propositional_variable_instantiation& init = m_pbes.initial_state();
828 33 : auto const& Xinit = init.name();
829 :
830 85 : for (std::size_t j: component)
831 : {
832 52 : const GCFP_vertex& u = m_GCFP_graph.vertex(j);
833 52 : if (u.name() == Xinit)
834 : {
835 20 : const data::data_expression& d = nth_element(init.parameters(), u.index());
836 20 : result.insert(d);
837 : }
838 : }
839 :
840 : // source(X, i, k) = v
841 85 : for (std::size_t p: component)
842 : {
843 52 : const GCFP_vertex& u = m_GCFP_graph.vertex(p);
844 52 : auto const& X = u.name();
845 52 : std::size_t k = u.index();
846 52 : auto const& eq_X = *find_equation(m_pbes, X);
847 145 : for (const predicate_variable& predvar: eq_X.predicate_variables())
848 : {
849 93 : auto q = predvar.source().find(k);
850 93 : if (q != predvar.source().end())
851 : {
852 77 : const data::data_expression& v = q->second;
853 77 : result.insert(v);
854 : }
855 : }
856 : }
857 :
858 : // target(X, i, k) = v
859 85 : for (std::size_t p: component)
860 : {
861 52 : const GCFP_vertex& u = m_GCFP_graph.vertex(p);
862 52 : auto const& Y = u.name();
863 52 : std::size_t k = u.index();
864 52 : auto const& eq_Y = *find_equation(m_pbes, Y);
865 145 : for (const predicate_variable& predvar: eq_Y.predicate_variables())
866 : {
867 93 : if (predvar.name() != Y)
868 : {
869 61 : continue;
870 : }
871 32 : auto q = predvar.target().find(k);
872 32 : if (q != predvar.target().end())
873 : {
874 31 : const data::data_expression& v = q->second;
875 31 : result.insert(v);
876 : }
877 : }
878 : }
879 :
880 33 : return result;
881 0 : }
882 :
883 27 : void compute_connected_component_values()
884 : {
885 27 : mCRL2log(log::debug) << "=== computing values for the components" << std::endl;
886 60 : for (const std::set<std::size_t>& component: m_connected_components)
887 : {
888 33 : std::set<data::data_expression> values = compute_connected_component_values(component);
889 33 : m_connected_components_values.push_back(values);
890 33 : mCRL2log(log::debug) << print_connected_component(component) << " values = " << core::detail::print_set(values) << std::endl;
891 33 : }
892 27 : }
893 :
894 : // Returns the possible values of the vertex (X, j). N.B. Very inefficient!
895 : std::vector<data::data_expression> compute_values(const core::identifier_string& X, std::size_t j) const
896 : {
897 : // search for a graph that contains (X, j)
898 : for (std::size_t k = 0; k < m_local_control_flow_graphs.size(); k++)
899 : {
900 : auto const& Gk = m_local_control_flow_graphs[k];
901 : if (Gk.has_vertex(X, j))
902 : {
903 : auto const& values = m_connected_components_values[k];
904 : return std::vector<data::data_expression>(values.begin(), values.end());
905 : }
906 : }
907 : throw mcrl2::runtime_error("error in compute_values: vertex not found");
908 : }
909 :
910 : /// \brief Computes the control flow graph
911 27 : virtual void run()
912 : {
913 27 : simplify(m_pbes);
914 27 : m_pbes.compute_source_target_copy();
915 27 : mCRL2log(log::debug) << "--- source, target, copy ---\n" << m_pbes.print_source_target_copy() << std::endl;
916 27 : compute_control_flow_parameters();
917 27 : remove_invalid_connected_components();
918 27 : remove_only_copy_components();
919 27 : mCRL2log(log::trace) << "--- GCFP graph = ---\n" << m_GCFP_graph << std::endl;
920 27 : set_parameters(m_pbes);
921 27 : print_final_control_flow_parameters();
922 :
923 27 : start_timer("compute_connected_component_values");
924 27 : compute_connected_component_values();
925 27 : finish_timer("compute_connected_component_values");
926 27 : }
927 :
928 0 : const stategraph_pbes& get_pbes() const
929 : {
930 0 : return m_pbes;
931 : }
932 :
933 31 : const GCFP_graph& GCFP() const
934 : {
935 31 : return m_GCFP_graph;
936 : }
937 :
938 : const std::vector<local_control_flow_graph>& local_graphs() const
939 : {
940 : return m_local_control_flow_graphs;
941 : }
942 : };
943 :
944 : } // namespace detail
945 :
946 : } // namespace pbes_system
947 :
948 : } // namespace mcrl2
949 :
950 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_ALGORITHM_H
|
