Line data Source code
1 : // Author(s): Jeroen Keiren, 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 data_specification_test.cpp
10 : /// \brief Basic regression test for data specifications.
11 :
12 : #define BOOST_TEST_MODULE data_specification_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/data_io.h"
16 : #include "mcrl2/data/merge_data_specifications.h"
17 : #include "mcrl2/data/parse.h"
18 : #include "mcrl2/data/print.h"
19 :
20 : using namespace mcrl2;
21 : using namespace mcrl2::data;
22 :
23 : template <typename Container1, typename Container2>
24 : bool equal_content(Container1 const& c1, Container2 const& c2)
25 : {
26 : std::set<typename Container1::value_type> s1(c1.begin(), c1.end());
27 : std::set<typename Container2::value_type> s2(c2.begin(), c2.end());
28 :
29 : if (s1 != s2)
30 : {
31 : std::clog << "+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++" << std::endl
32 : << "Detailed comparison:" << std::endl;
33 : std::clog << data::pp(c1) << std::endl;
34 : std::clog << data::pp(c2) << std::endl;
35 : }
36 : return s1 == s2;
37 : }
38 :
39 15 : bool detailed_compare_for_equality(data_specification const& left, data_specification const& right)
40 : {
41 15 : std::set<sort_expression> left_sorts(left.sorts().begin(), left.sorts().end());
42 15 : std::set<sort_expression> right_sorts(right.sorts().begin(), right.sorts().end());
43 15 : BOOST_CHECK(left_sorts == right_sorts);
44 :
45 15 : std::set<data::function_symbol> left_constructors(left.constructors().begin(), left.constructors().end());
46 15 : std::set<data::function_symbol> right_constructors(right.constructors().begin(), right.constructors().end());
47 15 : BOOST_CHECK(left_constructors == right_constructors);
48 :
49 15 : std::set<data::function_symbol> left_mappings(left.mappings().begin(), left.mappings().end());
50 15 : std::set<data::function_symbol> right_mappings(right.mappings().begin(), right.mappings().end());
51 15 : BOOST_CHECK(left_mappings == right_mappings);
52 :
53 15 : BOOST_CHECK(left.equations() == right.equations());
54 :
55 15 : if (/*(left_aliases != right_aliases)*/
56 15 : (left_sorts != right_sorts)
57 15 : || (left_constructors != right_constructors)
58 15 : || (left_mappings != right_mappings)
59 30 : || (left.equations() != right.equations()))
60 : {
61 0 : std::clog << "+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++" << std::endl
62 0 : << "Specification detailed comparison:" << std::endl;
63 :
64 : /*
65 : if (left_aliases != right_aliases)
66 : {
67 : std::clog << "Aliases (left) " << data::pp(left.aliases()) << std::endl;
68 : std::clog << "Aliases (right) " << data::pp(right.aliases()) << std::endl;
69 : }*/
70 0 : if (left_sorts != right_sorts)
71 : {
72 0 : std::clog << "Sorts (left) " << data::pp(left.sorts()) << std::endl;
73 0 : std::clog << "Sorts (right) " << data::pp(right.sorts()) << std::endl;
74 : }
75 0 : if (left_constructors != right_constructors)
76 : {
77 0 : std::clog << "Constructors (left) " << data::pp(left.constructors()) << std::endl;
78 0 : std::clog << "Constructors (right) " << data::pp(right.constructors()) << std::endl;
79 : }
80 0 : if (left_mappings != right_mappings)
81 : {
82 0 : std::clog << "Mappings (left) " << data::pp(left.mappings()) << std::endl;
83 0 : std::clog << "Mappings (right) " << data::pp(right.mappings()) << std::endl;
84 : }
85 0 : if (left.equations() != right.equations())
86 : {
87 0 : std::clog << "Equations (left) " << data::pp(left.equations()) << std::endl;
88 0 : std::clog << "Equations (right) " << data::pp(right.equations()) << std::endl;
89 : }
90 :
91 0 : std::clog << "+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++" << std::endl;
92 :
93 0 : return false;
94 : }
95 15 : return true;
96 15 : }
97 :
98 15 : bool compare_for_equality(data_specification const& left, data_specification const& right)
99 : {
100 15 : return detailed_compare_for_equality(left, right);
101 : }
102 :
103 1 : void test_sorts()
104 : {
105 1 : std::clog << "test_sorts" << std::endl;
106 :
107 2 : basic_sort s("S");
108 2 : basic_sort s0("S0");
109 2 : alias s1(s,basic_sort("S1"));
110 :
111 1 : std::vector< sort_expression > sl;
112 1 : sl.push_back(basic_sort("S1"));
113 1 : sl.push_back(s0);
114 :
115 1 : data_specification spec;
116 1 : spec.add_sort(s);
117 1 : spec.add_sort(s0);
118 1 : spec.add_alias(s1);
119 1 : data_specification spec1;
120 1 : spec1.add_alias(s1);
121 1 : spec1.add_sort(s0);
122 1 : spec1.add_sort(s);
123 :
124 : //BOOST_CHECK(equal_content(sl, spec.user_defined_sorts()));
125 : //BOOST_CHECK(equal_content(sl, spec1.user_defined_sorts()));
126 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
127 :
128 2 : basic_sort s2("S2");
129 3 : sort_expression_vector s2l {s2};
130 1 : spec.add_context_sort(s2);
131 1 : spec1.add_context_sorts(s2l);
132 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
133 :
134 2 : std::for_each(s2l.begin(), s2l.end(), [&spec](const sort_expression& s){ spec.remove_sort(s); });
135 1 : spec1.remove_sort(s2);
136 1 : compare_for_equality(spec, spec1);
137 1 : }
138 :
139 0 : void test_aliases()
140 : {
141 0 : std::clog << "test_aliases" << std::endl;
142 :
143 0 : basic_sort s("S");
144 0 : basic_sort t("T");
145 0 : alias s1(basic_sort("S1"), s);
146 0 : alias s2(basic_sort("S2"), s);
147 :
148 0 : data_specification spec;
149 :
150 : // BOOST_CHECK(spec.aliases().size()) == 0);
151 :
152 0 : std::set<basic_sort> sorts = { s, t };
153 0 : std::for_each(sorts.begin(), sorts.end(), [&spec](const basic_sort& s){ spec.add_sort(s); });
154 :
155 : /* std::set< sort_expression > aliases;
156 : aliases.insert(s1);
157 : aliases.insert(s2);
158 : spec.add_aliases(aliases);
159 :
160 : BOOST_CHECK(spec.aliases(s).size()) == 2);
161 : BOOST_CHECK(spec.aliases(t).size()) == 0);
162 : BOOST_CHECK(spec.aliases(s) == aliases); */
163 0 : }
164 :
165 1 : void test_constructors()
166 : {
167 1 : std::clog << "test_constructors" << std::endl;
168 :
169 2 : basic_sort s("S");
170 2 : basic_sort s0("S0");
171 3 : function_sort s0s(sort_expression_list({s0}),s);
172 2 : data::function_symbol f("f", s);
173 2 : data::function_symbol g("g", s0s);
174 2 : data::function_symbol h("h", s0);
175 4 : function_symbol_vector fgl {f,g};
176 3 : function_symbol_vector hl {h};
177 5 : function_symbol_vector fghl {f,g,h};
178 :
179 1 : data_specification spec;
180 1 : spec.add_sort(s);
181 1 : spec.add_sort(s0);
182 :
183 1 : spec.add_constructor(f);
184 1 : spec.add_constructor(g);
185 1 : spec.add_constructor(h);
186 :
187 1 : data_specification spec1(spec);
188 4 : std::for_each(fghl.begin(), fghl.end(), [&spec1](const function_symbol& f){ spec1.add_constructor(f); });
189 :
190 1 : function_symbol_vector constructors(spec.constructors());
191 1 : BOOST_CHECK(spec.constructors(s) == fgl);
192 1 : BOOST_CHECK(constructors.size() == 7); // f,g,h, true, false.
193 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), f) != constructors.end());
194 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), g) != constructors.end());
195 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), h) != constructors.end());
196 :
197 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
198 1 : BOOST_CHECK(spec.constructors() == spec1.constructors());
199 1 : BOOST_CHECK(spec.constructors(s) == fgl);
200 1 : BOOST_CHECK(spec.constructors(s0) == hl);
201 1 : BOOST_CHECK(spec1.constructors(s) == fgl);
202 1 : BOOST_CHECK(spec1.constructors(s0) == hl);
203 1 : spec.add_constructor(data::function_symbol("i", s0));
204 2 : data::function_symbol i("i", s0);
205 1 : spec.remove_constructor(i);
206 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
207 :
208 1 : spec.add_constructor(i);
209 3 : function_symbol_vector il {i};
210 2 : std::for_each(il.begin(), il.end(), [&spec1](const function_symbol& f){ spec1.add_constructor(f); });
211 :
212 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
213 :
214 1 : spec.remove_constructor(i);
215 2 : std::for_each(il.begin(), il.end(), [&spec1](const function_symbol& f){ spec1.remove_constructor(f); });
216 :
217 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
218 1 : }
219 :
220 1 : void test_functions()
221 : {
222 1 : std::clog << "test_functions" << std::endl;
223 :
224 2 : basic_sort s("S");
225 2 : basic_sort s0("S0");
226 3 : function_sort s0s(sort_expression_list({s0}), s);
227 2 : data::function_symbol f("f", s);
228 2 : data::function_symbol g("g", s0s);
229 2 : data::function_symbol h("h", s0);
230 :
231 4 : function_symbol_vector fgl {f,g};
232 3 : function_symbol_vector hl {h};
233 5 : function_symbol_vector fghl {f,g,h};
234 :
235 1 : data_specification spec;
236 1 : spec.add_sort(s);
237 1 : spec.add_sort(s0);
238 1 : spec.add_mapping(f);
239 1 : spec.add_mapping(g);
240 1 : spec.add_mapping(h);
241 :
242 1 : data_specification spec1(spec);
243 4 : std::for_each(fghl.begin(), fghl.end(), [&spec1](const function_symbol& f){ spec1.add_mapping(f); } );
244 :
245 1 : std::cerr << "#mappings " << spec.mappings().size() << "\n";
246 1 : BOOST_CHECK(spec.mappings().size() == 54);
247 :
248 1 : function_symbol_vector mappings(spec.mappings());
249 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), f) != mappings.end());
250 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), g) != mappings.end());
251 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), h) != mappings.end());
252 :
253 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
254 1 : BOOST_CHECK(spec.mappings(s).size() == 3);
255 1 : BOOST_CHECK(std::find(spec.mappings(s).begin(), spec.mappings(s).end(), f) != spec.mappings(s).end());
256 1 : BOOST_CHECK(std::find(spec.mappings(s).begin(), spec.mappings(s).end(), g) != spec.mappings(s).end());
257 1 : BOOST_CHECK(std::find(spec.mappings(s0).begin(), spec.mappings(s0).end(), h) != spec.mappings(s0).end());
258 1 : BOOST_CHECK(spec1.mappings(s).size() == 3);
259 1 : BOOST_CHECK(std::find(spec1.mappings(s).begin(), spec1.mappings(s).end(), f) != spec1.mappings(s).end());
260 1 : BOOST_CHECK(std::find(spec1.mappings(s).begin(), spec1.mappings(s).end(), g) != spec1.mappings(s).end());
261 1 : BOOST_CHECK(std::find(spec1.mappings(s0).begin(), spec1.mappings(s0).end(), h) != spec1.mappings(s0).end());
262 :
263 2 : data::function_symbol i("i", s0);
264 1 : spec.add_mapping(i);
265 3 : function_symbol_vector il {i};
266 2 : std::for_each(il.begin(), il.end(), [&spec1](const function_symbol& f){ spec1.add_mapping(f); });
267 1 : compare_for_equality(spec, spec1);
268 :
269 2 : std::for_each(il.begin(), il.end(), [&spec](const function_symbol& f){ spec.remove_mapping(f); });
270 1 : spec1.remove_mapping(i);
271 1 : compare_for_equality(spec, spec1);
272 1 : }
273 :
274 1 : void test_equations()
275 : {
276 1 : std::clog << "test_equations" << std::endl;
277 2 : basic_sort s("S");
278 2 : basic_sort s0("S0");
279 3 : function_sort s0s(sort_expression_list({s0}), s);
280 2 : data::function_symbol f("f", s0s);
281 2 : variable x("x", s0);
282 3 : data_expression_vector xel {x};
283 1 : application fx(f, xel.begin(), xel.end());
284 3 : variable_vector xl {x};
285 1 : data_equation fxx(xl, x, fx, x);
286 :
287 1 : data_specification spec;
288 1 : data_specification spec1;
289 1 : spec.add_sort(s);
290 1 : spec.add_sort(s0);
291 :
292 1 : spec1 = spec;
293 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
294 1 : spec.add_equation(fxx);
295 3 : data_equation_vector fxxl {fxx};
296 2 : std::for_each(fxxl.begin(), fxxl.end(), [&spec1](const data_equation& eqn){ spec1.add_equation(eqn); });
297 :
298 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
299 :
300 1 : data_equation fxf(xl, x, fx, f);
301 3 : data_equation_vector fxfl {fxf};
302 1 : spec.add_equation(fxf);
303 2 : std::for_each(fxfl.begin(), fxfl.end(), [&spec1](const data_equation& eqn){ spec1.add_equation(eqn); });
304 :
305 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
306 :
307 1 : data_equation_vector result = find_equations(spec, f);
308 1 : BOOST_CHECK(result.size() == 2);
309 1 : BOOST_CHECK(std::find(result.begin(), result.end(), fxf) != result.end());
310 1 : BOOST_CHECK(std::find(result.begin(), result.end(), fxx) != result.end());
311 2 : std::for_each(fxfl.begin(), fxfl.end(), [&spec](const data_equation& eqn){ spec.remove_equation(eqn); });
312 1 : spec1.remove_equation(fxf);
313 1 : BOOST_CHECK(compare_for_equality(spec, spec1));
314 1 : }
315 :
316 1 : void test_is_certainly_finite()
317 : {
318 1 : std::clog << "test_is_certainly_finite" << std::endl;
319 2 : basic_sort s("S");
320 2 : basic_sort s0("S0");
321 3 : function_sort s0s0(sort_expression_list({s0}), s0);
322 2 : data::function_symbol f("f", s);
323 2 : data::function_symbol g("g", s0s0);
324 2 : variable x("x", s0);
325 1 : application gx(g, x);
326 1 : data_specification spec;
327 1 : spec.add_sort(s);
328 1 : spec.add_sort(s0);
329 1 : spec.add_constructor(f);
330 1 : spec.add_constructor(g);
331 :
332 1 : BOOST_CHECK(spec.is_certainly_finite(s));
333 1 : BOOST_CHECK(!spec.is_certainly_finite(s0));
334 :
335 1 : spec.add_context_sort(sort_real::real_());
336 1 : BOOST_CHECK(spec.is_certainly_finite(sort_bool::bool_()));
337 1 : BOOST_CHECK(!spec.is_certainly_finite(sort_pos::pos()));
338 1 : BOOST_CHECK(!spec.is_certainly_finite(sort_nat::nat()));
339 1 : BOOST_CHECK(!spec.is_certainly_finite(sort_int::int_()));
340 1 : BOOST_CHECK(!spec.is_certainly_finite(sort_real::real_()));
341 :
342 2 : basic_sort s1("S1");
343 2 : basic_sort s2("S2");
344 1 : spec.add_constructor(data::function_symbol("h", make_function_sort_(s1, s2)));
345 1 : spec.add_constructor(data::function_symbol("i", make_function_sort_(s2, s1)));
346 :
347 1 : spec.add_alias(alias(basic_sort("a"), s));
348 1 : spec.add_alias(alias(basic_sort("a0"), s0));
349 1 : spec.add_alias(alias(basic_sort("a1"), s1));
350 :
351 1 : BOOST_CHECK(spec.is_certainly_finite(normalize_sorts(basic_sort("a"),spec)));
352 1 : BOOST_CHECK(!spec.is_certainly_finite(normalize_sorts(basic_sort("a0"),spec)));
353 1 : BOOST_CHECK(!spec.is_certainly_finite(normalize_sorts(basic_sort("a1"),spec)));
354 :
355 : using namespace sort_list;
356 :
357 1 : BOOST_CHECK(!spec.is_certainly_finite(list(s)));
358 1 : BOOST_CHECK(!spec.is_certainly_finite(list(s0)));
359 :
360 : using namespace sort_set;
361 :
362 1 : BOOST_CHECK(spec.is_certainly_finite(set_(s)));
363 1 : BOOST_CHECK(!spec.is_certainly_finite(set_(s0)));
364 1 : BOOST_CHECK(!spec.is_certainly_finite(normalize_sorts(set_(s0),spec)));
365 :
366 : using namespace sort_bag;
367 :
368 1 : BOOST_CHECK(!spec.is_certainly_finite(bag(s)));
369 1 : BOOST_CHECK(!spec.is_certainly_finite(bag(s0)));
370 1 : BOOST_CHECK(spec.is_certainly_finite(make_function_sort_(s,s)));
371 1 : BOOST_CHECK(!spec.is_certainly_finite(make_function_sort_(s,s0)));
372 1 : BOOST_CHECK(!spec.is_certainly_finite(make_function_sort_(s0,s)));
373 :
374 : // structured sort
375 : /* This test should be reconsidered, as it does not work in this way.
376 : * Having a test for structured sort is good.
377 :
378 : std::vector< data::structured_sort_constructor_argument > arguments;
379 :
380 : arguments.push_back(data::structured_sort_constructor_argument(s));
381 : arguments.push_back(data::structured_sort_constructor_argument(s0));
382 : arguments.push_back(data::structured_sort_constructor_argument(s1));
383 :
384 : std::vector< data::structured_sort_constructor > constructors;
385 : constructors.push_back(data::structured_sort_constructor("a", structured_sort_constructor_argument_list(arguments.begin(), arguments.begin() + 1)));
386 : constructors.push_back(data::structured_sort_constructor("b", structured_sort_constructor_argument_list(arguments.begin() + 1, arguments.begin() + 2)));
387 : constructors.push_back(data::structured_sort_constructor("b", structured_sort_constructor_argument_list(arguments.begin() + 2, arguments.begin() + 3)));
388 :
389 : structured_sort struct1(structured_sort_constructor_list(constructors.begin(), constructors.begin() + 1));
390 : structured_sort struct2(structured_sort_constructor_list(constructors.begin() + 1, constructors.begin() + 2));
391 : structured_sort struct3(structured_sort_constructor_list(constructors.begin() + 2, constructors.begin() + 3));
392 : structured_sort struct4(structured_sort_constructor_list(constructors.begin() + 0, constructors.begin() + 3));
393 : spec.add_sort(struct1); add_sort does not work on complex sorts, since 2/6/2015.
394 : spec.add_sort(struct2);
395 : spec.add_sort(struct3);
396 : spec.add_sort(struct4);
397 : BOOST_CHECK(spec.is_certainly_finite(struct1));
398 : BOOST_CHECK(!spec.is_certainly_finite(struct2));
399 : BOOST_CHECK(!spec.is_certainly_finite(struct3));
400 : BOOST_CHECK(!spec.is_certainly_finite(struct4)); */
401 1 : }
402 :
403 1 : void test_constructor()
404 : {
405 1 : std::clog << "test_constructor" << std::endl;
406 : std::string SPEC =
407 : "sort \n"
408 : " D = struct d1 | d2; \n"
409 : " Error = struct e; \n"
410 1 : " \n"
411 : ;
412 1 : data_specification data = parse_data_specification(SPEC);
413 1 : atermpp::aterm_appl a = data::detail::data_specification_to_aterm(data);
414 1 : data_specification spec1(a);
415 1 : }
416 :
417 : template < typename Container, typename Expression >
418 1 : bool search(Container const& container, Expression const& expression)
419 : {
420 1 : return std::find(container.begin(), container.end(), expression) != container.end();
421 : }
422 :
423 3 : bool search_alias(const alias_vector& v, const sort_expression& s)
424 : {
425 6 : for(const alias& a: v)
426 : {
427 6 : if(a.name() == s)
428 : {
429 3 : return true;
430 : }
431 : }
432 0 : return false;
433 : }
434 :
435 1 : void test_system_defined()
436 : {
437 1 : std::clog << "test_system_defined" << std::endl;
438 :
439 1 : data_specification specification;
440 :
441 1 : BOOST_CHECK(!specification.constructors(sort_bool::bool_()).empty());
442 :
443 2 : specification = parse_data_specification(
444 : "sort S;"
445 1 : "map f: Set(S);");
446 :
447 1 : BOOST_CHECK(search(specification.sorts(), sort_set::set_(basic_sort("S"))));
448 : // BOOST_CHECK(search(specification.sorts(), sort_fset::fset(basic_sort("S")))); MUST BE CHECKED ALSO?
449 :
450 2 : specification = parse_data_specification(
451 : "sort D = Set(Nat);"
452 : "sort E = D;"
453 1 : "sort F = E;");
454 1 : BOOST_CHECK(specification.constructors(::sort_set::set_(sort_nat::nat())) == specification.constructors(basic_sort("D")));
455 1 : BOOST_CHECK(specification.constructors(normalize_sorts(basic_sort("D"),specification)) ==
456 : specification.constructors(normalize_sorts(basic_sort("E"),specification)));
457 1 : BOOST_CHECK(specification.mappings(normalize_sorts(basic_sort("D"),specification)) ==
458 : specification.mappings(normalize_sorts(basic_sort("E"),specification)));
459 1 : BOOST_CHECK(specification.constructors(normalize_sorts(basic_sort("D"),specification)) ==
460 : specification.constructors(normalize_sorts(basic_sort("F"),specification)));
461 :
462 1 : data_specification copy = specification;
463 :
464 : // A data specification that is constructed using data_specification_to_aterm is assumed not
465 : // not be type checked. This must be indicated explicitly.
466 2 : data_specification specification1=data_specification(data::detail::data_specification_to_aterm(copy));
467 1 : BOOST_CHECK(compare_for_equality(specification1,specification));
468 :
469 2 : specification = parse_data_specification(
470 : "sort D = struct d(getBool : Bool)?is_d;"
471 : "sort E = D;"
472 1 : "sort F = E;");
473 :
474 1 : alias_vector aliases(specification.user_defined_aliases());
475 1 : BOOST_CHECK(search_alias(aliases, basic_sort("D")));
476 1 : BOOST_CHECK(search_alias(aliases, basic_sort("E")));
477 1 : BOOST_CHECK(search_alias(aliases, basic_sort("F")));
478 1 : BOOST_CHECK(specification.constructors(basic_sort("D")).size() == 1);
479 :
480 1 : BOOST_CHECK(specification.constructors(basic_sort("D")) == specification.constructors(basic_sort("E")));
481 1 : BOOST_CHECK(specification.mappings(basic_sort("D")) == specification.mappings(basic_sort("E")));
482 1 : BOOST_CHECK(specification.constructors(basic_sort("D")) == specification.constructors(basic_sort("F")));
483 :
484 : /* copy = specification;
485 : specification1=data_specification(data::detail::data_specification_to_aterm(copy));
486 : specification1.declare_data_specification_to_be_type_checked();
487 : BOOST_CHECK(compare_for_equality(specification1, specification)); */
488 :
489 : // Check for the non presence of function sort
490 1 : BOOST_CHECK(specification.mappings(make_function_sort_(basic_sort("D"), sort_bool::bool_())).empty());
491 :
492 1 : specification.add_mapping(data::function_symbol("f", make_function_sort_(sort_bool::bool_(), sort_bool::bool_(), sort_nat::nat())));
493 :
494 1 : BOOST_CHECK(!specification.mappings(make_function_sort_(sort_bool::bool_(), sort_bool::bool_(), sort_nat::nat())).empty());
495 :
496 : // Manually structured sort
497 1 : std::vector< data::structured_sort_constructor_argument > arguments;
498 :
499 : // sort that references itself by a name
500 1 : arguments.push_back(data::structured_sort_constructor_argument(basic_sort("Q")));
501 :
502 1 : std::vector< data::structured_sort_constructor > constructors;
503 1 : constructors.push_back(data::structured_sort_constructor("q",structured_sort_constructor_argument_list(arguments.begin(), arguments.begin() + 1)));
504 :
505 1 : specification.add_alias(alias(basic_sort("Q"), data::structured_sort(constructors)));
506 1 : }
507 :
508 1 : void test_utility_functionality()
509 : {
510 1 : data_specification spec;
511 :
512 2 : basic_sort s("S");
513 2 : basic_sort s0("S0");
514 2 : basic_sort a("a");
515 3 : function_sort s0s(sort_expression_list({s0}), s);
516 2 : data::function_symbol f("f", s);
517 :
518 2 : data::function_symbol g("g", s0s);
519 2 : data::function_symbol h("h", s0);
520 :
521 : {
522 1 : const std::set<sort_expression>& sorts(spec.sorts());
523 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), s0) == sorts.end());
524 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), s) == sorts.end());
525 1 : function_symbol_vector constructors(spec.constructors());
526 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), f) == constructors.end());
527 1 : function_symbol_vector mappings(spec.mappings());
528 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), f) == mappings.end());
529 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), g) == mappings.end());
530 1 : }
531 :
532 1 : spec.add_sort(s0);
533 1 : spec.add_constructor(f);
534 1 : spec.add_mapping(g);
535 :
536 : {
537 1 : const std::set<sort_expression>& sorts(spec.sorts());
538 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), s0) != sorts.end());
539 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), s) != sorts.end()); // Automatically added!
540 1 : function_symbol_vector constructors(spec.constructors());
541 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), f) != constructors.end());
542 1 : function_symbol_vector mappings(spec.mappings());
543 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), f) == mappings.end());
544 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), g) != mappings.end());
545 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), h) == mappings.end());
546 1 : }
547 1 : spec.add_mapping(h);
548 :
549 1 : spec.add_sort(s);
550 1 : spec.add_alias(alias(basic_sort("a"),s));
551 :
552 1 : const std::set<sort_expression> sorts(spec.sorts());
553 1 : function_symbol_vector constructors(spec.constructors());
554 1 : function_symbol_vector mappings(spec.mappings());
555 :
556 :
557 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), s0) != sorts.end());
558 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), normalize_sorts(a,spec)) != sorts.end());
559 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), s) != sorts.end());
560 :
561 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), f) == mappings.end());
562 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), f) != constructors.end());
563 :
564 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), g) == constructors.end());
565 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), g) != mappings.end());
566 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), g) == constructors.end());
567 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), h) == constructors.end());
568 1 : BOOST_CHECK(std::find(mappings.begin(), mappings.end(), h) != mappings.end());
569 1 : BOOST_CHECK(spec.constructors(a) == spec.constructors(s));
570 1 : BOOST_CHECK(spec.mappings(a) == spec.mappings(s));
571 1 : }
572 :
573 1 : void test_normalisation()
574 : {
575 : using namespace mcrl2::data;
576 : using namespace mcrl2::data::sort_list;
577 : using namespace mcrl2::data::sort_set;
578 : using namespace mcrl2::data::sort_bag;
579 :
580 1 : data_specification specification;
581 :
582 2 : basic_sort A("A");
583 :
584 1 : specification.add_sort(A);
585 :
586 2 : basic_sort L("L");
587 2 : basic_sort S("S");
588 2 : basic_sort B("B");
589 :
590 1 : specification.add_alias(alias(L, list(A)));
591 1 : specification.add_alias(alias(S, set_(A)));
592 1 : specification.add_alias(alias(B, bag(A)));
593 1 : BOOST_CHECK(normalize_sorts(L,specification) == normalize_sorts(list(A),specification));
594 1 : BOOST_CHECK(normalize_sorts(list(L),specification) == normalize_sorts(list(list(A)),specification));
595 1 : BOOST_CHECK(normalize_sorts(S,specification) == normalize_sorts(set_(A),specification));
596 1 : BOOST_CHECK(normalize_sorts(list(S),specification) == normalize_sorts(list(set_(A)),specification));
597 1 : BOOST_CHECK(normalize_sorts(B,specification) == normalize_sorts(bag(A),specification));
598 1 : BOOST_CHECK(normalize_sorts(list(B),specification) == normalize_sorts(list(bag(A)),specification));
599 :
600 2 : specification = parse_data_specification(
601 : "sort A = struct a(B);"
602 1 : "sort B = struct b(A)|c;");
603 :
604 1 : std::vector< structured_sort_constructor_argument > arguments;
605 :
606 1 : arguments.push_back(structured_sort_constructor_argument(basic_sort("B")));
607 1 : arguments.push_back(structured_sort_constructor_argument(basic_sort("A")));
608 :
609 1 : std::vector< structured_sort_constructor > constructors;
610 :
611 1 : constructors.push_back(structured_sort_constructor("a", structured_sort_constructor_argument_list(arguments.begin(), arguments.begin() + 1)));
612 1 : constructors.push_back(structured_sort_constructor("b", structured_sort_constructor_argument_list(arguments.begin() + 1, arguments.end())));
613 1 : constructors.push_back(structured_sort_constructor("c"));
614 :
615 1 : structured_sort sA(data::structured_sort(structured_sort_constructor_list(constructors.begin(), constructors.begin() + 1)));
616 1 : structured_sort sB(data::structured_sort(structured_sort_constructor_list(constructors.begin() + 1, constructors.end())));
617 :
618 1 : const std::set<sort_expression> sorts(specification.sorts());
619 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), normalize_sorts(sA,specification)) != sorts.end());
620 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), normalize_sorts(sB,specification)) != sorts.end());
621 :
622 1 : BOOST_CHECK(normalize_sorts(sA,specification) == normalize_sorts(normalize_sorts(sA,specification),specification));
623 1 : BOOST_CHECK(normalize_sorts(sB,specification) == normalize_sorts(normalize_sorts(sB,specification),specification));
624 :
625 : // Check whether the sort expression struct f(struct f(A)|g) |g normalises to A
626 : // in the context of the specification sort A = struct f(A) | g;
627 2 : specification = parse_data_specification(
628 1 : "sort A = struct f(A) | g;");
629 :
630 1 : std::vector< structured_sort_constructor_argument > arguments1;
631 1 : arguments1.push_back(structured_sort_constructor_argument(basic_sort("A")));
632 :
633 1 : std::vector< structured_sort_constructor > constructors1;
634 1 : constructors1.push_back(structured_sort_constructor("f", arguments1));
635 1 : constructors1.push_back(structured_sort_constructor("g"));
636 :
637 1 : sort_expression s1=structured_sort(constructors1); // s1 has the shape struct f(A)|g
638 1 : std::vector< structured_sort_constructor_argument > arguments2;
639 1 : arguments2.push_back(structured_sort_constructor_argument(s1));
640 :
641 1 : std::vector< structured_sort_constructor > constructors2;
642 1 : constructors2.push_back(structured_sort_constructor("f", arguments2));
643 1 : constructors2.push_back(structured_sort_constructor("g"));
644 :
645 2 : sort_expression s2=structured_sort(constructors2); // s2 has the shape f(struct f(A)|g) |g
646 1 : BOOST_CHECK(normalize_sorts(s2,specification)==basic_sort("A"));
647 1 : }
648 :
649 1 : void test_copy()
650 : {
651 1 : std::clog << "test_copy" << std::endl;
652 :
653 : data_specification specification = parse_data_specification(
654 : "sort D = struct d(bla : Bool)?is_d;"
655 : "sort A = S;"
656 : "sort S;"
657 2 : "map f: Set(S);");
658 :
659 1 : function_symbol_vector constructors(specification.constructors());
660 1 : BOOST_CHECK(std::find(constructors.begin(), constructors.end(), sort_bool::true_()) != constructors.end());
661 :
662 1 : data_specification other;
663 1 : other = specification;
664 :
665 1 : BOOST_CHECK(other == specification);
666 :
667 1 : specification = data_specification();
668 :
669 :
670 1 : BOOST_CHECK(normalize_sorts(basic_sort("A"),other) == normalize_sorts(basic_sort("S"),other));
671 :
672 1 : const std::set<sort_expression> sorts(specification.sorts());
673 1 : BOOST_CHECK(std::find(sorts.begin(), sorts.end(), basic_sort("A")) == sorts.end());
674 1 : }
675 :
676 1 : void test_specification()
677 : {
678 2 : data_specification spec = parse_data_specification("sort D = struct d1|d2;");
679 1 : BOOST_CHECK(spec.constructors(basic_sort("D")).size() == 2);
680 1 : }
681 :
682 1 : void test_bke()
683 : {
684 1 : std::cout << "test_bke" << std::endl;
685 :
686 : std::string BKE =
687 : "% This model is translated from the mCRL model used for analysing the Bilateral \n"
688 : "% Key Exchange (BKE) protocol. The analysis is described in a paper with the \n"
689 : "% name 'Analysing the BKE-security protocol with muCRL', by Jan Friso Groote, \n"
690 : "% Sjouke Mauw and Alexander Serebrenik. \n"
691 : "% \n"
692 : "% The translation of the existing mCRL model into this mCRL2 model has been \n"
693 : "% performed manually. The purpose was making use of the additional language \n"
694 : "% features of mCRL2 with respect to mCRL. \n"
695 : "% \n"
696 : "% The behaviour of this model should be bisimular with the original mcrl model \n"
697 : "% after renaming actions. Though this is not verified for all system \n"
698 : "% configurations below. \n"
699 : "% \n"
700 : "% Eindhoven, June 11, 2008, Jeroen van der Wulp \n"
701 : " \n"
702 : "% Agents. There are exactly three agents - A, B, E An order E < A < B is \n"
703 : "% imposed on agents to reduce the size of the state space. \n"
704 : "sort Agent = struct A | B | E; \n"
705 : "map less : Agent # Agent -> Bool; \n"
706 : "var a: Agent; \n"
707 : "eqn less(A,a) = (a == B); \n"
708 : " less(B,a) = false; \n"
709 : " less(E,a) = (a != E); \n"
710 : " \n"
711 : "sort Address = struct address(agent : Agent); \n"
712 : "map bad_address : Address; \n"
713 : " \n"
714 : "% A nonce is a random, unpredictable value which is used to make the \n"
715 : "% exchanged messages unique and thus helps to counter replay attacks. \n"
716 : "sort Nonce = struct nonce(value : Nat); \n"
717 : " \n"
718 : "% There are two kinds of keys used in the protocol: symmetric and \n"
719 : "% asymmetric ones (functional keys). \n"
720 : "% Symmetric keys have form K(n) where n is a natural number. \n"
721 : "sort SymmetricKey = struct symmetric_key(value : Nat); \n"
722 : " \n"
723 : "% Sort for representing asymmetric keys \n"
724 : "sort AsymmetricKey = struct public_key(Agent)?is_public | \n"
725 : " secret_key(Agent)?is_secret | \n"
726 : " hash(value : Nonce)?is_hash; \n"
727 : "map has_complementary_key: AsymmetricKey -> Bool; \n"
728 : " complementary_key : AsymmetricKey -> AsymmetricKey; \n"
729 : "var a : Agent; \n"
730 : " n : Nonce; \n"
731 : "eqn has_complementary_key(public_key(a)) = true; \n"
732 : " has_complementary_key(secret_key(a)) = true; \n"
733 : " has_complementary_key(hash(n)) = false; \n"
734 : " complementary_key(public_key(a)) = secret_key(a); \n"
735 : " complementary_key(secret_key(a)) = public_key(a); \n"
736 : " \n"
737 : "sort Key = struct key(SymmetricKey)?is_symmetric | key(AsymmetricKey)?is_asymmetric; \n"
738 : "map has_complementary_key: Key -> Bool; \n"
739 : " complementary_key : Key -> Key; % gets the complementary key if key is asymmetric \n"
740 : "var a,a1 : Agent; \n"
741 : " n,n1 : Nat; \n"
742 : " k,k1 : Key; \n"
743 : " ak,ak1 : AsymmetricKey; \n"
744 : "eqn \n"
745 : " % gets the complementary key if key is asymmetric \n"
746 : " complementary_key(key(ak)) = key(complementary_key(ak)); \n"
747 : " has_complementary_key(key(ak)) = has_complementary_key(ak); \n"
748 : " \n"
749 : "sort Message = struct \n"
750 : " encrypt(Nonce, Address, AsymmetricKey)?is_message_1 | \n"
751 : " encrypt(AsymmetricKey, Nonce, SymmetricKey, AsymmetricKey)?is_message_2 | \n"
752 : " encrypt(AsymmetricKey, SymmetricKey)?is_message_3; \n"
753 : "map valid_message_1 : Message # AsymmetricKey -> Bool; \n"
754 : " valid_message_2 : Message # AsymmetricKey -> Bool; \n"
755 : " valid_message_3 : Message # SymmetricKey -> Bool; \n"
756 : " used_key : Message -> Key; % key used to encrypt \n"
757 : "var sk, sk1 : SymmetricKey; \n"
758 : " ak, ak1, ak2 : AsymmetricKey; \n"
759 : " n, n1 : Nonce; \n"
760 : " m, m1 : Message; \n"
761 : " a, a1 : Address; \n"
762 : "eqn used_key(encrypt(n,a,ak)) = key(ak); \n"
763 : " used_key(encrypt(ak,n1,sk,ak1)) = key(ak1); \n"
764 : " used_key(encrypt(ak,sk)) = key(sk); \n"
765 : " valid_message_1(m, ak) = is_message_1(m) && (used_key(m) == key(ak)); \n"
766 : " valid_message_2(m, ak) = is_message_2(m) && (used_key(m) == key(ak)); \n"
767 : " valid_message_3(m, sk) = is_message_3(m) && (used_key(m) == key(sk)); \n"
768 : " \n"
769 : "% Type for message sets; currently cannot use Set() because set iteration is not possible \n"
770 : "sort MessageSet = List(Message); \n"
771 : "map insert : Message # MessageSet -> MessageSet; \n"
772 : " select_crypted_by : Key # MessageSet -> MessageSet; \n"
773 : " select_not_crypted_by : Key # MessageSet -> MessageSet; \n"
774 : " select : (Message -> Bool) # MessageSet -> MessageSet; \n"
775 : "var k,k1 : Key; \n"
776 : " m,m1 : Message; \n"
777 : " ms : MessageSet; \n"
778 : " c : Message -> Bool; \n"
779 : "eqn \n"
780 : " % inserts a message m, if it is not in the list \n"
781 : " insert(m,[]) = [m]; \n"
782 : " m < m1 -> insert(m,m1|>ms) = m|>m1|>ms; \n"
783 : " m == m1 -> insert(m,m1|>ms) = m1|>ms; \n"
784 : " m1 < m -> insert(m,m1|>ms) = m1|>insert(m,ms); \n"
785 : " \n"
786 : " % the set (as ordered list) of messages in m that are signed by sk \n"
787 : " select_crypted_by(k,ms) = select(lambda x : Message.k == used_key(x),ms); \n"
788 : " select_not_crypted_by(k,ms) = select(lambda x : Message.k != used_key(x),ms); \n"
789 : " \n"
790 : " select(c,[]) = []; \n"
791 : " select(c,m|>ms) = if(c(m),m|>r,r) whr r = select(c, ms) end; \n"
792 : " \n"
793 : "% The eavesdropper's knowledge consists of: \n"
794 : "% * a list of addresses \n"
795 : "% * a list of nonces \n"
796 : "% * a list of keys (both symmetric and asymmetric) \n"
797 : "% * a list of messages of which the key is not known \n"
798 : "sort Knowledge = struct \n"
799 : " knowledge(addresses : Set(Address), \n"
800 : " nonces : Set(Nonce), \n"
801 : " keys : Set(Key), \n"
802 : " messages : MessageSet); \n"
803 : "map update_knowledge : Message # Knowledge -> Knowledge; \n"
804 : " propagate : MessageSet # Knowledge -> Knowledge; \n"
805 : " propagate : Key # Knowledge -> Knowledge; \n"
806 : " add_key : Key # Knowledge -> Knowledge; \n"
807 : " add_nonce : Nonce # Knowledge -> Knowledge; \n"
808 : " add_address : Address # Knowledge -> Knowledge; \n"
809 : "var m : Message; \n"
810 : " as : Set(Address); \n"
811 : " ns : Set(Nonce); \n"
812 : " ks : Set(Key); \n"
813 : " ms : MessageSet; \n"
814 : " k : Knowledge; \n"
815 : " sk : SymmetricKey; \n"
816 : " ak,hk : AsymmetricKey; \n"
817 : " ck : Key; \n"
818 : " n, n1 : Nonce; \n"
819 : " a : Address; \n"
820 : "eqn \n"
821 : " % adds keys to knowledge that are part of known messages encrypted with a new key \n"
822 : " has_complementary_key(ak) && complementary_key(key(ak)) in keys(k) -> \n"
823 : " update_knowledge(encrypt(n,a,ak),k) = \n"
824 : " propagate(key(ak), add_key(key(ak), \n"
825 : " add_address(a, add_nonce(n, k)))); \n"
826 : " has_complementary_key(ak) && complementary_key(key(ak)) in keys(k) -> \n"
827 : " update_knowledge(encrypt(hk,n1,sk,ak),k) = \n"
828 : " propagate(key(sk), propagate(key(ak), \n"
829 : " add_key(key(sk),add_key(key(ak),k)))); \n"
830 : " key(sk) in keys(k) -> \n"
831 : " update_knowledge(encrypt(ak,sk),k) = \n"
832 : " propagate(key(ak), add_key(key(ak),k)); \n"
833 : " \n"
834 : " % adds a message that cannot be decrypted with any known key \n"
835 : " ((is_symmetric(ck) && !(ck in keys(k))) || \n"
836 : " (is_asymmetric(ck) && !(has_complementary_key(ck) && \n"
837 : " (complementary_key(ck) in keys(k))))) whr ck = used_key(m) end -> \n"
838 : " update_knowledge(m,k) = \n"
839 : " knowledge(addresses(k),nonces(k),keys(k),insert(m,messages(k))); \n"
840 : " \n"
841 : " % adds a key to knowledge \n"
842 : " add_key(ck,knowledge(as,ns,ks,ms)) = knowledge(as,ns,ks + {ck},ms); \n"
843 : " add_nonce(n,knowledge(as,ns,ks,ms)) = knowledge(as,ns + {n},ks,ms); \n"
844 : " add_address(a,knowledge(as,ns,ks,ms)) = knowledge(as + {a},ns,ks,ms); \n"
845 : " \n"
846 : " % adds keys to knowledge that are part of messages encrypted with a key k \n"
847 : " propagate([],k) = k; \n"
848 : " propagate(m|>ms,k) = propagate(ms, update_knowledge(m, k)); \n"
849 : " propagate(ck,knowledge(as,ns,ks,ms)) = \n"
850 : " propagate(select_crypted_by(ck,ms), \n"
851 1 : " knowledge(as,ns,ks,select_not_crypted_by(ck,ms))); \n"
852 : ;
853 :
854 1 : data_specification data_spec = parse_data_specification(BKE);
855 1 : const alias_vector& aliases = data_spec.user_defined_aliases();
856 10 : for (const alias& a: aliases)
857 : {
858 9 : std::cout << "alias " << a << std::endl;
859 9 : const sort_expression& s = a.reference();
860 9 : if (is_structured_sort(s))
861 : {
862 23 : for (const structured_sort_constructor& constructor: structured_sort(s).constructors())
863 : {
864 36 : for (const structured_sort_constructor_argument& argument: constructor.arguments())
865 : {
866 21 : std::cout << "argument: " << argument << " " << argument << std::endl;
867 21 : const atermpp::aterm_appl& name = argument.name();
868 21 : if (name != core::empty_identifier_string())
869 : {
870 8 : std::cout << "name = " << name << std::endl;
871 : }
872 : }
873 : }
874 : }
875 : }
876 1 : }
877 :
878 1 : void test_abuse_of_tail()
879 : {
880 1 : std::cout << "Test abuse of tail\n";
881 : const std::string spec_string =
882 : "map tail:Nat#List(Bool) -> List(Bool);\n"
883 : "var vs: List(Bool);\n"
884 : "n: Nat;\n"
885 1 : "eqn tail(n, vs) = if(n==0, vs, tail(Int2Nat(n-1),vs));\n";
886 : try
887 : {
888 1 : data_specification data_spec=parse_data_specification(spec_string);
889 0 : BOOST_CHECK(false); // Typechecking is supposed to fail; one cannot get here.
890 0 : }
891 1 : catch (mcrl2::runtime_error &e)
892 : {
893 : // It is expected that a runtime error is thrown.
894 1 : }
895 1 : }
896 :
897 1 : void test_merge_data_specifications()
898 : {
899 : std::string DATASPEC =
900 : "sort D;\n"
901 1 : "cons s: D;"
902 : ;
903 1 : data_specification dataspec1 = parse_data_specification(DATASPEC);
904 1 : data_specification dataspec2 = parse_data_specification(DATASPEC);
905 1 : data_specification dataspec3 = merge_data_specifications(dataspec1, dataspec2);
906 1 : BOOST_CHECK(dataspec1 == dataspec3);
907 1 : }
908 :
909 1 : void test_standard_sorts_mappings_functions()
910 : {
911 1 : std::set < sort_expression > sorts;
912 1 : std::set < function_symbol > constructors;
913 1 : std::set <function_symbol > mappings;
914 :
915 1 : data_specification spec;
916 1 : spec.get_system_defined_sorts_constructors_and_mappings(sorts, constructors, mappings);
917 :
918 1 : BOOST_CHECK(sorts.size()==10);
919 1 : BOOST_CHECK(constructors.size()==17);
920 1 : BOOST_CHECK(mappings.size()==225);
921 1 : }
922 :
923 2 : BOOST_AUTO_TEST_CASE(test_main)
924 : {
925 1 : test_bke();
926 :
927 1 : test_sorts();
928 :
929 1 : test_constructors();
930 :
931 1 : test_functions();
932 :
933 1 : test_equations();
934 :
935 1 : test_is_certainly_finite();
936 :
937 1 : test_constructor();
938 :
939 1 : test_system_defined();
940 :
941 1 : test_utility_functionality();
942 :
943 1 : test_normalisation();
944 :
945 1 : test_copy();
946 :
947 1 : test_specification();
948 :
949 1 : test_abuse_of_tail();
950 :
951 1 : test_merge_data_specifications();
952 :
953 1 : test_standard_sorts_mappings_functions();
954 1 : }
955 :
956 :
|
