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 gauss_elimination_test.cpp
10 : /// \brief Gauss elimination tests.
11 :
12 : #define BOOST_TEST_MODULE gauss_elimination_test
13 : #define MCRL2_GAUSS_ELIMINATION_DEBUG
14 : #include <boost/test/included/unit_test.hpp>
15 :
16 : #include "mcrl2/lps/detail/test_input.h"
17 : #include "mcrl2/modal_formula/parse.h"
18 : #include "mcrl2/pbes/pbes_gauss_elimination.h"
19 : #include "mcrl2/pbes/lps2pbes.h"
20 : #include "mcrl2/pbes/pbes_gauss_elimination.h"
21 : #include "mcrl2/pbes/rewriter.h"
22 : #include "mcrl2/pbes/txt2pbes.h"
23 :
24 :
25 : using namespace mcrl2;
26 : using namespace mcrl2::pbes_system;
27 :
28 : std::string BES1 =
29 : "pbes mu X = X; \n"
30 : " \n"
31 : "init X; \n"
32 : ;
33 :
34 : std::string BES2 =
35 : "pbes nu X = X; \n"
36 : " \n"
37 : "init X; \n"
38 : ;
39 :
40 : std::string BES3 =
41 : "pbes mu X = Y; \n"
42 : " nu Y = X; \n"
43 : " \n"
44 : "init X; \n"
45 : ;
46 :
47 : std::string BES4 =
48 : "pbes nu Y = X; \n"
49 : " mu X = Y; \n"
50 : " \n"
51 : "init X; \n"
52 : ;
53 :
54 : std::string BES5 =
55 : "pbes mu X1 = X2; \n"
56 : " nu X2 = X1 || X3; \n"
57 : " mu X3 = X4 && X5; \n"
58 : " nu X4 = X1; \n"
59 : " nu X5 = X1 || X3; \n"
60 : " \n"
61 : "init X1; \n"
62 : ;
63 :
64 : std::string BES6 =
65 : "pbes nu X1 = X2 && X1; \n"
66 : " mu X2 = X1 || X3; \n"
67 : " nu X3 = X3; \n"
68 : " \n"
69 : "init X1; \n"
70 : ;
71 :
72 : std::string BES7 =
73 : "pbes nu X1 = X2 && X3; \n"
74 : " nu X2 = X4 && X5; \n"
75 : " nu X3 = true; \n"
76 : " nu X4 = false; \n"
77 : " nu X5 = X6; \n"
78 : " nu X6 = X5; \n"
79 : " \n"
80 : "init X1; \n"
81 : ;
82 :
83 : std::string BES8 =
84 : "pbes nu X1 = X2 && X1; \n"
85 : " mu X2 = X1; \n"
86 : " \n"
87 : "init X1; \n"
88 : ;
89 :
90 : std::string BES9 =
91 : "pbes mu X = false; \n"
92 : " \n"
93 : "init X; \n"
94 : ;
95 :
96 : std::string BES10 =
97 : "pbes nu X = false; \n"
98 : " \n"
99 : "init X; \n"
100 : ;
101 :
102 10 : void test_bes(const std::string& bes_spec, bool expected_result)
103 : {
104 10 : pbes_system::pbes p = pbes_system::txt2pbes(bes_spec);
105 10 : int result = pbes_system::gauss_elimination(p);
106 10 : switch (result)
107 : {
108 6 : case 0:
109 6 : std::cout << "FALSE" << std::endl;
110 6 : break;
111 4 : case 1:
112 4 : std::cout << "true" << std::endl;
113 4 : break;
114 0 : case 2:
115 0 : std::cout << "UNKNOWN" << std::endl;
116 0 : break;
117 : }
118 10 : BOOST_CHECK((!expected_result && result == 0) || (expected_result && result == 1));
119 :
120 : // BOOST_CHECK(pbes2bool(p) == expected_result);
121 : // this gives assertion failures in pbes2bool
122 :
123 10 : }
124 :
125 1 : void test_bes_examples()
126 : {
127 1 : test_bes(BES1, false);
128 1 : test_bes(BES2, true);
129 1 : test_bes(BES3, false);
130 1 : test_bes(BES4, true);
131 1 : test_bes(BES5, false);
132 1 : test_bes(BES6, true);
133 1 : test_bes(BES7, false);
134 1 : test_bes(BES8, true);
135 1 : test_bes(BES9, false);
136 1 : test_bes(BES10, false);
137 1 : }
138 :
139 1 : void test_abp()
140 : {
141 1 : bool timed = false;
142 1 : std::string FORMULA = "[true*]<true*>true";
143 2 : lps::specification spec=remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
144 1 : state_formulas::state_formula formula = state_formulas::parse_state_formula(FORMULA, spec, false);
145 :
146 1 : pbes_system::pbes p = pbes_system::lps2pbes(spec, formula, timed);
147 1 : int result = pbes_system::gauss_elimination(p);
148 1 : switch (result)
149 : {
150 0 : case 0:
151 0 : std::cout << "FALSE" << std::endl;
152 0 : break;
153 1 : case 1:
154 1 : std::cout << "true" << std::endl;
155 1 : break;
156 0 : case 2:
157 0 : std::cout << "UNKNOWN" << std::endl;
158 0 : break;
159 : }
160 :
161 1 : }
162 :
163 1 : void test_bes()
164 : {
165 : using namespace pbes_system;
166 :
167 2 : propositional_variable X("X");
168 2 : propositional_variable Y("Y");
169 :
170 : // empty boolean equation system
171 1 : std::vector<pbes_equation> empty;
172 :
173 1 : pbes_system::fixpoint_symbol mu = pbes_system::fixpoint_symbol::mu();
174 1 : pbes_system::fixpoint_symbol nu = pbes_system::fixpoint_symbol::nu();
175 :
176 : // pbes mu X = X;
177 : //
178 : // init X;
179 1 : pbes_equation e1(mu, X, propositional_variable_instantiation(X.name()));
180 2 : pbes bes1(data::data_specification(), empty, propositional_variable_instantiation(X.name()));
181 1 : bes1.equations().push_back(e1);
182 :
183 : // pbes nu X = X;
184 : //
185 : // init X;
186 1 : pbes_equation e2(nu, X, propositional_variable_instantiation(X.name()));
187 2 : pbes bes2(data::data_specification(), empty, propositional_variable_instantiation(X.name()));
188 1 : bes2.equations().push_back(e2);
189 :
190 : // pbes mu X = Y;
191 : // nu Y = X;
192 : //
193 : // init X;
194 1 : pbes_equation e3(mu, X, propositional_variable_instantiation(Y.name()));
195 1 : pbes_equation e4(nu, Y, propositional_variable_instantiation(X.name()));
196 2 : pbes bes3(data::data_specification(), empty, propositional_variable_instantiation(X.name()));
197 1 : bes3.equations().push_back(e3);
198 1 : bes3.equations().push_back(e4);
199 :
200 : // pbes nu Y = X;
201 : // mu X = Y;
202 : //
203 : // init X;
204 2 : pbes bes4(data::data_specification(), empty, propositional_variable_instantiation(X.name()));
205 1 : bes4.equations().push_back(e4);
206 1 : bes4.equations().push_back(e3);
207 :
208 1 : BOOST_CHECK(!gauss_elimination(bes1));
209 1 : BOOST_CHECK(gauss_elimination(bes2));
210 1 : BOOST_CHECK(!gauss_elimination(bes3));
211 1 : BOOST_CHECK(gauss_elimination(bes4));
212 1 : }
213 :
214 : inline
215 3 : bool compare(const pbes_system::pbes_expression& x, const pbes_system::pbes_expression& y)
216 : {
217 3 : return x == y;
218 : }
219 :
220 : typedef bool (*compare_function)(const pbes_system::pbes_expression& x, const pbes_system::pbes_expression& y);
221 :
222 1 : void test_approximate()
223 : {
224 : using namespace pbes_system;
225 : typedef core::term_traits<pbes_expression> tr;
226 :
227 : gauss_elimination_algorithm<pbes_traits> algorithm;
228 1 : pbes_system::pbes p = pbes_system::txt2pbes(BES4);
229 1 : algorithm.run(p.equations().begin(), p.equations().end(), approximate<pbes_traits, compare_function > (compare));
230 1 : if (tr::is_false(p.equations().front().formula()))
231 : {
232 0 : std::cout << "FALSE" << std::endl;
233 : }
234 1 : else if (tr::is_true(p.equations().front().formula()))
235 : {
236 1 : std::cout << "true" << std::endl;
237 : }
238 : else
239 : {
240 0 : std::cout << "UNKNOWN" << std::endl;
241 : }
242 1 : }
243 :
244 : // simple solver that only works if the PBES is a BES
245 : struct fixpoint_equation_solver
246 : {
247 :
248 2 : void operator()(pbes_equation& e) const
249 : {
250 2 : pbes_expression phi = e.symbol().is_mu() ? false_() : true_();
251 2 : e.formula() = replace_propositional_variables(e.formula(), propositional_variable_substitution(e.variable(), phi));
252 2 : }
253 : };
254 :
255 1 : void tutorial1()
256 : {
257 : using namespace pbes_system;
258 :
259 : std::string txt =
260 : "pbes nu Y = X; \n"
261 : " mu X = Y; \n"
262 : " \n"
263 1 : "init X; \n"
264 : ;
265 1 : pbes p = txt2pbes(txt);
266 : gauss_elimination_algorithm<pbes_traits> algorithm;
267 1 : algorithm.run(p.equations().begin(), p.equations().end(), fixpoint_equation_solver());
268 1 : }
269 :
270 1 : void tutorial2()
271 : {
272 : using namespace pbes_system;
273 :
274 : std::string txt =
275 : "pbes mu X = X; \n"
276 : " \n"
277 1 : "init X; \n"
278 : ;
279 1 : pbes p = txt2pbes(txt);
280 1 : int solution = gauss_elimination(p);
281 1 : BOOST_CHECK(solution == 0); // 0 indicates false
282 1 : }
283 :
284 2 : BOOST_AUTO_TEST_CASE(test_main)
285 : {
286 1 : test_bes();
287 1 : test_abp();
288 1 : test_bes_examples();
289 1 : test_approximate();
290 1 : tutorial1();
291 1 : tutorial2();
292 1 : }
|
