Line data Source code
1 : // Author(s): Wieger Wesselink; Alexander van Dam
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/pbesinst_finite_algorithm.h
10 : /// \brief add your file description here.
11 :
12 : #ifndef MCRL2_PBES_PBESINST_FINITE_ALGORITHM_H
13 : #define MCRL2_PBES_PBESINST_FINITE_ALGORITHM_H
14 :
15 : #include "mcrl2/data/consistency.h"
16 : #include "mcrl2/data/enumerator.h"
17 : #include "mcrl2/data/replace.h"
18 : #include "mcrl2/pbes/algorithms.h"
19 : #include "mcrl2/pbes/detail/pbes_parameter_map.h"
20 : #include "mcrl2/pbes/join.h"
21 : #include "mcrl2/pbes/rewriters/data_rewriter.h"
22 :
23 : namespace mcrl2
24 : {
25 :
26 : namespace pbes_system
27 : {
28 :
29 : /// \brief Data structure for storing the indices of the variables that should be expanded by the finite pbesinst algorithm.
30 : typedef std::map<core::identifier_string, std::vector<std::size_t>> pbesinst_index_map;
31 :
32 : /// \brief Data structure for storing the variables that should be expanded by the finite pbesinst algorithm.
33 : typedef std::map<core::identifier_string, std::vector<data::variable>> pbesinst_variable_map;
34 :
35 : /// \brief Function object for renaming a propositional variable instantiation
36 : struct pbesinst_finite_rename
37 : {
38 : protected:
39 : mutable std::unordered_map<propositional_variable_instantiation, core::identifier_string> m;
40 : mutable data::set_identifier_generator id_generator;
41 :
42 29 : core::identifier_string rename(const core::identifier_string& name, const data::data_expression_list& parameters) const
43 : {
44 29 : std::ostringstream out;
45 29 : out << std::string(name);
46 55 : for (const data::data_expression& param: parameters)
47 : {
48 26 : out << "_" << data::pp(param);
49 : }
50 87 : return core::identifier_string(out.str());
51 29 : }
52 :
53 : public:
54 : /// \brief Renames the propositional variable x.
55 122 : core::identifier_string operator()(const core::identifier_string& name, const data::data_expression_list& parameters) const
56 : {
57 122 : propositional_variable_instantiation P(name, parameters);
58 122 : auto i = m.find(P);
59 122 : if (i == m.end())
60 : {
61 29 : core::identifier_string dest = rename(name, parameters);
62 29 : if (id_generator.has_identifier(dest))
63 : {
64 0 : dest = id_generator(dest);
65 : }
66 : else
67 : {
68 29 : id_generator.add_identifier(dest);
69 : }
70 29 : m[P] = dest;
71 29 : return dest;
72 29 : }
73 : else
74 : {
75 93 : return i->second;
76 : }
77 122 : }
78 : };
79 :
80 : /// \brief Exception that is used to signal an empty parameter selection
81 : struct empty_parameter_selection: public mcrl2::runtime_error
82 : {
83 0 : explicit empty_parameter_selection(const std::string& msg)
84 0 : : mcrl2::runtime_error(msg)
85 0 : {}
86 : };
87 :
88 : namespace detail
89 : {
90 :
91 : /// \brief Computes the subset with variables of finite sort and infinite.
92 : /// \param X A propositional variable instantiation
93 : /// \param index_map a container storing the indices of the variables that
94 : /// should be expanded by the finite pbesinst algorithm.
95 : /// \param finite A sequence of data expressions
96 : /// \param infinite A sequence of data expressions
97 : template <typename PropositionalVariable, typename Parameter>
98 76 : void split_parameters(const PropositionalVariable& X,
99 : const pbesinst_index_map& index_map,
100 : std::vector<Parameter>& finite,
101 : std::vector<Parameter>& infinite
102 : )
103 : {
104 76 : auto pi = index_map.find(X.name());
105 76 : assert(pi != index_map.end());
106 76 : const std::vector<std::size_t>& v = pi->second;
107 76 : auto i = X.parameters().begin();
108 76 : std::size_t index = 0;
109 76 : auto j = v.begin();
110 172 : for (; i != X.parameters().end(); ++i, ++index)
111 : {
112 96 : if (j != v.end() && index == *j)
113 : {
114 57 : finite.push_back(*i);
115 57 : ++j;
116 : }
117 : else
118 : {
119 39 : infinite.push_back(*i);
120 : }
121 : }
122 76 : }
123 :
124 : /// \brief Visitor that applies a propositional variable substitution to a pbes expression.
125 : template <typename DataRewriter, typename SubstitutionFunction>
126 : struct pbesinst_finite_builder: public pbes_system::detail::data_rewriter_builder<pbesinst_finite_builder<DataRewriter, SubstitutionFunction>, DataRewriter, SubstitutionFunction>
127 : {
128 : typedef pbes_system::detail::data_rewriter_builder<pbesinst_finite_builder, DataRewriter, SubstitutionFunction> super;
129 : using super::apply;
130 : using super::sigma;
131 :
132 : const pbesinst_finite_rename& m_rename;
133 : const data::data_specification& m_data_spec;
134 : const pbesinst_index_map& m_index_map;
135 : const pbesinst_variable_map& m_variable_map;
136 :
137 40 : pbesinst_finite_builder(const DataRewriter& R,
138 : SubstitutionFunction& sigma,
139 : const pbesinst_finite_rename& rho,
140 : const data::data_specification& data_spec,
141 : const pbesinst_index_map& index_map,
142 : const pbesinst_variable_map& variable_map
143 : )
144 : : super(R, sigma),
145 40 : m_rename(rho),
146 40 : m_data_spec(data_spec),
147 40 : m_index_map(index_map),
148 40 : m_variable_map(variable_map)
149 40 : {}
150 :
151 0 : std::string print_parameters(const std::vector<data::data_expression>& finite_parameters,
152 : const std::vector<data::data_expression>& infinite_parameters
153 : ) const
154 : {
155 0 : std::ostringstream out;
156 0 : out << "<finite>";
157 0 : for (const data::data_expression& e: finite_parameters)
158 : {
159 0 : out << e << " ";
160 : }
161 0 : out << "<infinite>";
162 0 : for (const data::data_expression& e: infinite_parameters)
163 : {
164 0 : out << e << " ";
165 : }
166 0 : out << std::endl;
167 0 : return out.str();
168 0 : }
169 :
170 : /// \brief Computes the condition 'for all i: variables[i] == expressions[i]'.
171 : template <typename VariableContainer, typename ExpressionContainer>
172 82 : data::data_expression make_condition(const VariableContainer& variables, const ExpressionContainer& expressions) const
173 : {
174 82 : assert(variables.size() == expressions.size());
175 82 : if (variables.empty())
176 : {
177 16 : return data::true_();
178 : }
179 66 : auto vi = variables.begin();
180 66 : auto ei = expressions.begin();
181 66 : data::data_expression result = data::equal_to(*vi, *ei);
182 66 : ++vi;
183 66 : ++ei;
184 66 : for (; vi != variables.end(); ++vi, ++ei)
185 : {
186 0 : result = data::and_(result, data::equal_to(*vi, *ei));
187 : }
188 66 : return result;
189 66 : }
190 :
191 : template <typename DataExpressionContainer>
192 22 : data::data_expression_list rewrite_container(const DataExpressionContainer& v, const data::rewriter& rewr)
193 : {
194 41 : return data::data_expression_list(v.begin(), v.end(), [&](const data::data_expression& x) { return rewr(x); });
195 : }
196 :
197 : template <typename DataExpressionContainer>
198 164 : data::data_expression_list rewrite_container(const DataExpressionContainer& v, const data::rewriter& rewr, const data::mutable_indexed_substitution<>& sigma)
199 : {
200 270 : return data::data_expression_list(v.begin(), v.end(), [&](const data::data_expression& x) { return rewr(x, sigma); });
201 : }
202 :
203 : template <class T>
204 49 : void apply(T& result, const propositional_variable_instantiation& x)
205 : {
206 : typedef data::enumerator_list_element_with_substitution<> enumerator_element;
207 :
208 : // TODO: this code contains too much conversion between vectors and aterm lists
209 49 : std::vector<data::data_expression> finite_parameters;
210 49 : std::vector<data::data_expression> infinite_parameters;
211 49 : split_parameters(x, m_index_map, finite_parameters, infinite_parameters);
212 49 : mCRL2log(log::debug) << print_parameters(finite_parameters, infinite_parameters);
213 49 : data::data_expression_list d(finite_parameters.begin(), finite_parameters.end());
214 49 : data::data_expression_list e(infinite_parameters.begin(), infinite_parameters.end());
215 49 : const core::identifier_string& Xi = x.name();
216 : // x = Xi(d,e)
217 :
218 49 : auto vi = m_variable_map.find(Xi);
219 49 : std::vector<data::variable> di;
220 49 : if (vi != m_variable_map.end())
221 : {
222 33 : di = vi->second;
223 : }
224 :
225 49 : std::set<pbes_expression> result_set;
226 49 : bool accept_solutions_with_variables = false;
227 98 : data::enumerator_identifier_generator id_generator;
228 49 : data::enumerator_algorithm<> E(super::R, m_data_spec, super::R, id_generator, accept_solutions_with_variables);
229 49 : const data::variable_list di_list(di.begin(), di.end());
230 49 : data::mutable_indexed_substitution<> local_sigma;
231 49 : E.enumerate(enumerator_element(di_list, data::true_()),
232 : local_sigma,
233 656 : [&](const enumerator_element& p) {
234 82 : data::mutable_indexed_substitution<> sigma_i;
235 82 : p.add_assignments(di_list, sigma_i, super::R);
236 82 : data::data_expression_list d_copy = rewrite_container(d, super::R, sigma);
237 82 : data::data_expression_list e_copy = rewrite_container(e, super::R, sigma);
238 82 : data::data_expression_list di_copy = atermpp::container_cast<data::data_expression_list>(di_list);
239 82 : di_copy = data::replace_free_variables(di_copy, sigma_i);
240 82 : data::data_expression c = make_condition(di_copy, d_copy);
241 82 : core::identifier_string Y = m_rename(Xi, di_copy);
242 82 : result_set.insert(and_(c, propositional_variable_instantiation(Y, e_copy)));
243 82 : return false;
244 82 : }
245 : );
246 49 : result = join_or(result_set.begin(), result_set.end());
247 49 : }
248 :
249 : /// \return Visits the initial state
250 11 : propositional_variable_instantiation visit_initial_state(const propositional_variable_instantiation& init)
251 : {
252 11 : std::vector<data::data_expression> finite_parameters_vector;
253 11 : std::vector<data::data_expression> infinite_parameters_vector;
254 11 : split_parameters(init, m_index_map, finite_parameters_vector, infinite_parameters_vector);
255 :
256 11 : data::data_expression_list finite_parameters = rewrite_container(finite_parameters_vector, super::R);
257 11 : data::data_expression_list infinite_parameters = rewrite_container(infinite_parameters_vector, super::R);
258 11 : core::identifier_string X = m_rename(init.name(), finite_parameters);
259 22 : return propositional_variable_instantiation(X, infinite_parameters);
260 11 : }
261 : };
262 :
263 : } // namespace detail
264 :
265 : /// \brief Algorithm class for the finite pbesinst algorithm.
266 : class pbesinst_finite_algorithm
267 : {
268 : protected:
269 : /// \brief The strategy of the data rewriter.
270 : data::rewriter::strategy m_rewriter_strategy;
271 :
272 : /// \brief The number of generated equations.
273 : std::size_t m_equation_count = 0;
274 :
275 : /// \brief Identifier generator for the enumerator
276 : data::enumerator_identifier_generator m_id_generator;
277 :
278 : /// \brief Returns true if the container contains the given element
279 11 : void compute_index_map(const std::vector<pbes_equation>& equations,
280 : const pbesinst_variable_map& variable_map,
281 : pbesinst_index_map& index_map)
282 : {
283 : using utilities::detail::contains;
284 27 : for (const pbes_equation& eqn: equations)
285 : {
286 16 : const core::identifier_string& name = eqn.variable().name();
287 16 : const data::variable_list& parameters = eqn.variable().parameters();
288 :
289 16 : std::vector<std::size_t> v;
290 16 : auto j = variable_map.find(name);
291 16 : if (j != variable_map.end())
292 : {
293 13 : std::size_t index = 0;
294 34 : for (auto k = parameters.begin(); k != parameters.end(); ++k, ++index)
295 : {
296 21 : if (contains(j->second, *k))
297 : {
298 13 : v.push_back(index);
299 : }
300 : }
301 : }
302 16 : index_map[name] = v;
303 16 : }
304 11 : }
305 :
306 : /// \brief Prints a message for every 1000-th equation
307 0 : std::string print_equation_count(std::size_t size) const
308 : {
309 0 : if (size > 0 && size % 1000 == 0)
310 : {
311 0 : std::ostringstream out;
312 0 : out << "Generated " << size << " BES equations" << std::endl;
313 0 : return out.str();
314 0 : }
315 0 : return "";
316 : }
317 :
318 : public:
319 :
320 : /// \brief Constructor.
321 : /// \param rewriter_strategy Strategy to be used for the data rewriter.
322 11 : explicit pbesinst_finite_algorithm(data::rewriter::strategy rewriter_strategy = data::jitty)
323 11 : : m_rewriter_strategy(rewriter_strategy)
324 11 : {}
325 :
326 : /// \brief Runs the algorithm.
327 : /// \param pbesspec A PBES
328 : /// \param variable_map A map containing the finite parameters that should be expanded by the algorithm.
329 11 : void run(pbes& pbesspec, const pbesinst_variable_map& variable_map)
330 : {
331 11 : pbes_system::algorithms::instantiate_global_variables(pbesspec);
332 11 : pbesinst_finite_rename rename;
333 11 : m_equation_count = 0;
334 :
335 : // compute index map corresponding to the variable map
336 11 : pbesinst_index_map index_map;
337 11 : compute_index_map(pbesspec.equations(), variable_map, index_map);
338 :
339 11 : data::rewriter rewr(pbesspec.data(), m_rewriter_strategy);
340 :
341 : // compute new equations
342 11 : std::vector<pbes_equation> equations;
343 27 : for (const pbes_equation& eqn: pbesspec.equations())
344 : {
345 16 : std::vector<data::variable> finite_parameters;
346 16 : std::vector<data::variable> infinite_parameters;
347 16 : detail::split_parameters(eqn.variable(), index_map, finite_parameters, infinite_parameters);
348 16 : data::variable_list infinite(infinite_parameters.begin(), infinite_parameters.end());
349 :
350 : typedef data::enumerator_list_element_with_substitution<> enumerator_element;
351 16 : bool accept_solutions_with_variables = false;
352 16 : data::enumerator_algorithm<> E(rewr, pbesspec.data(), rewr, m_id_generator, accept_solutions_with_variables);
353 16 : data::variable_list finite_parameter_list(finite_parameters.begin(), finite_parameters.end());
354 16 : data::mutable_indexed_substitution<> sigma;
355 16 : E.enumerate(enumerator_element(finite_parameter_list, data::true_()),
356 : sigma,
357 29 : [&](const enumerator_element& p) {
358 29 : data::mutable_indexed_substitution<> sigma_j;
359 29 : p.add_assignments(finite_parameter_list, sigma_j, rewr);
360 29 : std::vector<data::data_expression> finite;
361 55 : for (const data::variable& v: finite_parameters)
362 : {
363 26 : finite.push_back(sigma_j(v));
364 : }
365 29 : core::identifier_string name = rename(eqn.variable().name(), data::data_expression_list(finite.begin(), finite.end()));
366 29 : propositional_variable X(name, infinite);
367 29 : detail::pbesinst_finite_builder<data::rewriter, data::mutable_indexed_substitution<>> visitor(rewr, sigma_j, rename, pbesspec.data(), index_map, variable_map);
368 29 : pbes_expression formula;
369 29 : visitor.apply(formula, eqn.formula());
370 29 : equations.emplace_back(eqn.symbol(), X, formula);
371 29 : mCRL2log(log::debug) << print_equation_count(++m_equation_count);
372 29 : mCRL2log(log::debug) << "Added equation " << pbes_system::pp(eqn) << "\n";
373 29 : return false;
374 29 : }
375 : );
376 16 : }
377 :
378 : // compute new initial state
379 : data::no_substitution sigma;
380 11 : detail::pbesinst_finite_builder<data::rewriter, data::no_substitution> visitor(rewr, sigma, rename, pbesspec.data(), index_map, variable_map);
381 11 : propositional_variable_instantiation initial_state = visitor.visit_initial_state(pbesspec.initial_state());
382 :
383 : // assign the result
384 11 : pbesspec.equations() = equations;
385 11 : pbesspec.initial_state() = initial_state;
386 11 : }
387 :
388 : /// \brief Runs the algorithm.
389 : /// \param p A PBES
390 9 : void run(pbes& p)
391 : {
392 : // put all finite variables in a variable map
393 9 : pbesinst_variable_map variable_map;
394 23 : for (const pbes_equation& eqn: p.equations())
395 : {
396 33 : for (const data::variable& v: eqn.variable().parameters())
397 : {
398 19 : if (p.data().is_certainly_finite(v.sort()))
399 : {
400 11 : variable_map[eqn.variable().name()].push_back(v);
401 : }
402 : }
403 : }
404 :
405 9 : run(p, variable_map);
406 9 : }
407 : };
408 :
409 : inline
410 0 : void pbesinst_finite(pbes& p, data::rewrite_strategy rewrite_strategy, const std::string& finite_parameter_selection)
411 : {
412 0 : if (finite_parameter_selection.empty())
413 : {
414 0 : throw empty_parameter_selection("no finite parameters were selected!");
415 : }
416 0 : pbesinst_finite_algorithm algorithm(rewrite_strategy);
417 0 : pbes_system::detail::pbes_parameter_map parameter_map = pbes_system::detail::parse_pbes_parameter_map(p, finite_parameter_selection);
418 :
419 0 : bool is_empty = true;
420 0 : for (auto& i: parameter_map)
421 : {
422 0 : if (!((i.second).empty()))
423 : {
424 0 : is_empty = false;
425 0 : break;
426 : }
427 : }
428 0 : if (is_empty)
429 : {
430 0 : mCRL2log(log::verbose) << "Warning: no parameters were found that match the string \"" + finite_parameter_selection + "\"" << std::endl;
431 : }
432 : else
433 : {
434 0 : algorithm.run(p, parameter_map);
435 : }
436 0 : }
437 :
438 : } // namespace pbes_system
439 :
440 : } // namespace mcrl2
441 :
442 : #endif // MCRL2_PBES_PBESINST_FINITE_ALGORITHM_H
|
