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_global_reset_variables.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_RESET_VARIABLES_H
13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_RESET_VARIABLES_H
14 :
15 : #include "mcrl2/pbes/detail/stategraph_global_algorithm.h"
16 : #include "mcrl2/pbes/detail/stategraph_reset_variables.h"
17 :
18 : namespace mcrl2 {
19 :
20 : namespace pbes_system {
21 :
22 : namespace detail {
23 :
24 : class global_reset_variables_algorithm;
25 : pbes_expression reset_variables(global_reset_variables_algorithm& algorithm, const pbes_expression& x, const stategraph_equation& eq_X);
26 :
27 : /// \brief Adds the reset variables procedure to the stategraph algorithm
28 : class global_reset_variables_algorithm: public stategraph_global_algorithm
29 : {
30 : public:
31 : typedef stategraph_global_algorithm super;
32 :
33 : protected:
34 : const pbes& m_original_pbes;
35 : pbes m_transformed_pbes; // will contain the result of the computation
36 :
37 : // if true, the resulting PBES is simplified
38 : bool m_simplify;
39 :
40 0 : data::data_expression default_value(const data::sort_expression& x)
41 : {
42 : // TODO: make this an attribute
43 0 : data::representative_generator f(m_pbes.data());
44 0 : return f(x);
45 0 : }
46 :
47 : // returns the parameters of the propositional variable with name X
48 0 : std::set<data::variable> propvar_parameters(const core::identifier_string& X) const
49 : {
50 0 : auto const& eq_X = *find_equation(m_pbes, X);
51 0 : auto const& d_X = eq_X.parameters();
52 0 : return std::set<data::variable>(d_X.begin(), d_X.end());
53 : }
54 :
55 : template <typename Graph>
56 0 : void compute_global_control_flow_marking(Graph& G)
57 : {
58 : using utilities::detail::pick_element;
59 :
60 0 : mCRL2log(log::debug) << "--- compute initial marking ---" << std::endl;
61 :
62 : // initialization
63 0 : for (auto i = G.begin(); i != G.end(); ++i)
64 : {
65 0 : auto const& v = *i;
66 0 : std::set<data::variable> dx = propvar_parameters(v.name());
67 0 : v.set_marking(utilities::detail::set_intersection(v.sig(), dx));
68 0 : mCRL2log(log::debug) << "vertex " << v << " sig = " << core::detail::print_set(v.sig()) << " dx = " << core::detail::print_set(dx) << "\n";
69 : }
70 0 : mCRL2log(log::debug) << "--- initial control flow marking ---\n" << G.print_marking();
71 :
72 : // backwards reachability algorithm
73 0 : std::set<const typename Graph::vertex_type*> todo;
74 0 : for (auto i = G.begin(); i != G.end(); ++i)
75 : {
76 0 : auto const& v = *i;
77 0 : todo.insert(&v);
78 : }
79 0 : mCRL2log(log::debug) << "--- update marking ---" << std::endl;
80 0 : while (!todo.empty())
81 : {
82 0 : auto const& v = *pick_element(todo);
83 0 : mCRL2log(log::debug) << "selected marking todo element " << v << std::endl;
84 0 : std::set<std::size_t> I = v.marking_variable_indices(m_pbes);
85 :
86 0 : auto const& incoming_edges = v.incoming_edges();
87 0 : for (auto ei = incoming_edges.begin(); ei != incoming_edges.end(); ++ei)
88 : {
89 0 : auto const& u = *ei->first;
90 0 : const std::set<std::size_t>& labels = ei->second;
91 0 : for (std::size_t i: labels)
92 : {
93 0 : std::size_t last_size = u.marking().size();
94 0 : const stategraph_equation& eq_X = *find_equation(m_pbes, u.name());
95 0 : const propositional_variable_instantiation& Y = eq_X.predicate_variables()[i].variable();
96 0 : std::set<data::variable> dx = propvar_parameters(u.name());
97 0 : mCRL2log(log::debug) << " vertex u = " << v << " label = " << i << " I = " << print_set(I) << " u.marking = " << core::detail::print_set(u.marking()) << std::endl;
98 0 : for (std::size_t m: I)
99 : {
100 0 : const data::data_expression_list& e = Y.parameters();
101 0 : const data::data_expression& e_m = nth_element(e, m);
102 0 : std::set<data::variable> fv = data::find_free_variables(e_m);
103 0 : u.set_marking(utilities::detail::set_union(utilities::detail::set_intersection(fv, dx), u.marking()));
104 0 : mCRL2log(log::debug) << " m = " << m << " freevars = " << core::detail::print_set(fv) << " dx = " << core::detail::print_set(dx) << "\n";
105 : }
106 0 : if (u.marking().size() > last_size)
107 : {
108 0 : todo.insert(&u);
109 0 : mCRL2log(log::debug) << "updated marking " << u.print_marking() << " using edge " << pbes_system::pp(Y) << "\n";
110 : }
111 : }
112 : }
113 : }
114 :
115 : // set the marking_parameters attributes
116 0 : for (auto i = G.begin(); i != G.end(); ++i)
117 : {
118 0 : auto const& v = *i;
119 0 : const stategraph_equation& eqn = *find_equation(m_pbes, v.name());
120 0 : for (const data::variable& w: eqn.parameters())
121 : {
122 0 : v.add_marked_parameter(v.marking().find(w) != v.marking().end());
123 : }
124 : }
125 0 : }
126 :
127 : // First determine whether this location should be considered
128 : template <typename Vertex>
129 0 : bool location_possibly_reachable(const core::identifier_string& Y, const Vertex& u, const std::vector<data::data_expression>& e_X, const stategraph_equation& eq_X,std::size_t i)
130 : {
131 0 : std::size_t N = e_X.size();
132 0 : data::data_expression_list::const_iterator k = u.values().begin();
133 0 : for (std::size_t j = 0; j < N; ++j)
134 : {
135 0 : if (is_global_control_flow_parameter(Y, j))
136 : {
137 0 : const predicate_variable& X_i = eq_X.predicate_variables()[i];
138 0 : auto target_j = X_i.target().find(j);
139 0 : if (target_j != X_i.target().end())
140 : {
141 0 : data::data_expression f_k = *k;
142 0 : if(f_k != target_j->second)
143 : {
144 0 : return false;
145 : }
146 0 : }
147 0 : ++k;
148 : }
149 : }
150 0 : return true;
151 : }
152 :
153 : public:
154 : // expands a propositional variable instantiation using the control flow graph
155 : // x = Y(e)
156 : // Y(e) = PVI(phi_X, i)
157 0 : pbes_expression reset_variable(const propositional_variable_instantiation& x, const stategraph_equation& eq_X, std::size_t i)
158 : {
159 0 : mCRL2log(log::debug) << "--- resetting variable Y(e) = " << pbes_system::pp(x) << " with index " << i << std::endl;
160 0 : assert(eq_X.predicate_variables()[i].variable() == x);
161 :
162 0 : std::vector<pbes_expression> phi;
163 0 : const core::identifier_string& Y = x.name();
164 0 : std::vector<data::data_expression> e(x.parameters().begin(),x.parameters().end());
165 :
166 : // iterate over the alternatives as defined by the control flow graph
167 0 : auto inst = m_control_flow_graph.index(Y);
168 0 : if (inst.empty())
169 : {
170 0 : mCRL2log(log::verbose) << "Equation " << Y << " is not reachable!" << std::endl;
171 : }
172 0 : for (auto q: inst)
173 : {
174 0 : auto& u = *q;
175 0 : mCRL2log(log::debug) << " vertex u = " << u << std::endl;
176 :
177 0 : if(!location_possibly_reachable(Y, u, e, eq_X, i))
178 : {
179 0 : continue;
180 : }
181 :
182 : // Now build the actual formula
183 0 : std::vector<data::data_expression> r;
184 0 : std::size_t N = u.marked_parameters().size();
185 0 : assert(e.size() == u.marked_parameters().size());
186 0 : auto k = u.values().begin();
187 0 : data::data_expression condition = data::true_();
188 0 : for (std::size_t j = 0; j < N; ++j)
189 : {
190 0 : mCRL2log(log::debug) << " j = " << j;
191 0 : if (is_global_control_flow_parameter(Y, j))
192 : {
193 0 : mCRL2log(log::debug) << " CFP(Y, j) = true";
194 0 : const data::data_expression& f_k = *k++;
195 0 : const predicate_variable& X_i = eq_X.predicate_variables()[i];
196 0 : if (X_i.target().find(j) == X_i.target().end() || !m_simplify)
197 : {
198 0 : condition = data::lazy::and_(condition, data::equal_to(e[j], f_k));
199 0 : r.push_back(e[j]);
200 0 : mCRL2log(log::debug) << " target(X, i, j) = false";
201 0 : mCRL2log(log::debug) << " c := c && " << data::pp(data::equal_to(e[j], f_k));
202 : }
203 : else
204 : {
205 0 : r.push_back(X_i.target().find(j)->second);
206 : }
207 0 : mCRL2log(log::debug) << " r := r <| " << data::pp(r.back());
208 :
209 : }
210 0 : else if (u.is_marked_parameter(j))
211 : {
212 0 : mCRL2log(log::debug) << " e[j] is in marking(u)";
213 0 : mCRL2log(log::debug) << " r := r <| " << data::pp(e[j]);
214 0 : r.push_back(e[j]);
215 : }
216 : else
217 : {
218 0 : mCRL2log(log::debug) << " default parameter ";
219 0 : mCRL2log(log::debug) << " r := r <| " << data::pp(default_value(e[j].sort()));
220 0 : r.push_back(default_value(e[j].sort()));
221 : }
222 0 : mCRL2log(log::debug) << std::endl;
223 : }
224 0 : propositional_variable_instantiation Yr(Y, data::data_expression_list(r.begin(),r.end()));
225 0 : if (m_simplify)
226 : {
227 0 : condition = m_datar(condition);
228 0 : if (condition != data::false_())
229 : {
230 0 : phi.push_back(imp(condition, Yr));
231 : }
232 : }
233 : else
234 : {
235 0 : phi.push_back(imp(condition, Yr));
236 : }
237 0 : }
238 0 : return join_and(phi.begin(), phi.end());
239 0 : }
240 :
241 : // Applies resetting of variables to the original PBES p.
242 0 : void reset_variables_to_original(pbes& p)
243 : {
244 0 : mCRL2log(log::debug) << "--- resetting variables to the original PBES ---" << std::endl;
245 :
246 : // apply the reset variable procedure to all propositional variable instantiations
247 0 : std::vector<pbes_equation>& p_eqn = p.equations();
248 0 : const std::vector<stategraph_equation>& s_eqn = m_pbes.equations();
249 :
250 0 : for (std::size_t k = 0; k < p_eqn.size(); k++)
251 : {
252 :
253 0 : p_eqn[k].formula() = reset_variables(*this, p_eqn[k].formula(), s_eqn[k]);
254 : }
255 :
256 : // TODO: merge the two rewriters?
257 0 : if (m_simplify)
258 : {
259 0 : pbes_system::simplify_data_rewriter<data::rewriter> pbesr(m_datar);
260 0 : pbes_system::pbes_rewrite(p, pbesr);
261 : }
262 0 : }
263 :
264 0 : global_reset_variables_algorithm(const pbes& p, const pbesstategraph_options& options)
265 0 : : stategraph_global_algorithm(p, options),
266 0 : m_original_pbes(p),
267 0 : m_simplify(options.simplify)
268 0 : {}
269 :
270 : /// \brief Runs the stategraph algorithm
271 : /// \param simplify If true, simplify the resulting PBES
272 : /// \param apply_to_original_pbes Apply resetting variables to the original PBES instead of the STATEGRAPH one
273 0 : void run() override
274 : {
275 0 : super::run();
276 0 : start_timer("compute_global_control_flow_marking");
277 0 : compute_global_control_flow_marking(m_control_flow_graph);
278 0 : finish_timer("compute_global_control_flow_marking");
279 0 : mCRL2log(log::verbose) << "Computed control flow marking" << std::endl;
280 0 : mCRL2log(log::debug) << "--- control flow marking ---\n" << m_control_flow_graph.print_marking();
281 0 : m_transformed_pbes = m_original_pbes;
282 0 : reset_variables_to_original(m_transformed_pbes);
283 0 : }
284 :
285 0 : const pbes& result() const
286 : {
287 0 : return m_transformed_pbes;
288 : }
289 : };
290 :
291 : /// \brief reset propositional variables
292 : /// N.B. It is essential that this traverser uses the same traversal order as the guard_traverser.
293 : struct reset_traverser: public pbes_expression_traverser<reset_traverser>
294 : {
295 : typedef pbes_expression_traverser<reset_traverser> super;
296 : using super::enter;
297 : using super::leave;
298 : using super::apply;
299 :
300 : global_reset_variables_algorithm& algorithm;
301 : const stategraph_equation& eq_X;
302 : std::size_t& i;
303 :
304 0 : reset_traverser(global_reset_variables_algorithm& algorithm_, const stategraph_equation& eq_X_, std::size_t& i_)
305 0 : : algorithm(algorithm_),
306 0 : eq_X(eq_X_),
307 0 : i(i_)
308 0 : {}
309 :
310 : std::vector<pbes_expression> expression_stack;
311 :
312 0 : void push(const pbes_expression& x)
313 : {
314 0 : mCRL2log(log::trace) << "<push>" << "\n" << x << std::endl;
315 0 : expression_stack.push_back(x);
316 0 : }
317 :
318 0 : pbes_expression& top()
319 : {
320 0 : return expression_stack.back();
321 : }
322 :
323 : const pbes_expression& top() const
324 : {
325 : return expression_stack.back();
326 : }
327 :
328 0 : pbes_expression pop()
329 : {
330 0 : pbes_expression result = top();
331 0 : expression_stack.pop_back();
332 0 : return result;
333 : }
334 :
335 0 : void leave(const data::data_expression& x)
336 : {
337 0 : push(x);
338 0 : }
339 :
340 0 : void leave(const pbes_system::propositional_variable_instantiation& x)
341 : {
342 0 : pbes_expression result = algorithm.reset_variable(x, eq_X, i);
343 0 : mCRL2log(log::debug) << "reset variable " << pbes_system::pp(x) << " with index " << i << " to " << pbes_system::pp(result) << std::endl;
344 0 : i++;
345 0 : push(result);
346 0 : }
347 :
348 0 : void leave(const pbes_system::not_& /* x */)
349 : {
350 0 : pbes_expression operand = pop();
351 0 : push(not_(static_cast<atermpp::aterm_appl>(operand)));
352 0 : }
353 :
354 0 : void leave(const pbes_system::and_& /* x */)
355 : {
356 0 : pbes_expression right = pop();
357 0 : pbes_expression left = pop();
358 0 : push(and_(left, right));
359 0 : }
360 :
361 0 : void leave(const pbes_system::or_& /* x */)
362 : {
363 0 : pbes_expression right = pop();
364 0 : pbes_expression left = pop();
365 0 : push(or_(left, right));
366 0 : }
367 :
368 0 : void leave(const pbes_system::imp& /* x */)
369 : {
370 0 : pbes_expression right = pop();
371 0 : pbes_expression left = pop();
372 0 : push(imp(left, right));
373 0 : }
374 :
375 0 : void leave(const pbes_system::forall& x)
376 : {
377 0 : pbes_expression operand = pop();
378 0 : push(forall(x.variables(), operand));
379 0 : }
380 :
381 0 : void leave(const pbes_system::exists& x)
382 : {
383 0 : pbes_expression operand = pop();
384 0 : push(exists(x.variables(), operand));
385 0 : }
386 : };
387 :
388 : inline
389 0 : pbes_expression reset_variables(global_reset_variables_algorithm& algorithm, const pbes_expression& x, const stategraph_equation& eq_X)
390 : {
391 0 : std::size_t i = 0;
392 0 : reset_traverser f(algorithm, eq_X, i);
393 0 : f.apply(x);
394 0 : return f.top();
395 0 : }
396 :
397 : } // namespace detail
398 :
399 : } // namespace pbes_system
400 :
401 : } // namespace mcrl2
402 :
403 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_GLOBAL_RESET_VARIABLES_H
|
