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 rewriter_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE rewriter_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/detail/parse_substitution.h"
16 : #include "mcrl2/lps/detail/specification_property_map.h"
17 : #include "mcrl2/lps/one_point_rule_rewrite.h"
18 : #include "mcrl2/lps/parse.h"
19 : #include "mcrl2/lps/rewrite.h"
20 :
21 : using namespace mcrl2;
22 : using namespace mcrl2::data;
23 : using namespace mcrl2::data::detail;
24 : using namespace mcrl2::lps;
25 : using namespace mcrl2::lps::detail;
26 :
27 : const std::string SPECIFICATION1 =
28 : "sort Natural; \n"
29 : " \n"
30 : "cons _0: Natural; \n"
31 : " S: Natural -> Natural; \n"
32 : " \n"
33 : "map eq: Natural # Natural -> Bool; \n"
34 : " less: Natural # Natural -> Bool; \n"
35 : " plus: Natural # Natural -> Natural; \n"
36 : " _1, _2, _3, _4, _5, _6, _7, _8, _9: Natural; \n"
37 : " P: Natural -> Natural; \n"
38 : " even: Natural -> Bool; \n"
39 : " \n"
40 : "var n, m: Natural; \n"
41 : " \n"
42 : "eqn eq(n, n) = true; \n"
43 : " eq(S(n), _0) = false; \n"
44 : " eq(_0, S(m)) = false; \n"
45 : " eq(S(n), S(m)) = eq(n, m); \n"
46 : " \n"
47 : " less(n, n) = false; \n"
48 : " less(n, _0) = false; \n"
49 : " less(_0, S(m)) = true; \n"
50 : " less(S(n), S(m)) = less(n, m); \n"
51 : " \n"
52 : " plus(_0, n) = n; \n"
53 : " plus(n, _0) = n; \n"
54 : " plus(S(n), m) = S(plus(n, m)); \n"
55 : " plus(n, S(m)) = S(plus(n, m)); \n"
56 : " \n"
57 : " even(_0) = true; \n"
58 : " even(S(n)) = !(even(n)); \n"
59 : " \n"
60 : " P(S(n)) = n; \n"
61 : " \n"
62 : " _1 = S(_0); \n"
63 : " _2 = S(_1); \n"
64 : " _3 = S(_2); \n"
65 : " _4 = S(_3); \n"
66 : " _5 = S(_4); \n"
67 : " _6 = S(_5); \n"
68 : " _7 = S(_6); \n"
69 : " _8 = S(_7); \n"
70 : " _9 = S(_8); \n"
71 : " \n"
72 : "act a: Natural; \n"
73 : " \n"
74 : "proc P(n: Natural) = sum m: Natural. a(m). P(m); \n"
75 : " \n"
76 : "init P(_0); \n"
77 : ;
78 :
79 1 : void test1()
80 : {
81 1 : specification spec = parse_linear_process_specification(SPECIFICATION1);
82 1 : rewriter r(spec.data());
83 :
84 2 : data_expression n1 = find_mapping(spec.data(), "_1");
85 2 : data_expression n2 = find_mapping(spec.data(), "_2");
86 2 : data_expression n3 = find_mapping(spec.data(), "_3");
87 2 : data_expression n4 = find_mapping(spec.data(), "_4");
88 2 : data_expression n5 = find_mapping(spec.data(), "_5");
89 2 : data_expression n6 = find_mapping(spec.data(), "_6");
90 2 : data_expression n7 = find_mapping(spec.data(), "_7");
91 2 : data_expression n8 = find_mapping(spec.data(), "_8");
92 2 : data_expression n9 = find_mapping(spec.data(), "_9");
93 2 : data_expression plus = find_mapping(spec.data(), "plus");
94 :
95 1 : BOOST_CHECK(r(plus(n4, n5)) == r(plus(n2, n7)));
96 :
97 1 : specification spec1 = spec;
98 1 : lps::rewrite(spec1, r);
99 1 : lps::detail::specification_property_map<> info(spec);
100 1 : lps::detail::specification_property_map<> info1(spec1);
101 1 : BOOST_CHECK(info.to_string() == info1.to_string());
102 :
103 : // test destructor
104 1 : const rewriter& r1 = r;
105 1 : BOOST_CHECK(r1(n1)==r(n1));
106 1 : }
107 :
108 : const std::string SPECIFICATION2=
109 : "act c:Pos#Nat; \n"
110 : "proc P(a:Pos,b:Nat)=c(a,0).P(a+1,b+1+2); \n"
111 : "init P(1+1,2+2); \n";
112 :
113 1 : void test2()
114 : {
115 1 : specification spec = parse_linear_process_specification(SPECIFICATION2);
116 1 : rewriter r(spec.data());
117 :
118 1 : specification spec1 = spec;
119 1 : lps::rewrite(spec1, r);
120 :
121 1 : specification spec2 = spec1;
122 1 : lps::rewrite(spec2, r);
123 :
124 1 : lps::detail::specification_property_map<> info1(spec1);
125 1 : lps::detail::specification_property_map<> info2(spec2);
126 1 : BOOST_CHECK(info1.to_string() == info2.to_string());
127 1 : BOOST_CHECK(spec1.process().summand_count() == 1);
128 1 : }
129 :
130 : const std::string SPECIFICATION3 =
131 : "act c:Pos#Nat; \n"
132 : "proc P(a:Pos,b:Nat)=tau.P(a+1,b+1+2)+ \n"
133 : " tau.P(a+1,pred(a))+ \n"
134 : " c(a,0).P(a,b); \n"
135 : "init P(1+1,0); \n";
136 1 : void test3()
137 : {
138 1 : specification spec = parse_linear_process_specification(SPECIFICATION3);
139 1 : rewriter r(spec.data());
140 :
141 1 : specification spec1 = spec;
142 1 : lps::rewrite(spec1, r);
143 :
144 1 : specification spec2 = spec1;
145 1 : lps::rewrite(spec2, r);
146 :
147 1 : lps::detail::specification_property_map<> info1(spec1);
148 1 : lps::detail::specification_property_map<> info2(spec2);
149 1 : BOOST_CHECK(info1.to_string() == info2.to_string());
150 1 : BOOST_CHECK(spec1.process().summand_count() == 3);
151 1 : }
152 :
153 : // Checks if rewriting the specification src with the substitutions sigma
154 : // results in the specification dest.
155 1 : void test_lps_rewriter(const std::string& src_text, const std::string& dest_text, const std::string& sigma_text)
156 : {
157 1 : lps::specification src = parse_linear_process_specification(src_text);
158 1 : lps::specification dest = parse_linear_process_specification(dest_text);
159 :
160 : // rewrite the specification src
161 1 : data::rewriter R(src.data());
162 1 : data::mutable_map_substitution<> sigma;
163 1 : data::detail::parse_substitution(sigma_text, sigma, src.data());
164 1 : lps::rewrite(src, R, sigma);
165 :
166 1 : if (src != dest)
167 : {
168 0 : std::cerr << "--- test failed ---" << std::endl;
169 0 : std::cerr << lps::pp(src) << std::endl;
170 0 : std::cerr << "-------------------" << std::endl;
171 0 : std::cerr << lps::pp(dest) << std::endl;
172 : }
173 1 : BOOST_CHECK(src == dest);
174 1 : }
175 :
176 1 : void test_lps_rewriter()
177 : {
178 : std::string src =
179 : "act c: Bool; \n"
180 : "proc P(b: Bool, c:Bool) = c(true && false).P(b || true, c && true); \n"
181 1 : "init P(true || false, true && false); \n";
182 :
183 : std::string dest =
184 : "act c: Bool; \n"
185 : "proc P(b: Bool, c:Bool) = c(false).P(true, c); \n"
186 1 : "init P(true, false); \n";
187 :
188 1 : test_lps_rewriter(src, dest, "");
189 1 : }
190 :
191 1 : void test_one_point_rule_rewriter()
192 : {
193 : std::string src =
194 : "act a: Bool;\n"
195 : "\n"
196 : "proc P(b: Bool) =\n"
197 : " (forall n: Nat. n != 1 || b) ->\n"
198 : " a(exists m: Nat. m == 1) .\n"
199 : " P(b = b);\n"
200 : "\n"
201 1 : "init P(true);";
202 :
203 : std::string expected_result =
204 : "act a: Bool;\n"
205 : "\n"
206 : "proc P(b: Bool) =\n"
207 : " (1 != 1 || b) ->\n"
208 : " a(1 == 1) .\n"
209 : " P(b = b);\n"
210 : "\n"
211 1 : "init P(true);";
212 :
213 1 : specification lpsspec = parse_linear_process_specification(src);
214 1 : specification expected_spec = parse_linear_process_specification(expected_result);
215 1 : lps::one_point_rule_rewrite(lpsspec);
216 2 : std::string result = utilities::trim_copy(lps::pp(lpsspec));
217 1 : BOOST_CHECK(result == expected_result);
218 1 : }
219 :
220 2 : BOOST_AUTO_TEST_CASE(test_main)
221 : {
222 1 : test1();
223 1 : test2();
224 1 : test3();
225 1 : test_lps_rewriter();
226 1 : test_one_point_rule_rewriter();
227 1 : }
|
