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 alphabet_test.cpp
10 : /// \brief Test for alphabet reduction.
11 :
12 : #define BOOST_TEST_MODULE alphabet_test
13 : #include <boost/algorithm/string/predicate.hpp>
14 : #include <boost/test/included/unit_test.hpp>
15 :
16 : #include "mcrl2/process/alphabet_reduce.h"
17 : #include "mcrl2/process/detail/alphabet_intersection.h"
18 : #include "mcrl2/process/detail/alphabet_parse.h"
19 : #include "mcrl2/process/detail/alphabet_push_block.h"
20 :
21 : using namespace mcrl2;
22 : using namespace mcrl2::process;
23 :
24 : struct LogDebug
25 : {
26 1 : LogDebug()
27 : {
28 1 : log::logger::set_reporting_level(log::debug);
29 1 : }
30 : };
31 : BOOST_GLOBAL_FIXTURE(LogDebug);
32 :
33 : inline
34 : multi_action_name name(const process::action& x)
35 : {
36 : multi_action_name result;
37 : result.insert(x.label().name());
38 : return result;
39 : }
40 :
41 : inline
42 : multi_action_name name(const core::identifier_string& x)
43 : {
44 : multi_action_name result;
45 : result.insert(x);
46 : return result;
47 : }
48 :
49 115 : std::string print(const multi_action_name& alpha)
50 : {
51 115 : if (alpha.empty())
52 : {
53 3 : return "tau";
54 : }
55 112 : std::ostringstream out;
56 311 : for (const auto & i : alpha)
57 : {
58 199 : out << std::string(i);
59 : }
60 112 : std::string result = out.str();
61 112 : std::sort(result.begin(), result.end());
62 112 : return result;
63 112 : }
64 :
65 47 : std::string print(const multi_action_name_set& A, bool A_includes_subsets = false)
66 : {
67 47 : std::multiset<std::string> V;
68 162 : for (const auto & i : A)
69 : {
70 115 : V.insert(print(i));
71 : }
72 141 : return core::detail::print_set(V, "", false, false) + (A_includes_subsets ? "@" : "");
73 47 : }
74 :
75 12 : std::string print(const allow_set& x)
76 : {
77 12 : return print(x.A, x.A_includes_subsets);
78 : }
79 :
80 2 : BOOST_AUTO_TEST_CASE(test_print)
81 : {
82 2 : auto [A, dummy] = detail::parse_simple_multi_action_name_set("{a}");
83 1 : multi_action_name tau;
84 1 : A.insert(tau);
85 1 : std::cout << print(A) << std::endl;
86 1 : BOOST_CHECK(print(A) == "{a, tau}");
87 1 : }
88 :
89 2 : BOOST_AUTO_TEST_CASE(test_parse)
90 : {
91 1 : multi_action_name_set B;
92 : bool dummy;
93 1 : std::tie(B, dummy) = detail::parse_simple_multi_action_name_set("{a, ab}");
94 1 : std::cout << "B = " << print(B) << std::endl;
95 1 : BOOST_CHECK(print(B) == "{a, ab}");
96 1 : }
97 :
98 2 : BOOST_AUTO_TEST_CASE(test_includes)
99 : {
100 2 : multi_action_name alpha = detail::parse_simple_multi_action_name("abb");
101 2 : multi_action_name beta = detail::parse_simple_multi_action_name("aabb");
102 1 : BOOST_CHECK(!alphabet_operations::includes(alpha, beta));
103 1 : BOOST_CHECK(alphabet_operations::includes(beta, alpha));
104 1 : }
105 :
106 2 : BOOST_AUTO_TEST_CASE(test_alphabet_reduce)
107 : {
108 : std::string text =
109 : "act a; \n"
110 : "proc P = a.P; \n"
111 1 : "init P; \n"
112 : ;
113 1 : process_specification procspec = parse_process_specification(text);
114 1 : alphabet_reduce(procspec);
115 1 : }
116 :
117 44 : void check_result(const std::string& expression, const std::string& result, const std::string& expected_result, const std::string& title)
118 : {
119 44 : if (result != expected_result)
120 : {
121 0 : std::cout << "--- failure in " << title << " ---" << std::endl;
122 0 : std::cout << "expression = " << expression << std::endl;
123 0 : std::cout << "result = " << result << std::endl;
124 0 : std::cout << "expected result = " << expected_result << std::endl;
125 0 : BOOST_CHECK(result == expected_result);
126 : }
127 44 : }
128 :
129 7 : void test_alphabet(const std::string& expression, const std::string& expected_result, const std::string& equations = "")
130 : {
131 14 : std::string text = "act a, b, c, d;\n" + equations + "\ninit " + expression + ";\n";
132 7 : process_specification procspec = parse_process_specification(text);
133 7 : multi_action_name_set A = alphabet(procspec.init(), procspec.equations());
134 7 : std::string result = print(A);
135 7 : check_result(expression, result, expected_result, "alphabet");
136 7 : }
137 :
138 2 : BOOST_AUTO_TEST_CASE(test_alphabet1)
139 : {
140 1 : test_alphabet("a || b", "{a, ab, b}");
141 1 : test_alphabet("allow({ a, a | b }, a || b)", "{a, ab}");
142 1 : test_alphabet("allow({a}, a || a)", "{a}");
143 1 : test_alphabet("a", "{a}");
144 1 : test_alphabet("c|c", "{cc}");
145 1 : test_alphabet("a.c|c", "{a, cc}");
146 1 : test_alphabet("tau.a", "{a, tau}");
147 1 : }
148 :
149 : template <typename Operation>
150 7 : void test_alphabet_operation(const std::string& text1, const std::string& text2, const std::string& expected_result, Operation op, const std::string& title)
151 : {
152 : bool dummy;
153 7 : multi_action_name_set A1, A2;
154 7 : std::tie(A1, dummy) = detail::parse_simple_multi_action_name_set(text1);
155 7 : std::tie(A2, dummy) = detail::parse_simple_multi_action_name_set(text2);
156 7 : multi_action_name_set A3 = op(A1, A2);
157 7 : std::string result = print(A3);
158 7 : check_result(text1 + ", " + text2, result, expected_result, title);
159 7 : }
160 :
161 2 : BOOST_AUTO_TEST_CASE(test_alphabet_operations)
162 : {
163 : using namespace alphabet_operations;
164 1 : test_alphabet_operation("{a}", "{b}", "{ab}", concat, "concat");
165 1 : test_alphabet_operation("{ab}", "{b, c}", "{abb, abc}", concat, "concat");
166 1 : test_alphabet_operation("{ab, aabc}", "{b, bc}", "{a, aa, aabc, aac, ab}", left_arrow1, "left_arrow1");
167 1 : test_alphabet_operation("{aa, b}", "{a}", "{a, aa, b}", left_arrow1, "left_arrow1");
168 1 : test_alphabet_operation("{ab, b}", "{b}", "{a, ab, b}", left_arrow1, "left_arrow1"); // N.B. tau is excluded!
169 1 : test_alphabet_operation("{bc}", "{c}", "{b, bc}", left_arrow1, "left_arrow1");
170 1 : test_alphabet_operation("{a}", "{a}", "{a}", left_arrow1, "left_arrow1");
171 1 : }
172 :
173 1 : void test_push_allow(const std::string& expression, const std::string& Atext, const std::string& expected_result, const std::string& equations = "")
174 : {
175 2 : std::string text = "act a, b, c, d;\n" + equations + "\ninit " + expression + ";\n";
176 1 : process_specification procspec = parse_process_specification(text);
177 1 : auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
178 1 : data::set_identifier_generator id_generator;
179 :
180 1 : std::map<process_identifier, multi_action_name_set> pcrl_equation_cache = detail::compute_pcrl_equation_cache(procspec.equations());
181 1 : process::detail::push_allow_cache W(id_generator, pcrl_equation_cache);
182 2 : process::detail::push_allow_node node = process::detail::push_allow(procspec.init(), allow_set(A, A_includes_subsets), procspec.equations(), W);
183 1 : std::string result = process::pp(node.expression);
184 1 : check_result(expression, result, expected_result, "push_allow");
185 1 : }
186 :
187 2 : BOOST_AUTO_TEST_CASE(test_push_allow1)
188 : {
189 1 : test_push_allow("a || a", "{a}", "allow({a}, a || a)");
190 1 : }
191 :
192 : template <typename Operation>
193 4 : void test_comm_operation(const std::string& comm_text, const std::string& Atext, const std::string& expected_result, Operation op, const std::string& title)
194 : {
195 4 : communication_expression_list C = detail::parse_comm_set(comm_text);
196 4 : auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
197 4 : multi_action_name_set A1 = op(C, A, A_includes_subsets);
198 4 : std::string result = print(A1, A_includes_subsets);
199 4 : check_result(comm_text + ", " + Atext, result, expected_result, title);
200 :
201 4 : if (title == "comm_inverse")
202 : {
203 4 : allow_set A2 = alphabet_operations::comm_inverse(C, allow_set(A, A_includes_subsets));
204 2 : std::string result_allow = print(A2);
205 2 : check_result(comm_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
206 2 : }
207 4 : }
208 :
209 2 : BOOST_AUTO_TEST_CASE(test_comm_operations)
210 : {
211 : // resolve ambiguity
212 2 : auto comm_inverse = [](const communication_expression_list& C, const multi_action_name_set& A, bool A_includes_subsets) { return alphabet_operations::comm_inverse(C, A, A_includes_subsets); };
213 1 : test_comm_operation("{a|b -> c}", "{c}", "{ab, c}", comm_inverse, "comm_inverse");
214 1 : test_comm_operation("{a|a -> b}", "{b, bb}", "{aa, aaaa, aab, b, bb}", comm_inverse, "comm_inverse");
215 1 : test_comm_operation("{a|b -> c}", "{ab, aab, aabb, abd}", "{aab, aabb, ab, abc, abd, ac, c, cc, cd}", alphabet_operations::comm, "comm");
216 1 : test_comm_operation("{a|b -> c}", "{ab, aab, aabb, abd}@", "{aab, aabb, ab, abc, abd, ac, c, cc, cd}@", alphabet_operations::comm, "comm");
217 1 : }
218 :
219 : template <typename Operation>
220 8 : void test_rename_operation(const std::string& rename_text, const std::string& Atext, const std::string& expected_result, Operation op, const std::string& title)
221 : {
222 8 : rename_expression_list R = detail::parse_rename_set(rename_text);
223 8 : auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
224 8 : multi_action_name_set A1 = op(R, A, A_includes_subsets);
225 8 : std::string result = print(A1, A_includes_subsets);
226 8 : check_result(rename_text + ", " + Atext, result, expected_result, title);
227 :
228 8 : if (title == "rename_inverse")
229 : {
230 12 : allow_set A2 = alphabet_operations::rename_inverse(R, allow_set(A, A_includes_subsets));
231 6 : std::string result_allow = print(A2);
232 6 : check_result(rename_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
233 6 : }
234 8 : }
235 :
236 2 : BOOST_AUTO_TEST_CASE(test_rename_operations)
237 : {
238 : // resolve ambiguity
239 6 : auto rename_inverse = [](const rename_expression_list& R, const multi_action_name_set& A, bool A_includes_subsets) { return alphabet_operations::rename_inverse(R, A, A_includes_subsets); };
240 1 : test_rename_operation("{a -> b, c -> d}", "{ab, aacc}", "{bb, bbdd}", alphabet_operations::rename, "rename");
241 1 : test_rename_operation("{a -> b, c -> d}", "{ab, aacc}@", "{bb, bbdd}@", alphabet_operations::rename, "rename");
242 1 : test_rename_operation("{a -> b, c -> d}", "{abd, bcdd}", "{}", rename_inverse, "rename_inverse");
243 1 : test_rename_operation("{a -> b}", "{b, bb}", "{a, aa, ab, b, bb}", rename_inverse, "rename_inverse");
244 1 : test_rename_operation("{a -> b}", "{bb}@", "{aa, ab, bb}@", rename_inverse, "rename_inverse");
245 1 : test_rename_operation("{a -> b}", "{b}", "{a, b}", rename_inverse, "rename_inverse");
246 1 : test_rename_operation("{a -> b}", "{a}", "{}", rename_inverse, "rename_inverse");
247 1 : test_rename_operation("{b -> a}", "{a, bc}@", "{a, b, c}@", rename_inverse, "rename_inverse");
248 1 : }
249 :
250 : template <typename Operation>
251 1 : void test_hide_operation(const std::string& hide_text, const std::string& Atext, const std::string& expected_result, Operation op, const std::string& title)
252 : {
253 1 : core::identifier_string_list I = detail::parse_block_set(hide_text);
254 1 : auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
255 1 : multi_action_name_set A1 = op(I, A, A_includes_subsets);
256 1 : std::string result = print(A1, A_includes_subsets);
257 1 : check_result(hide_text + ", " + Atext, result, expected_result, title);
258 1 : }
259 :
260 2 : BOOST_AUTO_TEST_CASE(test_hide_operations)
261 : {
262 1 : auto hide_inverse = [](const core::identifier_string_list& I, const multi_action_name_set& A, bool A_includes_subsets) { return alphabet_operations::hide_inverse(I, A, A_includes_subsets); };
263 1 : test_hide_operation("{b}", "{ab}", "{}", hide_inverse, "hide_inverse");
264 1 : }
265 :
266 2 : void test_allow(const std::string& allow_text, const std::string& Atext, const std::string& expected_result, const std::string& title)
267 : {
268 2 : action_name_multiset_list V = detail::parse_allow_set(allow_text);
269 2 : auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
270 2 : multi_action_name_set A1 = alphabet_operations::allow(V, A, A_includes_subsets);
271 2 : std::string result = print(A1);
272 2 : check_result(allow_text + ", " + Atext, result, expected_result, title);
273 :
274 4 : allow_set A2 = alphabet_operations::allow(V, allow_set(A, A_includes_subsets));
275 2 : std::string result_allow = print(A2);
276 2 : check_result(allow_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
277 2 : }
278 :
279 2 : BOOST_AUTO_TEST_CASE(test_allow1)
280 : {
281 1 : test_allow("{a|b, a|b|b, c}", "{ab, abbc, c}", "{ab, c}", "allow");
282 1 : test_allow("{a, b, c}", "{ab}@", "{a, b}", "allow");
283 : // test_allow("{a|b}", "{a}@{b, c}", "{a|b}", "allow");
284 1 : }
285 :
286 2 : void test_block(const std::string& block_text, const std::string& Atext, const std::string& expected_result, const std::string& title)
287 : {
288 2 : core::identifier_string_list B = detail::parse_block_set(block_text);
289 2 : auto [A, A_includes_subsets] = detail::parse_simple_multi_action_name_set(Atext);
290 2 : multi_action_name_set A1 = alphabet_operations::block(B, A, A_includes_subsets);
291 2 : std::string result = print(A1, A_includes_subsets);
292 2 : check_result(block_text + ", " + Atext, result, expected_result, title);
293 :
294 4 : allow_set A2 = alphabet_operations::block(B, allow_set(A, A_includes_subsets));
295 2 : std::string result_allow = print(A2);
296 2 : check_result(block_text + ", " + Atext, result_allow, expected_result, title + "<allow>");
297 2 : }
298 :
299 2 : BOOST_AUTO_TEST_CASE(test_block1)
300 : {
301 1 : test_block("{b}", "{ab, abbc, c}", "{c}", "block");
302 1 : test_block("{b}", "{ab, abbc, c}@", "{a, ac, c}@", "block");
303 1 : }
304 :
305 19 : multi_action_name make_multi_action_name(const std::string& x)
306 : {
307 19 : multi_action_name result;
308 19 : result.insert(core::identifier_string(x));
309 19 : return result;
310 0 : }
311 :
312 2 : BOOST_AUTO_TEST_CASE(test_alphabet_parallel)
313 : {
314 : std::string text =
315 : "act a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20; \n"
316 1 : "init a1 || a2 || a3 || a4 || a5 || a6 || a7 || a8 || a9 || a10 || a11 || a12 || a13 || a14 || a15 || a16 || a17 || a18 || a19 || a20; \n"
317 : ;
318 : // "init allow({a1, a2, a3, a4, a5, a6, a7, a8, a9, a10}, a1 || a2 || a3 || a4 || a5 || a6 || a7 || a8 || a9 || a10); \n"
319 1 : process_specification procspec = parse_process_specification(text);
320 1 : multi_action_name_set A;
321 1 : A.insert(make_multi_action_name("a1"));
322 1 : A.insert(make_multi_action_name("a2"));
323 1 : A.insert(make_multi_action_name("a3"));
324 1 : A.insert(make_multi_action_name("a4"));
325 1 : A.insert(make_multi_action_name("a5"));
326 1 : A.insert(make_multi_action_name("a6"));
327 1 : A.insert(make_multi_action_name("a7"));
328 1 : A.insert(make_multi_action_name("a8"));
329 1 : A.insert(make_multi_action_name("a9"));
330 1 : A.insert(make_multi_action_name("a11"));
331 1 : A.insert(make_multi_action_name("a12"));
332 1 : A.insert(make_multi_action_name("a13"));
333 1 : A.insert(make_multi_action_name("a14"));
334 1 : A.insert(make_multi_action_name("a15"));
335 1 : A.insert(make_multi_action_name("a16"));
336 1 : A.insert(make_multi_action_name("a17"));
337 1 : A.insert(make_multi_action_name("a18"));
338 1 : A.insert(make_multi_action_name("a19"));
339 1 : A.insert(make_multi_action_name("a20"));
340 :
341 1 : multi_action_name_set B = detail::alphabet_intersection(procspec.init(), procspec.equations(), A);
342 : //BOOST_CHECK_EQUAL(lps::pp(B),"{a1, a2, a3, a4, a5, a6, a7, a8, a9, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20}");
343 1 : BOOST_CHECK_EQUAL(process::pp(B), process::pp(A));
344 1 : }
345 :
346 2 : BOOST_AUTO_TEST_CASE(test_alphabet_new)
347 : {
348 : std::string text =
349 : "act a: Bool; \n"
350 : "proc S(d: Bool) = sum d:Bool. a(d).S(d); \n"
351 1 : "init allow({a}, S(true)) ; \n"
352 : ;
353 1 : process_specification procspec = parse_process_specification(text);
354 1 : alphabet_reduce(procspec);
355 1 : }
356 :
|