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 replace_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE replace_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/parse.h"
16 : #include "mcrl2/data/replace.h"
17 : #include "mcrl2/data/substitutions/assignment_sequence_substitution.h"
18 : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
19 : #include "mcrl2/data/substitutions/sequence_sequence_substitution.h"
20 :
21 : using namespace mcrl2;
22 :
23 : inline
24 584 : data::variable bool_(const std::string& name)
25 : {
26 1168 : return data::variable(core::identifier_string(name), data::sort_bool::bool_());
27 : }
28 :
29 : inline
30 : data::variable nat(const std::string& name)
31 : {
32 : return data::variable(core::identifier_string(name), data::sort_nat::nat());
33 : }
34 :
35 : inline
36 : data::variable pos(const std::string& name)
37 : {
38 : return data::variable(core::identifier_string(name), data::sort_pos::pos());
39 : }
40 :
41 : inline
42 20 : std::vector<data::variable> variable_context()
43 : {
44 : return std::vector<data::variable>
45 : {
46 : bool_("b"),
47 : bool_("b1"),
48 : bool_("b2"),
49 : bool_("b3"),
50 : bool_("b4"),
51 : bool_("k"),
52 : bool_("m"),
53 : bool_("n"),
54 : bool_("v"),
55 : bool_("w"),
56 : bool_("x"),
57 : bool_("y"),
58 : bool_("z"),
59 : bool_("k1"),
60 : bool_("m1"),
61 : bool_("n1"),
62 : bool_("v1"),
63 : bool_("w1"),
64 : bool_("x1"),
65 : bool_("y1"),
66 : bool_("z1"),
67 : bool_("k2"),
68 : bool_("m2"),
69 : bool_("n2"),
70 : bool_("v2"),
71 : bool_("w2"),
72 : bool_("x2"),
73 : bool_("y2"),
74 : bool_("z2")
75 600 : };
76 : }
77 :
78 : inline
79 10 : data::data_expression parse_data_expression(const std::string& text)
80 : {
81 20 : return data::parse_data_expression(text, variable_context());
82 : };
83 :
84 : /// \brief Parses a string of the form "b: Bool := v, c: Bool := !w", and adds
85 : inline
86 10 : data::mutable_map_substitution<> parse_substitution(const std::string& text, const std::vector<data::variable>& variables = variable_context())
87 : {
88 10 : data::mutable_map_substitution<> sigma;
89 20 : std::vector<std::string> substitutions = utilities::split(text, ";");
90 20 : for (const std::string& substitution: substitutions)
91 : {
92 20 : std::vector<std::string> words = utilities::regex_split(substitution, ":=");
93 10 : if (words.size() != 2)
94 : {
95 0 : continue;
96 : }
97 10 : data::variable v = data::parse_variable(words[0]);
98 10 : data::data_expression e = data::parse_data_expression(words[1], variables);
99 10 : sigma[v] = e;
100 10 : }
101 20 : return sigma;
102 10 : }
103 :
104 2 : BOOST_AUTO_TEST_CASE(test_assignment_list)
105 : {
106 : using namespace mcrl2::data::sort_bool;
107 :
108 2 : data::variable d1("d1", data::basic_sort("D"));
109 2 : data::variable d2("d2", data::basic_sort("D"));
110 2 : data::variable d3("d3", data::basic_sort("D"));
111 2 : data::variable e1("e1", data::basic_sort("D"));
112 2 : data::variable e2("e2", data::basic_sort("D"));
113 2 : data::variable e3("e3", data::basic_sort("D"));
114 :
115 1 : data::assignment_vector l;
116 1 : l.push_back(data::assignment(d1, e1));
117 1 : l.push_back(data::assignment(e1, e2));
118 1 : l.push_back(data::assignment(e2, e3));
119 :
120 2 : data::data_expression t = and_(equal_to(d1, e1), not_equal_to(e2, d3));
121 2 : data::data_expression t0 = and_(equal_to(e1, e2), not_equal_to(e3, d3));
122 1 : data::data_expression t2 = data::replace_variables(t, data::assignment_sequence_substitution(data::assignment_list(l.begin(), l.end())));
123 1 : BOOST_CHECK(t0 == t2);
124 1 : }
125 :
126 2 : BOOST_AUTO_TEST_CASE(test_variable_replace)
127 : {
128 : using namespace mcrl2::data::sort_bool;
129 :
130 2 : data::variable d1("d1", data::basic_sort("D"));
131 2 : data::variable d2("d2", data::basic_sort("D"));
132 2 : data::variable d3("d3", data::basic_sort("D"));
133 2 : data::variable x("x", data::basic_sort("D"));
134 2 : data::variable y("y", data::basic_sort("D"));
135 2 : data::variable z("z", data::basic_sort("D"));
136 :
137 5 : data::variable_vector variables{d1, d2, d3};
138 5 : data::data_expression_vector replacements{x, y, z};
139 5 : std::vector<data::variable> v{d1, d2, d3};
140 5 : std::list<data::data_expression> l{x, y, z};
141 :
142 2 : data::data_expression t = and_(equal_to(d1, d2), not_equal_to(d2, d3));
143 1 : data::data_expression t1 = data::replace_variables(t, make_sequence_sequence_substitution(variables, replacements));
144 1 : data::data_expression t2 = data::replace_variables(t, make_sequence_sequence_substitution(v, l));
145 1 : BOOST_CHECK(t1 == t2);
146 :
147 1 : t = and_(equal_to(d1, d2), not_equal_to(d2, d3));
148 1 : BOOST_CHECK(t1 == replace_variables(t, make_sequence_sequence_substitution(variables, replacements)));
149 1 : BOOST_CHECK(t1 == replace_variables(t, make_sequence_sequence_substitution(variables, replacements)));
150 1 : BOOST_CHECK(t1 == replace_variables(t, make_sequence_sequence_substitution(v, l)));
151 1 : BOOST_CHECK(t1 == replace_variables(t, make_mutable_map_substitution(variables, replacements)));
152 1 : }
153 :
154 2 : BOOST_AUTO_TEST_CASE(test_replace_with_binders)
155 : {
156 1 : data::mutable_map_substitution< > sigma;
157 2 : data::data_expression input1(data::variable("c", data::sort_bool::bool_()));
158 2 : data::data_expression input2(data::parse_data_expression("exists b: Bool, c: Bool. if(b, c, b)"));
159 :
160 1 : sigma[data::variable("c", data::sort_bool::bool_())] = data::sort_bool::false_();
161 :
162 1 : BOOST_CHECK(replace_free_variables(input1, sigma) == data::sort_bool::false_());
163 :
164 : // variable c is bound and should not be replaced
165 1 : BOOST_CHECK(replace_free_variables(input2, sigma) == input2);
166 1 : }
167 :
168 2 : BOOST_AUTO_TEST_CASE(test_variables)
169 : {
170 2 : data::variable d1 = bool_("d1");
171 2 : data::variable d2 = bool_("d2");
172 2 : data::variable d3 = bool_("d3");
173 2 : data::variable d4 = bool_("d4");
174 1 : data::data_expression e1 = data::sort_bool::not_(d1);
175 1 : data::data_expression e2 = data::sort_bool::not_(d2);
176 1 : data::data_expression e3 = data::sort_bool::not_(d3);
177 :
178 1 : data::mutable_map_substitution<> sigma;
179 1 : sigma[d1] = e1;
180 1 : sigma[d2] = e2;
181 1 : sigma[d3] = e3;
182 :
183 : // the variable in an assignment is not replaced by replace_free_variables
184 1 : data::assignment a(d1, d4);
185 1 : data::assignment b = replace_free_variables(a, sigma);
186 1 : BOOST_CHECK(b == a);
187 :
188 : // the variable in an assignment is not replaced by replace_variables
189 1 : data::assignment c = replace_variables(a, sigma);
190 1 : BOOST_CHECK(c == a);
191 :
192 : // the variable d1 in the right hand side is replaced by replace_free_variables, since
193 : // we do not consider the left hand side a binding variable
194 1 : a = data::assignment(d1, data::sort_bool::and_(d1, d2));
195 1 : b = replace_free_variables(a, sigma);
196 1 : BOOST_CHECK(b == data::assignment(d1, data::sort_bool::and_(e1, e2)));
197 :
198 : // the variable d1 in the right hand side is replaced by replace_free_variables
199 1 : c = replace_variables(a, sigma);
200 1 : BOOST_CHECK(c == data::assignment(d1, data::sort_bool::and_(e1, e2)));
201 :
202 : // this will lead to an assertion failure, because an attempt will be made to store
203 : // a data expression in a variable
204 1 : sigma[d1] = data::sort_bool::and_(d1, d2);
205 : // data::data_expression z1 = replace_variables(d1, sigma);
206 :
207 : // therefore one should first convert d1 to a data expression:
208 2 : data::data_expression z2 = replace_variables(data::data_expression(d1), sigma);
209 1 : BOOST_CHECK(z2 == data::sort_bool::and_(d1, d2));
210 1 : }
211 :
212 10 : void check_result(const std::string& expression, const std::string& result, const std::string& expected_result, const std::string& title)
213 : {
214 10 : if (result != expected_result)
215 : {
216 0 : std::cout << "--- failure in " << title << " ---" << std::endl;
217 0 : std::cout << "expression = " << expression << std::endl;
218 0 : BOOST_CHECK_EQUAL(result, expected_result);
219 : }
220 10 : }
221 :
222 10 : void test_replace_variables_capture_avoiding(const std::string& x_text, const std::string& sigma_text, const std::string& expected_result)
223 : {
224 10 : data::data_expression x = parse_data_expression(x_text);
225 10 : data::mutable_map_substitution<> sigma = parse_substitution(sigma_text);
226 10 : std::string result = data::pp(data::replace_variables_capture_avoiding(x, sigma));
227 10 : check_result(x_text + " sigma = " + sigma_text, result, expected_result, "replace_variables_capture_avoiding");
228 10 : }
229 :
230 2 : BOOST_AUTO_TEST_CASE(replace_variables_capture_avoiding_test)
231 : {
232 1 : test_replace_variables_capture_avoiding("v", "v: Bool := w", "w");
233 1 : test_replace_variables_capture_avoiding("forall x: Bool . x => y", "x: Bool := z", "forall x1: Bool. x1 => y");
234 1 : test_replace_variables_capture_avoiding("forall x: Bool . x => y", "y: Bool := z", "forall x1: Bool. x1 => z");
235 1 : test_replace_variables_capture_avoiding("forall x: Bool . x => y", "y: Bool := x", "forall x1: Bool. x1 => x");
236 1 : test_replace_variables_capture_avoiding("forall x: Bool . x => x1 => y", "y: Bool := x", "forall x2: Bool. x2 => x1 => x");
237 1 : test_replace_variables_capture_avoiding("x => x1 => y whr x = y end", "y: Bool := x", "x2 => x1 => x whr x2 = x end");
238 1 : test_replace_variables_capture_avoiding("forall n: Bool. n => forall k: Bool. k => m", "m: Bool := n", "forall n1: Bool. n1 => (forall k1: Bool. k1 => n)");
239 1 : test_replace_variables_capture_avoiding("forall n: Bool. n => forall n: Bool. n => m", "m: Bool := n", "forall n1: Bool. n1 => (forall n2: Bool. n2 => n)");
240 1 : test_replace_variables_capture_avoiding("forall n: Bool. n => forall k: Bool. k => m", "m: Bool := n", "forall n1: Bool. n1 => (forall k1: Bool. k1 => n)");
241 1 : test_replace_variables_capture_avoiding("forall n: Bool. n => forall n: Bool. n => m", "m: Bool := n", "forall n1: Bool. n1 => (forall n2: Bool. n2 => n)");
242 1 : }
243 :
244 2 : BOOST_AUTO_TEST_CASE(test_replace_free_variables)
245 : {
246 1 : data::mutable_map_substitution<> sigma;
247 2 : data::variable x("x", data::sort_bool::bool_());
248 1 : data::data_expression y = data::sort_bool::not_(x);
249 1 : sigma[x] = y;
250 1 : data::assignment a(x, x);
251 1 : data::assignment b(x, y);
252 1 : data::assignment c = data::replace_free_variables(a, sigma);
253 1 : BOOST_CHECK(b == c);
254 :
255 2 : data::assignment_list va{a};
256 2 : data::assignment_list vb{b};
257 1 : data::assignment_list vc = data::replace_free_variables(va, sigma);
258 1 : BOOST_CHECK_EQUAL(vb, vc);
259 1 : }
260 :
261 2 : BOOST_AUTO_TEST_CASE(test_ticket_1209)
262 : {
263 1 : std::string text = "n whr n = m, m = 3 end whr m = 255 end";
264 1 : std::string expected_result = "n1 whr n1 = m2, m3 = 3 end whr m2 = 255 end";
265 1 : data::data_expression x = data::parse_data_expression(text);
266 1 : data::mutable_map_substitution<> sigma;
267 2 : data::variable m("m", data::sort_pos::pos());
268 2 : data::variable m1("m1", data::sort_pos::pos());
269 1 : sigma[m] = m1;
270 1 : data::data_expression x1 = data::replace_variables_capture_avoiding(x, sigma);
271 1 : std::string result = data::pp(x1);
272 1 : BOOST_CHECK_EQUAL(result, expected_result);
273 1 : }
|