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_reset_variables.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_DETAIL_STATEGRAPH_LOCAL_RESET_VARIABLES_H
13 : #define MCRL2_PBES_DETAIL_STATEGRAPH_LOCAL_RESET_VARIABLES_H
14 :
15 : #include "mcrl2/pbes/detail/stategraph_local_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 : template <typename Container>
25 : std::string print_vector(const Container& v, const std::string& delim)
26 : {
27 : std::ostringstream os;
28 : for (auto i = v.begin(); i != v.end(); ++i)
29 : {
30 : if(i != v.begin())
31 : {
32 : os << delim;
33 : }
34 : os << *i;
35 : }
36 : return os.str();
37 : }
38 :
39 : class local_reset_variables_algorithm;
40 : pbes_expression local_reset_variables(local_reset_variables_algorithm& algorithm, const pbes_expression& x, const stategraph_equation& eq_X);
41 :
42 : /// \brief Adds the reset variables procedure to the stategraph algorithm
43 : class local_reset_variables_algorithm: public stategraph_local_algorithm
44 : {
45 : public:
46 : typedef stategraph_local_algorithm super;
47 :
48 : protected:
49 : const pbes m_original_pbes; // TODO: make this a const reference again
50 : pbes m_transformed_pbes; // will contain the result of the computation
51 :
52 : // if true, the resulting PBES is simplified
53 : bool m_simplify;
54 :
55 : // m_occurring_data_parameters[X] contains the indices of data parameters that occur in at least one local control flow graph
56 : std::map<core::identifier_string, std::set<std::size_t> > m_occurring_data_parameters;
57 :
58 : // returns a default value for the given sort, that corresponds to parameter d_X[j]
59 0 : data::data_expression default_value(const core::identifier_string& X, std::size_t j, const data::sort_expression& x)
60 : {
61 0 : auto const& Xinit = m_pbes.initial_state();
62 0 : if (X == Xinit.name())
63 : {
64 0 : return nth_element(Xinit.parameters(), j);
65 : }
66 :
67 : // TODO: make this an attribute
68 0 : data::representative_generator f(m_pbes.data());
69 0 : return f(x);
70 0 : }
71 :
72 1 : void compute_occurring_data_parameters()
73 : {
74 1 : m_occurring_data_parameters.clear();
75 :
76 : // first collect all parameters (X, p) that are being used in a local control flow graph
77 4 : for (auto& G: m_local_control_flow_graphs)
78 : {
79 3 : auto const& V = G.vertices;
80 9 : for (const auto& u: V)
81 : {
82 6 : auto const& X = u.name();
83 6 : auto p = u.index();
84 6 : m_occurring_data_parameters[X].insert(p);
85 : }
86 : }
87 :
88 : // then intersect them with the data parameter indices
89 3 : for (auto& i: m_occurring_data_parameters)
90 : {
91 2 : auto const& X = i.first;
92 2 : auto const& eq_X = *find_equation(m_pbes, X);
93 2 : auto const& dp_X = eq_X.data_parameter_indices();
94 2 : i.second = utilities::detail::set_intersection(i.second, std::set<std::size_t>(dp_X.begin(), dp_X.end()));
95 : }
96 1 : }
97 :
98 : data::data_expression_list reset_variable_parameters(const propositional_variable_instantiation& x,
99 : const stategraph_equation& eq_X, std::size_t i);
100 :
101 : public:
102 :
103 : // expands a propositional variable instantiation using the control flow graph
104 : // x = Y(e)
105 : // Y(e) = PVI(phi_X, i)
106 3 : pbes_expression reset_variable(const propositional_variable_instantiation& x, const stategraph_equation& eq_X, std::size_t i)
107 : {
108 3 : const predicate_variable& Ye = eq_X.predicate_variables()[i];
109 3 : data::data_expression_list e = reset_variable_parameters(x, eq_X, i);
110 6 : return propositional_variable_instantiation(Ye.name(), e);
111 3 : }
112 :
113 : // Applies resetting of variables to the original PBES p.
114 1 : void reset_variables_to_original(pbes& p)
115 : {
116 1 : mCRL2log(log::debug) << "=== resetting variables to the original PBES ---" << std::endl;
117 :
118 : // apply the reset variable procedure to all propositional variable instantiations
119 1 : std::vector<pbes_equation>& p_eqn = p.equations();
120 1 : const std::vector<stategraph_equation>& s_eqn = m_pbes.equations();
121 :
122 3 : for (std::size_t k = 0; k < p_eqn.size(); k++)
123 : {
124 2 : mCRL2log(log::trace) << "--- resetting equation " << p_eqn[k] << std::endl;
125 2 : p_eqn[k].formula() = local_reset_variables(*this, p_eqn[k].formula(), s_eqn[k]);
126 : }
127 :
128 : // Commented out, since Tim thinks this should not have any effect
129 : // if (m_simplify)
130 : // {
131 : // pbes_system::simplify_data_rewriter<data::rewriter> pbesr(m_datar);
132 : // pbes_system::pbes_rewrite(p, pbesr);
133 : // }
134 1 : }
135 :
136 1 : local_reset_variables_algorithm(const pbes& p, const pbesstategraph_options& options)
137 1 : : stategraph_local_algorithm(p, options),
138 1 : m_original_pbes(p),
139 1 : m_simplify(options.simplify)
140 1 : {}
141 :
142 : /// \brief Runs the stategraph algorithm
143 : /// \param simplify If true, simplify the resulting PBES
144 : /// \param apply_to_original_pbes Apply resetting variables to the original PBES instead of the STATEGRAPH one
145 1 : void run() override
146 : {
147 1 : super::run();
148 1 : m_transformed_pbes = m_original_pbes;
149 1 : compute_occurring_data_parameters();
150 :
151 1 : start_timer("reset_variables_to_original");
152 1 : reset_variables_to_original(m_transformed_pbes);
153 1 : finish_timer("reset_variables_to_original");
154 1 : }
155 :
156 0 : const pbes& result() const
157 : {
158 0 : return m_transformed_pbes;
159 : }
160 : };
161 :
162 : /// N.B. It is essential that this traverser uses the same traversal order as the guard_traverser.
163 : struct local_reset_traverser: public pbes_expression_traverser<local_reset_traverser>
164 : {
165 : typedef pbes_expression_traverser<local_reset_traverser> super;
166 : using super::enter;
167 : using super::leave;
168 : using super::apply;
169 :
170 : local_reset_variables_algorithm& algorithm;
171 : const stategraph_equation& eq_X;
172 : std::size_t& i;
173 :
174 2 : local_reset_traverser(local_reset_variables_algorithm& algorithm_, const stategraph_equation& eq_X_, std::size_t& i_)
175 2 : : algorithm(algorithm_),
176 2 : eq_X(eq_X_),
177 2 : i(i_)
178 2 : {}
179 :
180 : std::vector<pbes_expression> expression_stack;
181 :
182 12 : void push(const pbes_expression& x)
183 : {
184 12 : mCRL2log(log::trace) << "<push>" << "\n" << x << std::endl;
185 12 : expression_stack.push_back(x);
186 12 : }
187 :
188 12 : pbes_expression& top()
189 : {
190 12 : return expression_stack.back();
191 : }
192 :
193 : const pbes_expression& top() const
194 : {
195 : return expression_stack.back();
196 : }
197 :
198 10 : pbes_expression pop()
199 : {
200 10 : pbes_expression result = top();
201 10 : expression_stack.pop_back();
202 10 : return result;
203 : }
204 :
205 4 : void leave(const data::data_expression& x)
206 : {
207 4 : push(x);
208 4 : }
209 :
210 3 : void leave(const pbes_system::propositional_variable_instantiation& x)
211 : {
212 3 : pbes_expression result = algorithm.reset_variable(x, eq_X, i);
213 3 : mCRL2log(log::trace) << "reset variable " << x << " with index " << i << " to " << result << std::endl;
214 3 : i++;
215 3 : push(result);
216 3 : }
217 :
218 0 : void leave(const pbes_system::not_& /* x */)
219 : {
220 0 : pbes_expression operand = pop();
221 0 : push(not_(static_cast<atermpp::aterm_appl>(operand)));
222 0 : }
223 :
224 2 : void leave(const pbes_system::and_& /* x */)
225 : {
226 2 : pbes_expression right = pop();
227 2 : pbes_expression left = pop();
228 2 : push(and_(left, right));
229 2 : }
230 :
231 0 : void leave(const pbes_system::or_& /* x */)
232 : {
233 0 : pbes_expression right = pop();
234 0 : pbes_expression left = pop();
235 0 : push(or_(left, right));
236 0 : }
237 :
238 3 : void leave(const pbes_system::imp& /* x */)
239 : {
240 3 : pbes_expression right = pop();
241 3 : pbes_expression left = pop();
242 3 : push(imp(left, right));
243 3 : }
244 :
245 0 : void leave(const pbes_system::forall& x)
246 : {
247 0 : pbes_expression operand = pop();
248 0 : push(forall(x.variables(), operand));
249 0 : }
250 :
251 0 : void leave(const pbes_system::exists& x)
252 : {
253 0 : pbes_expression operand = pop();
254 0 : push(exists(x.variables(), operand));
255 0 : }
256 : };
257 :
258 : inline
259 2 : pbes_expression local_reset_variables(local_reset_variables_algorithm& algorithm, const pbes_expression& x, const stategraph_equation& eq_X)
260 : {
261 2 : std::size_t i = 0;
262 2 : local_reset_traverser f(algorithm, eq_X, i);
263 2 : f.apply(x);
264 4 : return f.top();
265 2 : }
266 :
267 3 : data::data_expression_list local_reset_variables_algorithm::reset_variable_parameters(const propositional_variable_instantiation& x, const stategraph_equation& eq_X, std::size_t i)
268 : {
269 : using utilities::detail::contains;
270 :
271 : // mCRL2log(log::debug) << "--- resetting variable Y(e) = " << x << " with index " << i << std::endl;
272 3 : assert(i < eq_X.predicate_variables().size());
273 3 : const predicate_variable& Ye = eq_X.predicate_variables()[i];
274 3 : assert(Ye.variable() == x);
275 :
276 3 : const core::identifier_string& X = eq_X.variable().name();
277 3 : const core::identifier_string& Y = Ye.name();
278 3 : const stategraph_equation& eq_Y = *find_equation(m_pbes, Y);
279 3 : const data::data_expression_list& e = x.parameters();
280 3 : std::vector<data::data_expression> e1(e.begin(), e.end());
281 3 : const std::vector<data::variable>& d_Y = eq_Y.parameters();
282 3 : assert(d_Y.size() == Ye.parameters().size());
283 3 : const std::size_t J = m_local_control_flow_graphs.size();
284 :
285 3 : auto const& dp_Y = eq_Y.data_parameter_indices();
286 6 : for (std::size_t k: dp_Y)
287 : {
288 3 : bool relevant = true;
289 3 : std::set<data::data_expression> condition;
290 12 : for (std::size_t j = 0; j < J; j++)
291 : {
292 9 : auto const& Vj = m_local_control_flow_graphs[j];
293 9 : auto& Bj = m_belongs[j];
294 9 : default_rules_predicate rules(Vj);
295 9 : if (rules(X, i))
296 : {
297 5 : auto const& v = Vj.find_vertex(Y); // v = (Y, p, q)
298 5 : std::size_t p = v.index();
299 5 : auto di = Ye.target().find(p);
300 5 : if (di != Ye.target().end())
301 : {
302 3 : auto const& q1 = di->second; // q1 = target(X, i, p)
303 3 : auto const& u = Vj.find_vertex(local_control_flow_graph_vertex(Y, p, data::undefined_variable(), q1));
304 3 : if (contains(Bj[Y], d_Y[k]) && !contains(u.marking(), d_Y[k]))
305 : {
306 0 : relevant = false;
307 0 : break;
308 : }
309 : }
310 2 : else if(!v.has_variable())
311 : {
312 2 : if (contains(Bj[Y], d_Y[k]) && !contains(v.marking(), d_Y[k]))
313 : {
314 0 : relevant = false;
315 0 : break;
316 : }
317 : }
318 : else
319 : {
320 : // update relevant and condition
321 0 : if (contains(Bj[Y], d_Y[k]))
322 : {
323 0 : bool found = false;
324 0 : for (const auto& w: Vj.vertices)
325 : {
326 0 : if (w.name() == Y && w.index() == p) // w = (Y, p, d_Y[p]=r)
327 : {
328 0 : if (contains(w.marking(), d_Y[k]))
329 : {
330 0 : found = true;
331 : }
332 : else
333 : {
334 0 : if (w.has_variable())
335 : {
336 0 : auto const& r = w.value();
337 0 : condition.insert(data::equal_to(nth_element(e, p), r));
338 : }
339 : }
340 : }
341 : }
342 0 : if (!found)
343 : {
344 0 : relevant = false;
345 0 : break;
346 : }
347 : }
348 : }
349 : }
350 : }
351 3 : if (!relevant)
352 : {
353 0 : e1[k] = default_value(Y, k, e1[k].sort());
354 : }
355 : else
356 : {
357 3 : if (!condition.empty())
358 : {
359 0 : e1[k] = data::if_(data::lazy::join_or(condition.begin(), condition.end()), default_value(Y, k, e1[k].sort()), nth_element(e, k));
360 0 : mCRL2log(log::trace) << " reset copy Y = " << Y << " k = " << k << " e'[k] = " << e1[k] << std::endl;
361 : }
362 : }
363 3 : }
364 6 : return data::data_expression_list(e1.begin(), e1.end());
365 3 : }
366 :
367 :
368 : } // namespace detail
369 :
370 : } // namespace pbes_system
371 :
372 : } // namespace mcrl2
373 :
374 : #endif // MCRL2_PBES_DETAIL_STATEGRAPH_LOCAL_RESET_VARIABLES_H
|
