Line data Source code
1 : // Author(s): Gijs Kant
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_explorer_test.cpp
10 : /// \brief Test for the PBES_Explorer interface.
11 :
12 : #include <boost/test/included/unit_test.hpp>
13 : #include "mcrl2/utilities/logger.h"
14 :
15 : #ifndef MCRL2_SKIP_LONG_TESTS
16 :
17 : #include "mcrl2/utilities/test_utilities.h"
18 : #include "mcrl2/pbes/normalize.h"
19 : #include "mcrl2/pbes/pbes_explorer.h"
20 : #include "mcrl2/pbes/txt2pbes.h"
21 :
22 : using namespace mcrl2;
23 : using namespace mcrl2::pbes_system;
24 : using namespace mcrl2::pbes_system::detail;
25 :
26 : namespace ltsmin
27 : {
28 :
29 : namespace test
30 : {
31 :
32 : class explorer : public mcrl2::pbes_system::explorer {
33 : private:
34 : std::set<std::vector<int> > visited;
35 : std::deque<std::vector<int> > fresh;
36 : std::size_t transition_count;
37 :
38 : public:
39 : #ifdef MCRL2_ENABLE_JITTYC
40 4 : explorer(const pbes& p, const std::string& rewrite_strategy = "jittyc", bool reset = false, bool always_split = false) :
41 : #else
42 : explorer(const pbes& p, const std::string& rewrite_strategy = "jitty", bool reset = false, bool always_split = false) :
43 : #endif
44 : mcrl2::pbes_system::explorer(p, rewrite_strategy, reset, always_split),
45 4 : transition_count(0)
46 4 : {}
47 :
48 2 : explorer(const std::string& f, const std::string& rewrite_strategy = "jittyc", bool reset = false, bool always_split = false) :
49 : mcrl2::pbes_system::explorer(f, rewrite_strategy, reset, always_split),
50 2 : transition_count(0)
51 2 : {}
52 :
53 : std::size_t get_state_count() const
54 : {
55 : return visited.size();
56 : }
57 :
58 : std::size_t get_transition_count() const
59 : {
60 : return transition_count;
61 : }
62 :
63 : const std::set<std::vector<int> >& get_visited() const
64 : {
65 : return visited;
66 : }
67 :
68 3366 : std::vector<int> to_int_vector(int size, int* data)
69 : {
70 3366 : std::vector<int> result;
71 16730 : for(int i=0; i < size; i++)
72 : {
73 : // testing serialisation/deserialisation
74 13364 : int type_no = this->get_info()->get_lts_type().get_state_type_no(i);
75 13364 : std::string s = this->get_value(type_no, data[i]);
76 : //std::clog << "Testing (de)serialisation of expression: " << s << std::endl;
77 13364 : int index = this->get_index(type_no, s);
78 13364 : BOOST_CHECK(index==data[i]);
79 :
80 13364 : result.push_back(data[i]);
81 13364 : }
82 3366 : return result;
83 0 : }
84 :
85 866 : void from_int_vector(int size, std::vector<int> data, int* dst)
86 : {
87 866 : BOOST_CHECK(size==(int)data.size());
88 866 : auto it = data.begin();
89 4302 : for(int i=0; i < size; i++, it++)
90 : {
91 3436 : dst[i] = *it;
92 : }
93 866 : }
94 :
95 : template <typename callback>
96 4302 : void next_state_long(int* const& src, std::size_t group, callback& f)
97 : {
98 4302 : mcrl2::pbes_system::explorer::next_state_long(src, group, f);
99 4302 : }
100 :
101 : template <typename callback>
102 866 : void next_state_all(int* const& src, callback& f)
103 : {
104 866 : mcrl2::pbes_system::explorer::next_state_all(src, f);
105 866 : }
106 :
107 6 : void initial_state(int* state)
108 : {
109 6 : mcrl2::pbes_system::explorer::initial_state(state);
110 6 : }
111 :
112 : int state_label(int label, int* const& s)
113 : {
114 : std::string varname = this->get_string_value(s[0]);
115 : if (label==0)
116 : {
117 : int priority = map_at(this->get_info()->get_variable_priorities(), varname);
118 : return priority;
119 : }
120 : else if (label==1)
121 : {
122 : lts_info::operation_type type = map_at(this->get_info()->get_variable_types(), varname);
123 : return type==parity_game_generator::PGAME_AND ? 1 : 0;
124 : }
125 : return 0;
126 : }
127 :
128 : void bfs();
129 : };
130 :
131 : struct pbes_state_cb
132 : {
133 : ltsmin::test::explorer* explorer;
134 : std::vector<std::vector<int> > successors;
135 : std::size_t count;
136 :
137 5168 : pbes_state_cb (ltsmin::test::explorer* explorer_)
138 5168 : : explorer(explorer_), count(0)
139 5168 : {}
140 :
141 3360 : void operator()(int* const& next_state,
142 : int group = -1)
143 : {
144 3360 : int state_length = explorer->get_info()->get_lts_type().get_state_length();
145 3360 : successors.push_back(explorer->to_int_vector(state_length, next_state));
146 3360 : count++;
147 3360 : }
148 :
149 5168 : const std::vector<std::vector<int> >& get_successors() const
150 : {
151 5168 : return successors;
152 : }
153 :
154 : std::size_t get_count() const
155 : {
156 : return count;
157 : }
158 : };
159 :
160 6 : void explorer::bfs()
161 : {
162 6 : int state_length = get_info()->get_lts_type().get_state_length();
163 6 : int num_rows = get_info()->get_number_of_groups();
164 : // int initial_state[state_length]; N.B. This is not portable C++
165 6 : int* initial_state = MCRL2_SPECIFIC_STACK_ALLOCATOR(int, state_length);
166 6 : this->initial_state(initial_state);
167 6 : std::vector<int> initial_state_vector = this->to_int_vector(state_length, initial_state);
168 6 : visited.insert(initial_state_vector);
169 6 : fresh.push_back(initial_state_vector);
170 : // int state[state_length]; N.B. This is not portable C++
171 6 : int* state = MCRL2_SPECIFIC_STACK_ALLOCATOR(int, state_length);
172 872 : while (!fresh.empty())
173 : {
174 866 : std::vector<int> state_vector = fresh.front();
175 866 : fresh.pop_front();
176 866 : from_int_vector(state_length, state_vector, state);
177 866 : ltsmin::test::pbes_state_cb f(this);
178 866 : this->next_state_all(state, f);
179 866 : std::vector<std::vector<int> > successors = f.get_successors();
180 :
181 866 : std::set<std::vector<int> > succ_set;
182 : //std::clog << successors.size() << " successors" << std::endl;
183 866 : transition_count += successors.size();
184 2546 : for(const std::vector<int>& s: successors)
185 : {
186 1680 : std::pair<std::set<std::vector<int> >::iterator,bool> ret;
187 1680 : ret = visited.insert(s);
188 1680 : if (ret.second)
189 : {
190 860 : fresh.push_back(s);
191 : }
192 1680 : succ_set.insert(s);
193 : }
194 : // check if the result is the same if we use groups:
195 :
196 866 : std::set<std::vector<int> > succ_set_groups;
197 5168 : for(int g=0; g < num_rows; g++)
198 : {
199 4302 : ltsmin::test::pbes_state_cb f(this);
200 4302 : this->next_state_long(state, g, f);
201 4302 : std::vector<std::vector<int> > successors_groups = f.get_successors();
202 :
203 5982 : for(const std::vector<int>& s: successors_groups)
204 : {
205 1680 : succ_set_groups.insert(s);
206 : }
207 4302 : }
208 866 : BOOST_CHECK(succ_set==succ_set_groups);
209 866 : }
210 6 : }
211 :
212 : } // namespace test
213 :
214 : } // namespace ltsmin
215 :
216 :
217 4 : void run_pbes_explorer(const std::string& pbes_text, int num_parts, int num_groups, int num_states, int num_transitions,
218 : const std::string& rewrite_strategy = "jitty")
219 : {
220 4 : std::clog << "run_pbes_explorer" << std::endl;
221 4 : pbes p = txt2pbes(pbes_text);
222 4 : normalize(p);
223 4 : if (!is_ppg(p))
224 : {
225 0 : std::clog << "Rewriting to PPG..." << std::endl;
226 0 : p = to_ppg(p);
227 0 : std::clog << "done." << std::endl;
228 : }
229 4 : ltsmin::test::explorer* pbes_explorer = new ltsmin::test::explorer(p, rewrite_strategy);
230 4 : lts_info* info = pbes_explorer->get_info();
231 4 : int state_length = info->get_lts_type().get_state_length();
232 4 : BOOST_CHECK(num_parts==state_length);
233 : //std::clog << state_length << " parts" << std::endl;
234 : //int num_rows = info->get_number_of_groups();
235 : //std::clog << num_rows << " groups" << std::endl;
236 : //BOOST_CHECK(num_groups==num_rows);
237 4 : std::map<int,std::vector<bool> > matrix = info->get_dependency_matrix();
238 4 : std::map<int,std::vector<bool> > read_matrix = info->get_read_matrix();
239 4 : std::map<int,std::vector<bool> > write_matrix = info->get_write_matrix();
240 : (void)matrix;
241 : (void)read_matrix;
242 : (void)write_matrix;
243 : // TODO: check matrices ...
244 :
245 4 : pbes_explorer->bfs();
246 : // check number of states and transitions:
247 : //BOOST_CHECK(num_states==(int)pbes_explorer->get_state_count());
248 : //BOOST_CHECK(num_transitions==(int)pbes_explorer->get_transition_count());
249 4 : delete pbes_explorer;
250 :
251 4 : }
252 :
253 2 : void run_pbes_explorer_file(const std::string& filename, int num_parts, int num_groups, int num_states, int num_transitions,
254 : const std::string& rewrite_strategy = "jitty")
255 : {
256 2 : std::clog << "run_pbes_explorer_file" << std::endl;
257 2 : ltsmin::test::explorer* pbes_explorer = new ltsmin::test::explorer(filename, rewrite_strategy);
258 2 : lts_info* info = pbes_explorer->get_info();
259 2 : int state_length = info->get_lts_type().get_state_length();
260 2 : BOOST_CHECK(num_parts==state_length);
261 : //std::clog << state_length << " parts" << std::endl;
262 : //int num_rows = info->get_number_of_groups();
263 : //std::clog << num_rows << " groups" << std::endl;
264 : //BOOST_CHECK(num_groups==num_rows);
265 2 : std::map<int,std::vector<bool> > matrix = info->get_dependency_matrix();
266 2 : std::map<int,std::vector<bool> > read_matrix = info->get_read_matrix();
267 2 : std::map<int,std::vector<bool> > write_matrix = info->get_write_matrix();
268 : (void)matrix;
269 : (void)read_matrix;
270 : (void)write_matrix;
271 : // TODO: check matrices ...
272 :
273 2 : pbes_explorer->bfs();
274 : // check number of states and transitions:
275 : //BOOST_CHECK(num_states==(int)pbes_explorer->get_state_count());
276 : //BOOST_CHECK(num_transitions==(int)pbes_explorer->get_transition_count());
277 2 : delete pbes_explorer;
278 2 : }
279 :
280 :
281 2 : BOOST_AUTO_TEST_CASE(buffer)
282 : {
283 : // buffer.nodeadlock.pbesparelm
284 : std::string pbes_text =
285 : "sort D = struct d1 | d2;\n"
286 : "map N: Pos;\n"
287 : "eqn N = 2;\n"
288 : "pbes nu X(q_Buffer: List(D)) =\n"
289 : " (val(#q_Buffer < 2) || val(!(q_Buffer == [])))\n"
290 : " && (forall d_Buffer1: D. val(!(#q_Buffer < 2)) || X(q_Buffer <| d_Buffer1))\n"
291 : " && (val(!!(q_Buffer == [])) || X(tail(q_Buffer)));\n"
292 1 : "init X([]);"
293 : ;
294 1 : int num_parts = 2; // 1 var + 1 parameter
295 1 : int num_groups = 3; // each of the conjuncts
296 1 : int num_states = 7;
297 1 : int num_transitions = 12;
298 1 : run_pbes_explorer(pbes_text, num_parts, num_groups, num_states, num_transitions, "jitty");
299 : #ifdef MCRL2_ENABLE_JITTYC
300 1 : run_pbes_explorer(pbes_text, num_parts, num_groups, num_states, num_transitions, "jittyc");
301 : #endif
302 1 : }
303 2 : BOOST_AUTO_TEST_CASE(buffer_2_read_then_eventually_send_pbesparelm_simple)
304 : {
305 : std::string pbes_text =
306 : "sort D = struct d1 | d2;\n"
307 : "map M: Pos;\n"
308 : "eqn M = 2;\n"
309 : "pbes nu Z(q_In,q_Out: List(D)) =\n"
310 : " (forall d: D. forall d_In2: D. val(!(d_In2 == d)) || val(!(#q_In < 2)) || X(q_In <| d_In2, q_Out, d)) && (forall d_In1: D. val(!(#q_In < 2)) || Z(q_In <| d_In1, q_Out)) && (val(q_Out == []) || Z(q_In, tail(q_Out))) && (val(!(!(q_In == []) && #q_Out < 2)) || Z(tail(q_In), q_Out <| head(q_In)));\n"
311 : "nu X(q_In,q_Out: List(D), d: D) =\n"
312 : " Y(q_In, q_Out, d);\n"
313 : "mu Y(q_In,q_Out: List(D), d: D) =\n"
314 : " (val(!(head(q_Out) == d)) || val(q_Out == []) || X(q_In, tail(q_Out), d)) && (forall d_In1: D. val(!(#q_In < 2)) || Y(q_In <| d_In1, q_Out, d)) && (val(head(q_Out) == d) || val(q_Out == []) || Y(q_In, tail(q_Out), d)) && (val(!(!(q_In == []) && #q_Out < 2)) || Y(tail(q_In), q_Out <| head(q_In), d));\n"
315 1 : "init Z([], []);\n"
316 : ;
317 1 : int num_parts = 4; // 1 var + 3 parameters: q_In, q_Out, d
318 1 : int num_groups = 9; // each of the conjuncts of every equation
319 1 : int num_states = 213;
320 1 : int num_transitions = 414;
321 :
322 2 : std::string pbes_filename = utilities::temporary_filename("pbes_explorer_test");
323 1 : save_pbes(txt2pbes(pbes_text), pbes_filename);
324 :
325 1 : run_pbes_explorer(pbes_text, num_parts, num_groups, num_states, num_transitions, "jitty");
326 1 : run_pbes_explorer_file(pbes_filename, num_parts, num_groups, num_states, num_transitions, "jitty");
327 : #ifdef MCRL2_ENABLE_JITTYC
328 1 : run_pbes_explorer(pbes_text, num_parts, num_groups, num_states, num_transitions, "jittyc");
329 1 : run_pbes_explorer_file(pbes_filename, num_parts, num_groups, num_states, num_transitions, "jittyc");
330 : #endif
331 : // clean up
332 1 : std::remove(pbes_filename.c_str());
333 1 : }
334 :
335 : #else // ndef MCRL2_SKIP_LONG_TESTS
336 :
337 : BOOST_AUTO_TEST_CASE(skip_test)
338 : {
339 : }
340 :
341 : #endif // ndef MCRL2_SKIP_LONG_TESTS
342 :
343 1 : boost::unit_test::test_suite* init_unit_test_suite(int argc, char* argv[])
344 : {
345 : (void) argc; (void) argv; //< avoid warning about unused parameters
346 1 : mcrl2::log::logger::set_reporting_level(mcrl2::log::debug);
347 1 : return nullptr;
348 : }
|
