Line data Source code
1 : // Author(s): Jeroen Keiren
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 binary.h
10 : /// \brief The binary algorithm.
11 :
12 : #ifndef MCRL2_LPS_BINARY_H
13 : #define MCRL2_LPS_BINARY_H
14 :
15 : #include "mcrl2/data/enumerator.h"
16 : #include "mcrl2/lps/detail/lps_algorithm.h"
17 : #include "mcrl2/lps/detail/parameter_selection.h"
18 :
19 : namespace mcrl2
20 : {
21 :
22 : namespace lps
23 : {
24 :
25 : // Compute the number of booleans needed to represent a set of size n.
26 : inline
27 13 : std::size_t nr_of_booleans_for_elements(std::size_t n)
28 : {
29 13 : if(n == 1)
30 : {
31 0 : return 1;
32 : }
33 : else
34 : {
35 13 : return utilities::ceil_log2(n-1);
36 : }
37 : }
38 :
39 : /// \brief Algorithm class that can be used to apply the binary algorithm
40 : ///
41 : /// All parameters of finite data types are replaced with a vector of
42 : /// booleans.
43 : template<typename DataRewriter, typename Specification>
44 : class binary_algorithm: public detail::lps_algorithm<Specification>
45 : {
46 : typedef data::enumerator_list_element_with_substitution<> enumerator_element;
47 : typedef typename detail::lps_algorithm<Specification> super;
48 : typedef typename Specification::process_type process_type;
49 : typedef typename process_type::action_summand_type action_summand_type;
50 : using super::m_spec;
51 :
52 : protected:
53 : /// Rewriter
54 : DataRewriter m_rewriter;
55 :
56 : const std::string m_parameter_selection;
57 :
58 : /// Mapping of finite variables to boolean vectors
59 : std::map<data::variable, std::vector<data::variable> > m_new_parameters;
60 :
61 : /// Mapping of variables to all values they can be assigned
62 : std::map<data::variable, std::vector<data::data_expression> > m_enumerated_elements;
63 :
64 : /// Mapping of variables to corresponding if-tree
65 : data::mutable_map_substitution<> m_if_trees;
66 :
67 : /// Contains the names of variables appearing in rhs of m_if_trees
68 : data::set_identifier_generator m_if_trees_generator;
69 :
70 : /// Identifier generator for the enumerator
71 : data::enumerator_identifier_generator m_id_generator;
72 :
73 : /// \brief Build an if-then-else tree of enumerated elements in terms
74 : /// of new parameters.
75 : /// \pre enumerated_elements.size() <= 2^new_parameters.size()
76 : /// \return if then else tree from enumerated_elements in terms of new_parameters
77 107 : data::data_expression make_if_tree(data::variable_vector new_parameters,
78 : const data::data_expression_vector& enumerated_elements)
79 : {
80 107 : data::data_expression result;
81 :
82 107 : if (new_parameters.empty())
83 : {
84 60 : result = enumerated_elements.front();
85 : }
86 : else
87 : {
88 47 : std::size_t n = enumerated_elements.size();
89 47 : std::size_t m = static_cast<std::size_t>(1) << (new_parameters.size() - 1); //m == 2^(new_parameters.size() - 1)
90 :
91 47 : if (m > n)
92 : {
93 3 : m = n;
94 : }
95 :
96 47 : data::data_expression_vector left_list(enumerated_elements.begin(), enumerated_elements.begin() + m);
97 47 : data::data_expression_vector right_list;
98 47 : if (m == n)
99 : {
100 10 : right_list = data::data_expression_vector(enumerated_elements.begin() + m - 1, enumerated_elements.end());
101 : }
102 : else
103 : {
104 37 : right_list = data::data_expression_vector(enumerated_elements.begin() + m, enumerated_elements.end());
105 : }
106 :
107 47 : data::data_expression condition = new_parameters.back();
108 47 : new_parameters.pop_back();
109 47 : result = if_(condition,
110 : make_if_tree(new_parameters, right_list),
111 : make_if_tree(new_parameters, left_list));
112 47 : }
113 :
114 107 : return result;
115 0 : }
116 :
117 : /// \brief Determine which variables should be replaced, based on parameter_selection
118 : /// \return A subset of the process parameters, with a finite sort that is not Bool
119 9 : std::set<data::variable> select_parameters(const std::string parameter_selection) const
120 : {
121 9 : const data::variable_list& process_parameters = m_spec.process().process_parameters();
122 9 : bool use_selection = !parameter_selection.empty();
123 :
124 9 : std::list<data::variable> selected_params;
125 9 : if (use_selection)
126 : {
127 1 : const data::variable_vector sel =
128 1 : detail::parse_lps_parameter_selection(process_parameters, m_spec.data(), parameter_selection);
129 1 : selected_params = std::list<data::variable>(sel.begin(), sel.end());
130 1 : }
131 : else
132 : {
133 8 : selected_params = std::list<data::variable>(process_parameters.begin(), process_parameters.end());
134 : }
135 9 : selected_params.remove_if([&](const data::variable& v)
136 : {
137 22 : bool cannot_replace = v.sort() == data::sort_bool::bool_() || !m_spec.data().is_certainly_finite(v.sort());
138 22 : if (cannot_replace && use_selection)
139 : {
140 0 : mCRL2log(log::info) << "Not selecting " << v << ":" << v.sort() << " since it is already Bool, or its type is not finite." << std::endl;
141 : }
142 22 : return cannot_replace;
143 : }
144 : );
145 :
146 9 : if (use_selection && selected_params.empty())
147 : {
148 0 : mCRL2log(log::info) << "No parameters were selected to be replaced." << std::endl;
149 : }
150 :
151 18 : return std::set<data::variable>(selected_params.begin(), selected_params.end());
152 9 : }
153 :
154 : /// \brief Take a specification and calculate a vector of boolean variables for each process
155 : /// parameter in selected_params. A mapping variable -> vector of booleans is stored in new_parameters_table
156 : /// a mapping variable -> enumerated elements is stored in enumerated_elements_table
157 : /// \pre all elements in selected_params should not be of type Bool and should have a finite type
158 : /// \return data variable list with the new process parameters (i.e. with all variables of a
159 : /// finite type != bool replaced by a vector of boolean variables.
160 9 : void replace_enumerated_parameters(const std::set<data::variable>& selected_params)
161 : {
162 9 : data::variable_list process_parameters = m_spec.process().process_parameters();
163 9 : data::variable_vector new_parameters;
164 :
165 9 : mCRL2log(log::debug) << "Original process parameters: " << data::pp(process_parameters) << std::endl;
166 :
167 9 : data::set_identifier_generator generator;
168 9 : generator.add_identifiers(lps::find_identifiers(m_spec));
169 9 : generator.add_identifiers(data::function_and_mapping_identifiers(m_spec.data()));
170 9 : bool accept_solutions_with_variables = false;
171 9 : data::enumerator_algorithm<> enumerator(m_rewriter, m_spec.data(), m_rewriter, m_id_generator, accept_solutions_with_variables);
172 :
173 : // Transpose all process parameters, and replace those that are finite, and not bool with boolean variables.
174 42 : for (const data::variable& par: process_parameters)
175 : {
176 24 : if (selected_params.find(par) != selected_params.end())
177 : {
178 : //Get all constructors for par
179 13 : data::data_expression_vector enumerated_elements; // List to store enumerated elements of a parameter
180 :
181 13 : data::mutable_indexed_substitution<> local_sigma;
182 26 : const data::variable_list vl{ par };
183 13 : enumerator.enumerate(enumerator_element(vl, data::sort_bool::true_()),
184 : local_sigma,
185 100 : [&](const enumerator_element& p)
186 : {
187 50 : p.add_assignments(vl, local_sigma, m_rewriter);
188 50 : enumerated_elements.push_back(local_sigma(par));
189 50 : return false;
190 : }
191 : );
192 13 : m_enumerated_elements[par] = enumerated_elements;
193 :
194 : //Calculate the number of booleans needed to encode par
195 13 : std::size_t n = nr_of_booleans_for_elements(enumerated_elements.size());
196 :
197 : //Set hint for fresh variable names
198 13 : std::string par_name = par.name();
199 :
200 : // Temp list for storage
201 13 : data::variable_vector new_pars;
202 : //Create new parameters and add them to the parameter list.
203 36 : for (std::size_t i = 0; i<n; ++i)
204 : {
205 23 : data::variable v(generator(par_name), data::sort_bool::bool_());
206 23 : new_parameters.push_back(v);
207 23 : new_pars.push_back(v);
208 : }
209 : // n = new_pars.size() && new_pars.size() = ceil(log_2(j)) && new_pars.size() = ceil(log_2(enumerated_elements.size()))
210 :
211 13 : mCRL2log(log::verbose) << "Parameter " << data::pp(par) << ":" << data::pp(par.sort()) << " has been replaced by " << new_pars.size() << " parameter(s) " << data::pp(new_pars) << " of sort Bool" << std::endl;
212 :
213 : //Store new parameters in a hastable
214 13 : m_new_parameters[par]=new_pars;
215 :
216 13 : m_if_trees[par]=make_if_tree(new_pars,
217 : enumerated_elements);
218 13 : }
219 : else
220 : {
221 11 : new_parameters.push_back(par);
222 : }
223 : }
224 :
225 9 : mCRL2log(log::debug) << "New process parameter(s): " << data::pp(new_parameters) << std::endl;
226 :
227 9 : m_spec.process().process_parameters() = data::variable_list(new_parameters.begin(),new_parameters.end());
228 32 : for (const data::variable& v: data::substitution_variables(m_if_trees))
229 : {
230 23 : m_if_trees_generator.add_identifier(v.name());
231 : }
232 9 : }
233 :
234 : /// \brief Replace expressions in v that are of a finite sort with a
235 : /// vector of assignments to Boolean variables.
236 9 : data::data_expression_list replace_enumerated_parameters_in_initial_expressions(
237 : const data::variable_list& vl,
238 : const data::data_expression_list& el)
239 : {
240 : // We use replace_variables, to make sure that the binding variables of assignments are ignored.
241 : // Note that this operation is safe because the generated fresh variables can not clash with other
242 : // binding variables.
243 9 : const data::data_expression_list el_ = data::replace_variables(el, m_if_trees);
244 :
245 9 : data::data_expression_vector result;
246 9 : data::variable_list::const_iterator i=vl.begin();
247 42 : for (const data::data_expression& a: el_)
248 : {
249 24 : const data::variable par= *i;
250 24 : i++;
251 24 : if (m_new_parameters.find(par) == m_new_parameters.end()) // This parameter is not replaced by a boolean parameters.
252 : {
253 11 : result.push_back(a);
254 : }
255 : else
256 : {
257 13 : data::variable_vector new_parameters = m_new_parameters[par];
258 13 : data::data_expression_vector elements = m_enumerated_elements[par];
259 :
260 13 : mCRL2log(log::debug) << "Found " << new_parameters.size() << " new parameter(s) for parameter " << data::pp(par) << std::endl;
261 :
262 36 : for (std::size_t j = 0; j < new_parameters.size(); ++j)
263 : {
264 23 : data::data_expression_vector disjuncts;
265 :
266 23 : data::data_expression_vector::iterator k = elements.begin();
267 65 : while (k != elements.end())
268 : {
269 : // Elements that get boolean value false
270 42 : std::ptrdiff_t count(static_cast<std::ptrdiff_t>(1) << j);
271 42 : if (std::distance(k, elements.end()) < count)
272 : {
273 2 : k = elements.end();
274 : }
275 : else
276 : {
277 40 : std::advance(k, count);
278 : }
279 :
280 : // Elements that get value true
281 95 : for (std::ptrdiff_t l = 0; l < count && k != elements.end(); ++l)
282 : {
283 53 : disjuncts.push_back(data::equal_to(a, *k++));
284 : }
285 : }
286 23 : result.push_back(data::lazy::join_or(disjuncts.begin(), disjuncts.end()));
287 : }
288 13 : }
289 : }
290 :
291 9 : mCRL2log(log::debug) << "Replaced expression(s) " << data::pp(el_) << " in the initial state with expression(s) " << data::pp(result) << std::endl;
292 :
293 18 : return data::data_expression_list(result.begin(),result.end());
294 9 : }
295 :
296 : /// \brief Replace assignments in v that are of a finite sort with a
297 : /// vector of assignments to Boolean variables.
298 19 : data::assignment_list replace_enumerated_parameters_in_assignments(data::assignment_list v)
299 : {
300 : // We use replace_variables, to make sure that the binding variables of assignments are ignored.
301 : // Note that this operation is safe because the generated fresh variables can not clash with other
302 : // binding variables.
303 19 : v = data::replace_variables(v, m_if_trees);
304 :
305 19 : data::assignment_vector result;
306 88 : for (const data::assignment& a: v)
307 : {
308 50 : if (m_new_parameters.find(a.lhs()) == m_new_parameters.end())
309 : {
310 29 : result.push_back(a);
311 : }
312 : else
313 : {
314 21 : data::variable_vector new_parameters = m_new_parameters[a.lhs()];
315 21 : data::data_expression_vector elements = m_enumerated_elements[a.lhs()];
316 :
317 21 : mCRL2log(log::debug) << "Found " << new_parameters.size() << " new parameter(s) for parameter " << data::pp(a.lhs()) << std::endl;
318 :
319 50 : for (std::size_t j = 0; j < new_parameters.size(); ++j)
320 : {
321 29 : data::data_expression_vector disjuncts;
322 :
323 29 : data::data_expression_vector::iterator k = elements.begin();
324 74 : while (k != elements.end())
325 : {
326 : // Elements that get boolean value false
327 45 : std::ptrdiff_t count(static_cast<std::ptrdiff_t>(1) << j);
328 45 : if (std::distance(k, elements.end()) < count)
329 : {
330 2 : k = elements.end();
331 : }
332 : else
333 : {
334 43 : std::advance(k, count);
335 : }
336 :
337 : // Elements that get value true
338 100 : for (std::ptrdiff_t l = 0; l < count && k != elements.end(); ++l)
339 : {
340 55 : disjuncts.push_back(data::equal_to(a.rhs(), *k++));
341 : }
342 : }
343 29 : result.push_back(data::assignment(new_parameters[j], data::lazy::join_or(disjuncts.begin(), disjuncts.end())));
344 : }
345 :
346 21 : }
347 : }
348 :
349 19 : mCRL2log(log::debug) << "Replaced assignment(s) " << data::pp(v) << " with assignment(s) " << data::pp(result) << std::endl;
350 :
351 38 : return data::assignment_list(result.begin(),result.end());
352 19 : }
353 :
354 : /// \brief Update an action summand with the new Boolean parameters
355 19 : void update_action_summand(action_summand& s)
356 : {
357 19 : s.condition() = data::replace_variables_capture_avoiding(s.condition(), m_if_trees, m_if_trees_generator);
358 19 : s.multi_action()=lps::replace_variables_capture_avoiding(s.multi_action(), m_if_trees, m_if_trees_generator);
359 19 : s.assignments() = replace_enumerated_parameters_in_assignments(s.assignments());
360 19 : }
361 :
362 : /// \brief Update an action summand with the new Boolean parameters
363 : void update_action_summand(stochastic_action_summand& s)
364 : {
365 : update_action_summand(static_cast<action_summand&>(s));
366 : s.distribution() = lps::replace_variables_capture_avoiding(s.distribution(), m_if_trees, m_if_trees_generator);
367 : }
368 :
369 : /// \brief Update a deadlock summand with the new Boolean parameters
370 2 : void update_deadlock_summand(deadlock_summand& s)
371 : {
372 2 : s.condition() = data::replace_variables_capture_avoiding(s.condition(), m_if_trees, m_if_trees_generator);
373 2 : lps::replace_variables_capture_avoiding(s.deadlock(), m_if_trees, m_if_trees_generator);
374 2 : }
375 :
376 9 : process_initializer update_initial_process(const data::variable_list& parameters, const process_initializer& init)
377 : {
378 9 : return process_initializer(replace_enumerated_parameters_in_initial_expressions(parameters, init.expressions()));
379 : }
380 :
381 0 : stochastic_process_initializer update_initial_process(const data::variable_list& parameters, const stochastic_process_initializer& init)
382 : {
383 : /* return stochastic_process_initializer(replace_enumerated_parameters_in_initial_expressions(parameters, init.expressions()),
384 : lps::replace_variables_capture_avoiding(init.distribution(), m_if_trees, m_if_trees_generator)
385 : ); */
386 0 : data::data_expression_list d = replace_enumerated_parameters_in_initial_expressions(parameters, init.expressions());
387 0 : const stochastic_distribution dist = lps::replace_variables_capture_avoiding(init.distribution(), d, m_if_trees, m_if_trees_generator);
388 0 : return stochastic_process_initializer(d, dist);
389 0 : }
390 :
391 : public:
392 : /// \brief Constructor for binary algorithm
393 : /// \param spec Specification to which the algorithm should be applied
394 : /// \param r a rewriter for data
395 9 : binary_algorithm(Specification& spec,
396 : DataRewriter& r,
397 : const std::string parameter_selection = "")
398 : : detail::lps_algorithm<Specification>(spec),
399 9 : m_rewriter(r),
400 18 : m_parameter_selection(parameter_selection)
401 9 : {}
402 :
403 : /// \brief Apply the algorithm to the specification passed in the
404 : /// constructor
405 9 : void run()
406 : {
407 9 : data::variable_list old_parameters = m_spec.process().process_parameters();
408 9 : const std::set<data::variable> to_replace = select_parameters(m_parameter_selection);
409 9 : replace_enumerated_parameters(to_replace);
410 :
411 : // Initial process
412 9 : mCRL2log(log::debug) << "Updating process initializer" << std::endl;
413 9 : m_spec.initial_process() = update_initial_process(old_parameters, m_spec.initial_process());
414 :
415 : // Summands
416 9 : mCRL2log(log::debug) << "Updating summands" << std::endl;
417 :
418 28 : for (action_summand& a: m_spec.process().action_summands())
419 : {
420 19 : update_action_summand(a);
421 : }
422 :
423 11 : for (deadlock_summand& d: m_spec.process().deadlock_summands())
424 : {
425 2 : update_deadlock_summand(d);
426 : }
427 9 : }
428 : };
429 :
430 : } // namespace lps
431 :
432 : } // namespace mcrl2
433 :
434 : #endif // MCRL2_LPS_BINARY_H
|
