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 pbes_expression_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE pbes_expression_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/pbes/find.h"
16 : #include "mcrl2/pbes/join.h"
17 : #include "mcrl2/pbes/detail/parse.h"
18 :
19 : using namespace mcrl2;
20 : using namespace mcrl2::pbes_system;
21 : using namespace mcrl2::pbes_system::detail;
22 :
23 2 : BOOST_AUTO_TEST_CASE(test_accessors)
24 : {
25 : using namespace mcrl2::pbes_system::accessors;
26 :
27 : std::string EXPRESSIONS =
28 : "datavar \n"
29 : " n: Nat; \n"
30 : " \n"
31 : "predvar \n"
32 : " \n"
33 : "expressions \n"
34 : " val(n > 2); \n"
35 1 : " val(n > 3) \n"
36 : ;
37 :
38 2 : std::vector<pbes_expression> expressions = parse_pbes_expressions(EXPRESSIONS).first;
39 1 : pbes_expression x = expressions[0];
40 1 : pbes_expression y = expressions[1];
41 2 : data::variable d(core::identifier_string("d"), data::sort_nat::nat());
42 2 : data::variable_list v = { d };
43 1 : pbes_expression z = d;
44 3 : propositional_variable_instantiation X(core::identifier_string("X"), { d });
45 :
46 1 : std::set<pbes_expression> q;
47 1 : q.insert(x);
48 1 : q.insert(y);
49 1 : q.insert(z);
50 :
51 : {
52 : using namespace mcrl2::pbes_system::accessors;
53 :
54 1 : pbes_expression a, b, c;
55 1 : data::variable_list w;
56 1 : core::identifier_string s;
57 1 : data::data_expression e;
58 1 : std::set<pbes_expression> q1;
59 :
60 1 : a = not_(x);
61 1 : b = arg(a);
62 1 : BOOST_CHECK(x == b);
63 :
64 1 : a = and_(x, y);
65 1 : b = left(a);
66 1 : c = right(a);
67 1 : BOOST_CHECK(x == b);
68 1 : BOOST_CHECK(y == c);
69 :
70 1 : a = or_(x, y);
71 1 : b = left(a);
72 1 : c = right(a);
73 1 : BOOST_CHECK(x == b);
74 1 : BOOST_CHECK(y == c);
75 :
76 1 : a = imp(x, y);
77 1 : b = left(a);
78 1 : c = right(a);
79 1 : BOOST_CHECK(x == b);
80 1 : BOOST_CHECK(y == c);
81 :
82 1 : a = forall(v, x);
83 1 : w = var(a);
84 1 : b = arg(a);
85 1 : BOOST_CHECK(v == w);
86 1 : BOOST_CHECK(x == b);
87 :
88 1 : a = exists(v, x);
89 1 : w = var(a);
90 1 : b = arg(a);
91 1 : BOOST_CHECK(v == w);
92 1 : BOOST_CHECK(x == b);
93 :
94 1 : s = name(X);
95 1 : BOOST_CHECK(s == core::identifier_string("X"));
96 :
97 1 : const data::data_expression_list& f = param(X);
98 3 : data::data_expression_list g = { d };
99 1 : BOOST_CHECK(f == g);
100 :
101 1 : a = join_or(q.begin(), q.end());
102 1 : q1 = split_or(a);
103 1 : BOOST_CHECK(q == q1);
104 :
105 1 : a = join_and(q.begin(), q.end());
106 1 : q1 = split_and(a);
107 1 : BOOST_CHECK(q == q1);
108 1 : }
109 :
110 : {
111 1 : pbes_expression a;
112 1 : core::identifier_string s;
113 1 : data::data_expression e;
114 1 : std::set<pbes_expression> q1;
115 :
116 1 : a = not_(x);
117 1 : a = and_(x, y);
118 1 : a = or_(x, y);
119 1 : a = imp(x, y);
120 1 : a = forall(v, x);
121 1 : a = exists(v, x);
122 1 : s = name(X);
123 1 : param(X);
124 1 : a = join_or(q.begin(), q.end());
125 1 : a = join_and(q.begin(), q.end());
126 1 : q1 = split_or(a);
127 1 : q1 = split_and(a);
128 1 : }
129 1 : }
130 :
131 2 : BOOST_AUTO_TEST_CASE(test_term_traits)
132 : {
133 : typedef core::term_traits<pbes_expression> tr;
134 :
135 : const std::string VARSPEC =
136 : "datavar \n"
137 : " m: Nat; \n"
138 : " n: Nat; \n"
139 : " b: Bool; \n"
140 : " c: Bool; \n"
141 : " \n"
142 : "predvar \n"
143 : " X: Bool, Pos; \n"
144 1 : " Y: Nat; \n"
145 : ;
146 :
147 1 : pbes_expression x, y, z;
148 1 : data::variable_list v;
149 1 : data::data_expression_list e;
150 :
151 : // and 1
152 1 : x = parse_pbes_expression("Y(1) && Y(2)", VARSPEC);
153 1 : z = pbes_system::accessors::left(x);
154 1 : z = pbes_system::accessors::right(x);
155 :
156 : // and 2
157 1 : x = parse_pbes_expression("val(b && c)", VARSPEC);
158 1 : if (tr::is_and(x))
159 : {
160 0 : BOOST_CHECK(false);
161 0 : z = pbes_system::accessors::left(x);
162 0 : z = pbes_system::accessors::right(x);
163 : }
164 :
165 : // or 1
166 1 : x = parse_pbes_expression("Y(1) || Y(2)", VARSPEC);
167 1 : z = pbes_system::accessors::left(x);
168 1 : z = pbes_system::accessors::right(x);
169 :
170 : // or 2
171 1 : x = parse_pbes_expression("val(b || c)", VARSPEC);
172 1 : if (tr::is_or(x))
173 : {
174 0 : BOOST_CHECK(false);
175 0 : z = pbes_system::accessors::left(x);
176 0 : z = pbes_system::accessors::right(x);
177 : }
178 :
179 : // imp 1
180 1 : x = parse_pbes_expression("Y(1) => !Y(2)", VARSPEC);
181 1 : z = pbes_system::accessors::left(x);
182 1 : z = pbes_system::accessors::right(x);
183 :
184 : // imp 2
185 1 : x = parse_pbes_expression("val(b => c)", VARSPEC);
186 1 : if (tr::is_imp(x))
187 : {
188 0 : BOOST_CHECK(false);
189 0 : z = pbes_system::accessors::left(x);
190 0 : z = pbes_system::accessors::right(x);
191 : }
192 :
193 : // not 1
194 1 : x = parse_pbes_expression("!(Y(1) || Y(2))", VARSPEC);
195 1 : z = pbes_system::accessors::arg(x);
196 :
197 : // not 2
198 1 : x = parse_pbes_expression("!val(n < 10)", VARSPEC);
199 1 : z = pbes_system::accessors::arg(x);
200 :
201 : // not 3
202 1 : x = parse_pbes_expression("val(!(n < 10))", VARSPEC);
203 1 : if (tr::is_not(x))
204 : {
205 0 : BOOST_CHECK(false);
206 0 : z = pbes_system::accessors::arg(x);
207 : }
208 :
209 : // prop var 1
210 1 : x = parse_pbes_expression("Y(1)", VARSPEC);
211 1 : e = atermpp::down_cast<propositional_variable_instantiation>(x).parameters();
212 :
213 : // forall 1
214 1 : x = parse_pbes_expression("forall k:Nat.Y(k)", VARSPEC);
215 1 : v = tr::var(x);
216 1 : z = pbes_system::accessors::arg(x);
217 :
218 : // exists 1
219 1 : x = parse_pbes_expression("exists k:Nat.Y(k)", VARSPEC);
220 1 : v = tr::var(x);
221 1 : z = pbes_system::accessors::arg(x);
222 1 : }
|
