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_test.cpp
10 : /// \brief Some simple tests for the binary algorithm.
11 :
12 : #define BOOST_TEST_MODULE binary_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lps/binary.h"
16 : #include "mcrl2/lps/detail/test_input.h"
17 : #include "mcrl2/lps/linearise.h"
18 : #include "mcrl2/lps/parse.h"
19 :
20 : using namespace mcrl2;
21 : using namespace mcrl2::data;
22 : using namespace mcrl2::lps;
23 :
24 :
25 : ///All process parameters of sort D should have been translated to
26 : ///parameters of sort Bool. This leaves only parameters of sort Bool and Pos.
27 2 : BOOST_AUTO_TEST_CASE(case_1)
28 : {
29 : const std::string text(
30 : "sort D = struct d1|d2;\n"
31 : "act a:D;\n"
32 : "proc P(e:D) = sum d:D . a(e) . P(d);\n"
33 : "init P(d1);\n"
34 1 : );
35 :
36 1 : specification s0=remove_stochastic_operators(linearise(text));
37 1 : rewriter r(s0.data());
38 1 : specification s1 = s0;
39 1 : binary_algorithm<rewriter, specification>(s1, r).run();
40 :
41 1 : variable_list parameters1 = s1.process().process_parameters();
42 :
43 1 : int bool_param_count = 0;
44 2 : for (variable_list::iterator i = parameters1.begin(); i != parameters1.end(); ++i)
45 : {
46 1 : BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
47 1 : if (i->sort() == sort_bool::bool_())
48 : {
49 1 : ++bool_param_count;
50 : }
51 : }
52 1 : BOOST_CHECK_EQUAL(bool_param_count, 1);
53 1 : }
54 :
55 : /*
56 : * Sort D has got 8 constructors, which can therefore be encoded exactly in
57 : * a vector of 3 boolean variables. This means that all combinations of the
58 : * boolean variables encode a constructor.
59 : * Process parameter e should be replaced by a vector of boolean variables,
60 : * and should be replaced in nextstate.
61 : * The initial state should be altered accordingly.
62 : */
63 2 : BOOST_AUTO_TEST_CASE(case_2)
64 : {
65 : const std::string text(
66 : "sort D = struct d1|d2|d3|d4|d5|d6|d7|d8;\n"
67 : "act a:D;\n"
68 : "proc P(e:D) = sum d:D . a(e) . P(d);\n"
69 : "init P(d1);\n"
70 1 : );
71 :
72 1 : specification s0=remove_stochastic_operators(linearise(text));
73 1 : rewriter r(s0.data());
74 1 : specification s1 = s0;
75 1 : binary_algorithm<rewriter, specification>(s1, r).run();
76 :
77 1 : int bool_param_count = 0;
78 1 : for (variable_list::iterator i = s1.process().process_parameters().begin();
79 4 : i != s1.process().process_parameters().end();
80 3 : ++i)
81 : {
82 3 : BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
83 3 : if (i->sort() == sort_bool::bool_())
84 : {
85 3 : ++bool_param_count;
86 : }
87 : }
88 1 : BOOST_CHECK_EQUAL(bool_param_count, 3);
89 1 : }
90 :
91 : /*
92 : * Sort D has got 7 constructors, which can therefore be encoded in
93 : * a vector of 3 boolean variables. This means that there is one combination
94 : * of the boolean variables that does not encode a constructor.
95 : * Process parameter e should be replaced by a vector of boolean variables,
96 : * and should be replaced in nextstate.
97 : * The initial state should be altered accordingly.
98 : */
99 2 : BOOST_AUTO_TEST_CASE(case_3)
100 : {
101 : const std::string text(
102 : "sort D = struct d1|d2|d3|d4|d5|d6|d7;\n"
103 : "act a:D;\n"
104 : "proc P(e:D) = sum d:D . a(e) . P(d);\n"
105 : "init P(d1);\n"
106 1 : );
107 :
108 1 : specification s0=remove_stochastic_operators(linearise(text));
109 1 : rewriter r(s0.data());
110 1 : specification s1 = s0;
111 1 : binary_algorithm<rewriter, specification>(s1, r).run();
112 :
113 1 : int bool_param_count = 0;
114 1 : for (variable_list::iterator i = s1.process().process_parameters().begin();
115 4 : i != s1.process().process_parameters().end();
116 3 : ++i)
117 : {
118 3 : BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
119 3 : if (i->sort() == sort_bool::bool_())
120 : {
121 3 : ++bool_param_count;
122 : }
123 : }
124 1 : BOOST_CHECK_EQUAL(bool_param_count, 3);
125 1 : }
126 :
127 : /*
128 : * Sort D has got 2 constructors, and should be encoded into one boolean
129 : * variable. Process parameter e should be replaced by a single boolean variable
130 : * and the action a(e) and the initial state should be altered accordingly.
131 : *
132 : * Note there is parameter of sort Pos because of linearisation.
133 : */
134 2 : BOOST_AUTO_TEST_CASE(case_4)
135 : {
136 : const std::string text(
137 : "sort D = struct d1|d2;\n"
138 : "act a,b:D;\n"
139 : "proc P(e:D) = sum d:D . a(e) . b(d) . P(d);\n"
140 : "init P(d1);\n"
141 1 : );
142 :
143 1 : specification s0=remove_stochastic_operators(linearise(text));
144 1 : rewriter r(s0.data());
145 1 : specification s1 = s0;
146 1 : binary_algorithm<rewriter, specification>(s1, r).run();
147 :
148 1 : int bool_param_count = 0;
149 1 : for (variable_list::iterator i = s1.process().process_parameters().begin();
150 4 : i != s1.process().process_parameters().end();
151 3 : ++i)
152 : {
153 3 : BOOST_CHECK(i->sort() == sort_pos::pos() || i->sort() == sort_bool::bool_());
154 3 : if (i->sort() == sort_bool::bool_())
155 : {
156 2 : ++bool_param_count;
157 : }
158 : }
159 1 : BOOST_CHECK_EQUAL(bool_param_count, 2);
160 1 : }
161 :
162 : /*
163 : * Sort D has got 9 constructors, therefore it should be encoded in
164 : * a vector of 4 boolean variables. Note that this does leave a lot of
165 : * combinations of booleans that are not used (7 to be precise).
166 : * Process parameter e should be replaced by a vector of boolean variables,
167 : * and should be replaced in nextstate.
168 : * The initial state should be altered accordingly.
169 : */
170 2 : BOOST_AUTO_TEST_CASE(case_5)
171 : {
172 : const std::string text(
173 : "sort D = struct d1|d2|d3|d4|d5|d6|d7|d8|d9;\n"
174 : "act a:D;\n"
175 : "proc P(e:D) = sum d:D . a(e) . P(d);\n"
176 : "init P(d1);\n"
177 1 : );
178 :
179 1 : specification s0=remove_stochastic_operators(linearise(text));
180 1 : rewriter r(s0.data());
181 1 : specification s1 = s0;
182 1 : binary_algorithm<rewriter, specification>(s1, r).run();
183 :
184 1 : int bool_param_count = 0;
185 1 : for (variable_list::iterator i = s1.process().process_parameters().begin();
186 5 : i != s1.process().process_parameters().end();
187 4 : ++i)
188 : {
189 4 : BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
190 4 : if (i->sort() == sort_bool::bool_())
191 : {
192 4 : ++bool_param_count;
193 : }
194 : }
195 1 : BOOST_CHECK_EQUAL(bool_param_count, 4);
196 1 : }
197 :
198 : /*
199 : * Sort D is a sort with 4 constructors. It is a recursive construct of two
200 : * constructors parameterized with sort E, which is in turn a sort which has
201 : * got two simple constructors.
202 : * Sort D can be coded in a vector of 2 boolean variables, in which all
203 : * combinations are used.
204 : * Process parameter e should be replaced by a vector of boolean variables,
205 : * and should be replaced in nextstate.
206 : * The initial state should be altered accordingly.
207 : */
208 2 : BOOST_AUTO_TEST_CASE(case_6)
209 : {
210 : const std::string text(
211 : "sort D = struct d1(E) | d2(E);\n"
212 : " E = struct e1 | e2;\n"
213 : "act a:D;\n"
214 : "proc P(e:D) = sum d:D . a(e) . P(d);\n"
215 : "init P(d1(e1));\n"
216 1 : );
217 :
218 1 : specification s0=remove_stochastic_operators(linearise(text));
219 1 : rewriter r(s0.data());
220 1 : specification s1 = s0;
221 1 : binary_algorithm<rewriter, specification>(s1, r).run();
222 :
223 1 : int bool_param_count = 0;
224 1 : for (variable_list::iterator i = s1.process().process_parameters().begin();
225 3 : i != s1.process().process_parameters().end();
226 2 : ++i)
227 : {
228 2 : BOOST_CHECK_EQUAL(i->sort(), sort_bool::bool_());
229 2 : if (i->sort() == sort_bool::bool_())
230 : {
231 2 : ++bool_param_count;
232 : }
233 : }
234 1 : BOOST_CHECK_EQUAL(bool_param_count, 2);
235 1 : }
236 :
237 : // This test case shows a bug where apparently d1 and d2 are mapped to the
238 : // same boolean value. Test case was provided by Jan Friso Groote along with
239 : // bug 623.
240 2 : BOOST_AUTO_TEST_CASE(bug_623)
241 : {
242 : const std::string text(
243 : "sort D;\n"
244 : "cons d1,d2:D;\n"
245 : "act a:D#D;\n"
246 : "proc X(e1,e2:D) = a(e1,e2) . X(d1,d2);\n"
247 : "init X(d2,d1);\n"
248 1 : );
249 :
250 1 : specification s0=remove_stochastic_operators(linearise(text));
251 1 : rewriter r(s0.data());
252 1 : specification s1 = s0;
253 1 : binary_algorithm<rewriter, specification>(s1, r).run();
254 1 : action_summand_vector summands1 = s1.process().action_summands();
255 2 : for (auto & i : summands1)
256 : {
257 1 : data_expression_list next_state = i.next_state(s1.process().process_parameters());
258 1 : BOOST_CHECK_EQUAL(next_state.size(), 2u);
259 1 : BOOST_CHECK_NE(*next_state.begin(), *(++next_state.begin()));
260 1 : std::clog << "erroneous next state " << data::pp(next_state) << std::endl;
261 1 : }
262 :
263 1 : }
264 :
265 2 : BOOST_AUTO_TEST_CASE(abp)
266 : {
267 2 : specification spec=remove_stochastic_operators(linearise(lps::detail::ABP_SPECIFICATION()));
268 1 : std::clog << "--- before ---\n" << lps::pp(spec) << std::endl;
269 1 : rewriter r(spec.data());
270 1 : binary_algorithm<rewriter, specification>(spec, r).run();
271 1 : std::clog << "--- after ---\n" << lps::pp(spec) << std::endl;
272 1 : BOOST_CHECK(check_well_typedness(spec));
273 1 : }
274 :
275 2 : BOOST_AUTO_TEST_CASE(parameter_selection)
276 : {
277 : const std::string text =
278 : "sort Enum6 = struct e6_1 | e6_2 | e6_3 | e6_4 | e6_5 | e6_6;\n"
279 : "sort Enum5 = struct e5_1 | e5_2 | e5_3 | e5_4 | e5_5;\n"
280 : "act z;\n"
281 : "proc P(b:Pos, c:Enum6, d:Enum5) = z . P();\n"
282 1 : "init P(5, e6_2, e5_5);";
283 :
284 1 : specification s0 = parse_linear_process_specification(text);
285 1 : rewriter r(s0.data());
286 1 : specification s1 = s0;
287 1 : binary_algorithm<rewriter, specification>(s1, r, "*:Enum6").run();
288 :
289 1 : int bool_param_count = 0;
290 6 : for (const variable& v: s1.process().process_parameters())
291 : {
292 5 : BOOST_CHECK(v.sort() == sort_pos::pos() || v.sort() == sort_bool::bool_() || v.sort() == parse_sort_expression("Enum5", s0.data()));
293 5 : if (v.sort() == sort_bool::bool_())
294 : {
295 3 : ++bool_param_count;
296 : }
297 : }
298 1 : BOOST_CHECK_EQUAL(bool_param_count, 3);
299 1 : }
|
