Line data Source code
1 : // Author(s): Jan Friso Groote
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 action_rename_test.cpp
10 : /// \brief Action rename test.
11 :
12 : #define BOOST_TEST_MODULE action_rename_test
13 : #include "mcrl2/lps/linearise.h"
14 : #include "mcrl2/lps/parse.h"
15 : #include "mcrl2/lps/remove.h"
16 : #include "mcrl2/lps/rewrite.h"
17 : #include <boost/test/included/unit_test.hpp>
18 :
19 : using namespace mcrl2;
20 : using lps::stochastic_specification;
21 : using lps::action_rename_specification;
22 : using lps::action_summand;
23 : using lps::action_summand_vector;
24 : using lps::deadlock_summand;
25 :
26 1 : void test1()
27 : {
28 : // Check a renaming when more than one renaming rule
29 : // for one action is present.
30 : const std::string SPEC =
31 : "act a:Nat; \n"
32 : "proc P(n:Nat) = sum m: Nat. a(m). P(m); \n"
33 1 : "init P(0); \n";
34 :
35 : const std::string AR_SPEC =
36 : "act b,c:Nat;\n"
37 : "var n:Nat;\n"
38 : "rename \n"
39 : " (n>4) -> a(n) => b(n); \n"
40 1 : " (n<22) -> a(n) => c(n); \n";
41 :
42 1 : stochastic_specification spec=lps::linearise(SPEC);
43 1 : std::istringstream ar_spec_stream(AR_SPEC);
44 1 : action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
45 2 : stochastic_specification new_spec = action_rename(ar_spec,spec,data::rewriter(),false);
46 1 : BOOST_CHECK(check_well_typedness(new_spec));
47 1 : BOOST_CHECK(new_spec.process().summand_count()==3);
48 1 : }
49 :
50 1 : void test2()
51 : {
52 : // Check whether new declarations in the rename file
53 : // are read properly. Check for renamings of more than one action.
54 : const std::string SPEC =
55 : "act a,b:Nat; \n"
56 : "proc P(n:Nat) = sum m: Nat. a(m). P(m); \n"
57 1 : "init P(0); \n";
58 :
59 : const std::string AR_SPEC =
60 : "map f:Nat->Nat; \n"
61 : "var n':Nat; \n"
62 : "eqn f(n')=3; \n"
63 : "act c:Nat; \n"
64 : "var n:Nat; \n"
65 : "rename \n"
66 : " (f(n)>23) -> a(n) => b(n); \n"
67 1 : " b(n) => c(n); \n";
68 :
69 1 : stochastic_specification spec=lps::linearise(SPEC);
70 1 : std::istringstream ar_spec_stream(AR_SPEC);
71 1 : action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
72 2 : stochastic_specification new_spec = action_rename(ar_spec,spec,data::rewriter(),false);
73 1 : BOOST_CHECK(check_well_typedness(new_spec));
74 1 : BOOST_CHECK(new_spec.process().summand_count()==2);
75 1 : }
76 :
77 1 : void test3()
78 : {
79 : // Check whether constants in an action_rename file are properly translated.
80 : const std::string SPEC =
81 : "act a,b:Nat; \n"
82 : "proc P(n:Nat) = a(1). P(n)+b(1).P(1); \n"
83 1 : "init P(0); \n";
84 :
85 : const std::string AR_SPEC =
86 : "rename \n"
87 1 : " a(1) => delta; \n";
88 :
89 1 : stochastic_specification spec=lps::linearise(SPEC);
90 1 : std::istringstream ar_spec_stream(AR_SPEC);
91 1 : action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
92 1 : data::rewriter R (spec.data(), mcrl2::data::rewriter::strategy());
93 1 : stochastic_specification new_spec = action_rename(ar_spec,spec,data::rewriter(),false);
94 1 : lps::rewrite(new_spec, R);
95 1 : lps::remove_trivial_summands(new_spec);
96 1 : BOOST_CHECK(check_well_typedness(new_spec));
97 1 : BOOST_CHECK(new_spec.process().summand_count()==2);
98 1 : }
99 :
100 1 : void test4()
101 : {
102 : const std::string SPEC =
103 : "sort D = struct d1 | d2;\n"
104 : " E = D;\n"
105 : "\n"
106 : "act a : E;\n"
107 : "\n"
108 : "proc P(d:D) = a(d) . P(d1);\n"
109 : "\n"
110 1 : "init P(d2);\n";
111 :
112 : const std::string AR_SPEC =
113 : "var e : E;\n"
114 : "rename\n"
115 1 : "(e==d1) -> a(e) => tau;\n";
116 :
117 1 : stochastic_specification spec=lps::linearise(SPEC);
118 1 : std::istringstream ar_spec_stream(AR_SPEC);
119 1 : action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
120 1 : data::rewriter R (spec.data(), mcrl2::data::rewriter::strategy());
121 1 : stochastic_specification new_spec = action_rename(ar_spec,spec,data::rewriter(),false);
122 1 : lps::rewrite(new_spec, R);
123 1 : lps::remove_trivial_summands(new_spec);
124 1 : BOOST_CHECK(check_well_typedness(new_spec));
125 1 : BOOST_CHECK(new_spec.process().summand_count()==2);
126 1 : }
127 :
128 1 : void test5() // Test whether partial renaming to delta is going well. See bug report #1009.
129 : {
130 : const std::string SPEC =
131 : "sort Command = struct com1 | com2;\n"
132 : "sort State = struct st1 | st2;\n"
133 : "\n"
134 : "proc Parent(id: Nat, children: List(Nat)) =\n"
135 : " sum child: Nat, command: Command . (child in children) -> sc(id, child, command) . Parent()\n"
136 : "+ sum child: Nat, state: State . (child in children) -> rs(child, id, state) . Parent();\n"
137 : "\n"
138 : "proc Child(id: Nat, parent: Nat) =\n"
139 : " sum command: Command . rc(parent, id, command) . Child()\n"
140 : "+ sum state: State . ss(id, parent, state) . Child();\n"
141 : "\n"
142 : "act sc, rc, cc: Nat # Nat # Command;\n"
143 : " rs, ss, cs: Nat # Nat # State;\n"
144 : "\n"
145 : "act none;\n"
146 : "\n"
147 : "init\n"
148 : " allow({cc, cs, sc, rs},\n"
149 : " comm({sc|rc -> cc, rs|ss->cs},\n"
150 : " Parent(0, [1, 2]) ||\n"
151 : " Child(1, 0) ||\n"
152 : " Child(2, 0)\n"
153 1 : " ));\n";
154 :
155 :
156 : const std::string AR_SPEC =
157 : "var c: Command;\n"
158 : " s: State;\n"
159 : "rename\n"
160 : " sc(0, 1, c) => delta;\n"
161 1 : " rs(1, 0, s) => delta;\n";
162 :
163 :
164 1 : stochastic_specification spec=lps::linearise(SPEC);
165 1 : std::istringstream ar_spec_stream(AR_SPEC);
166 1 : action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
167 1 : data::rewriter R (spec.data(), mcrl2::data::rewriter::strategy());
168 1 : stochastic_specification new_spec = action_rename(ar_spec,spec,data::rewriter(),false);
169 1 : lps::rewrite(new_spec, R);
170 1 : lps::remove_trivial_summands(new_spec);
171 1 : BOOST_CHECK(check_well_typedness(new_spec));
172 1 : BOOST_CHECK(new_spec.process().summand_count()==8);
173 1 : }
174 :
175 : // Check whether renaming with a regular expression works well
176 1 : static void test_regex1()
177 : {
178 : const std::string SPEC =
179 : "act a_out, b_out, cout, ab_out, ac_out;\n"
180 1 : "init a_out|ab_out . b_out . cout . delta;";
181 :
182 1 : stochastic_specification spec = lps::linearise(SPEC);
183 : // This should rename a_out and ac_out, leaving the rest
184 2 : stochastic_specification new_spec = action_rename(std::regex("^([^b]*)_out"), "out_$1", spec);
185 :
186 1 : BOOST_CHECK(check_well_typedness(new_spec));
187 1 : BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "out_a");
188 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().front().name()) == "b_out");
189 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().front().name()) == "cout");
190 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().tail().front().name()) == "ab_out");
191 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().tail().tail().front().name()) == "out_ac");
192 :
193 4 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
194 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "out_a|ab_out"; }));
195 3 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
196 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "b_out"; }));
197 2 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
198 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "cout"; }));
199 1 : }
200 :
201 : // Check whether renaming some actions to delta works
202 1 : void test_regex2()
203 : {
204 : const std::string SPEC =
205 : "act a_out, b_out, cout, ab_out, ac_out;\n"
206 1 : "init a_out|ab_out . b_out . cout . delta;";
207 :
208 1 : stochastic_specification spec = lps::linearise(SPEC);
209 : // This should rename a_out, leaving the rest
210 2 : stochastic_specification new_spec = action_rename(std::regex("^a_out"), "delta", spec);
211 :
212 1 : BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "b_out");
213 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().front().name()) == "cout");
214 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().front().name()) == "ab_out");
215 :
216 3 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
217 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "b_out"; }));
218 2 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
219 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "cout"; }));
220 :
221 1 : BOOST_CHECK(new_spec.process().deadlock_summands().size() == 2);
222 1 : auto find_result = std::find_if(spec.process().action_summands().begin(), spec.process().action_summands().end(),
223 3 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "a_out|ab_out"; });
224 1 : BOOST_CHECK(find_result != spec.process().action_summands().end());
225 1 : if(find_result != spec.process().action_summands().end())
226 : {
227 3 : BOOST_CHECK(std::any_of(new_spec.process().deadlock_summands().begin(), new_spec.process().deadlock_summands().end(),
228 : [&find_result](const deadlock_summand& ds){ return ds.condition() == find_result->condition(); }));
229 : }
230 1 : }
231 :
232 : // Check whether renaming some actions to tau works
233 1 : void test_regex3()
234 : {
235 : const std::string SPEC =
236 : "act a_out, b_out, cout, ab_out, ac_out;\n"
237 1 : "init a_out|ab_out . b_out . cout . delta;";
238 :
239 1 : stochastic_specification spec = lps::linearise(SPEC);
240 : // This should rename a_out and cout, leaving the rest
241 2 : stochastic_specification new_spec = action_rename(std::regex("^(a_out|cout)$"), "tau", spec);
242 :
243 1 : BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "b_out");
244 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().front().name()) == "ab_out");
245 1 : BOOST_CHECK(std::string(new_spec.action_labels().tail().tail().front().name()) == "ac_out");
246 :
247 4 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
248 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "ab_out"; }));
249 3 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
250 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "b_out"; }));
251 2 : BOOST_CHECK(std::any_of(new_spec.process().action_summands().begin(), new_spec.process().action_summands().end(),
252 : [](const action_summand& as){ return lps::pp(as.multi_action()) == "tau"; }));
253 1 : }
254 :
255 : // Check whether the list of actions contains no duplicates after renaming multiple actions
256 : // to one action.
257 1 : void test_regex4()
258 : {
259 : const std::string SPEC =
260 : "act a_out, b_out;\n"
261 1 : "init a_out . b_out . delta;";
262 :
263 1 : stochastic_specification spec = lps::linearise(SPEC);
264 : // This should rename both actions to 'out'
265 2 : stochastic_specification new_spec = action_rename(std::regex("^(a|b)_out$"), "out", spec);
266 :
267 1 : BOOST_CHECK(new_spec.action_labels().size() == 1);
268 1 : BOOST_CHECK(std::string(new_spec.action_labels().front().name()) == "out");
269 1 : }
270 :
271 2 : BOOST_AUTO_TEST_CASE(multiple_action_declarations)
272 : {
273 : const std::string SPEC =
274 : "act a1,a2;\n"
275 : "proc P = a1.a2.P;\n"
276 1 : "init P;\n";
277 :
278 : const std::string RENAME_SPEC =
279 : "act b1;\n"
280 : "rename a1 => b1;\n"
281 : "act b2;\n"
282 1 : "rename a2 => b2;\n";
283 :
284 1 : stochastic_specification spec = lps::linearise(SPEC);
285 1 : std::istringstream ar_spec_stream(RENAME_SPEC);
286 1 : action_rename_specification ar_spec = parse_action_rename_specification(ar_spec_stream, spec);
287 2 : stochastic_specification new_spec = action_rename(ar_spec,spec,data::rewriter(),false);
288 :
289 1 : BOOST_CHECK(new_spec.action_labels().size() == 4);
290 1 : }
291 :
292 2 : BOOST_AUTO_TEST_CASE(test_main)
293 : {
294 1 : test1();
295 1 : test2();
296 1 : test3();
297 1 : test4();
298 1 : test5();
299 :
300 1 : test_regex1();
301 1 : test_regex2();
302 1 : test_regex3();
303 1 : test_regex4();
304 1 : }
|
