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 ltsmin_test.cpp
10 : /// \brief Test for the pins class that connects mCRL2 with LTSMin (http://fmt.cs.utwente.nl/tools/ltsmin/).
11 :
12 : #define BOOST_TEST_MODULE ltsmin_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/lps/detail/test_input.h"
16 : #include "mcrl2/lps/linearise.h"
17 : #include "mcrl2/lps/ltsmin.h"
18 :
19 : using namespace mcrl2;
20 :
21 : typedef int* state_vector;
22 :
23 : inline
24 14 : std::string print_state(const state_vector& s, std::size_t size, const std::string& msg = "state: ")
25 : {
26 14 : int* first = s;
27 14 : int* last = s + size;
28 :
29 14 : std::ostringstream out;
30 14 : out << msg << "[";
31 168 : for (int* i = first; i != last; ++i)
32 : {
33 154 : if (i != first)
34 : {
35 140 : out << ", ";
36 : }
37 154 : out << *i;
38 : }
39 14 : out << "]";
40 28 : return out.str();
41 14 : }
42 :
43 : struct state_callback_function
44 : {
45 : std::size_t state_size;
46 : std::size_t state_count;
47 :
48 26 : explicit state_callback_function(std::size_t size)
49 26 : : state_size(size),
50 26 : state_count(0)
51 26 : {}
52 :
53 12 : void operator()(state_vector const& next_state, int* const& labels, int group=-1)
54 : {
55 12 : state_count++;
56 12 : std::cout << print_state(next_state, state_size, "visit state: ") << " edge label = " << labels[0] << " group = " << group << std::endl;
57 12 : }
58 : };
59 :
60 2 : void test_data_type(lps::pins_data_type& type)
61 : {
62 2 : std::cout << "test_data_type(" << type.name() << ")" << std::endl;
63 :
64 : // check serialize/deserialize
65 6 : for (std::size_t i = 0; i < type.size(); ++i)
66 : {
67 4 : std::string s = type.serialize(i);
68 4 : std::cout << "serialize(" << i << ") = " << type.serialize(i) << std::endl;
69 4 : std::size_t j = type.deserialize(s);
70 4 : BOOST_CHECK(i == j);
71 4 : }
72 :
73 : // check print/parse
74 6 : for (std::size_t i = 0; i < type.size(); ++i)
75 : {
76 4 : std::string s = type.print(i);
77 4 : std::cout << "print(" << i << ") = " << s << std::endl;
78 4 : std::size_t j = type.parse(s);
79 4 : std::cout << "parse(" << s << ") = " << j << std::endl;
80 4 : }
81 :
82 : // test iterator
83 2 : std::size_t index = 0;
84 6 : for (auto i = type.index_begin(); i != type.index_end(); ++i)
85 : {
86 4 : std::cout << "iterator " << index << " -> " << *i << std::endl;
87 4 : BOOST_CHECK(*i == index);
88 4 : index++;
89 : }
90 2 : }
91 :
92 2 : void test_ltsmin(const lps::specification& lpsspec, const std::string& filename, const std::string& rewriter_strategy)
93 : {
94 2 : lps::pins p(filename, rewriter_strategy);
95 2 : std::size_t N = p.process_parameter_count();
96 :
97 2 : BOOST_CHECK(p.process_parameter_count() == 11);
98 :
99 2 : std::size_t G = p.guard_count();
100 :
101 2 : BOOST_CHECK(G == 13);
102 2 : BOOST_CHECK(p.guard_parameters(0).size() == 1);
103 2 : BOOST_CHECK(p.guard_info(5).size() == 2);
104 : // Check below is removed as the result is unpredictable, since processes are put into a set instead of
105 : // a vector. The result below depends on the ordering in which process identifiers are stored in memory.
106 : // BOOST_CHECK(p.guard_name(0) == "s1_S == 2" || p.guard_name(0) == "s1_S == 1");
107 :
108 2 : BOOST_CHECK(p.edge_label_count() == 1);
109 4 : for (std::size_t i = 0; i < p.edge_label_count(); i++)
110 : {
111 2 : BOOST_CHECK(p.edge_label_type(i) == p.datatype_count() - 1);
112 : }
113 :
114 2 : std::set<data::sort_expression> params;
115 24 : for (const data::variable& v: lpsspec.process().process_parameters())
116 : {
117 22 : params.insert(v.sort());
118 : }
119 2 : BOOST_CHECK(p.datatype_count() == params.size() + 1);
120 2 : BOOST_CHECK(p.group_count() == 10);
121 :
122 2 : std::size_t index = 0;
123 24 : for (const data::variable& v: lpsspec.process().process_parameters())
124 : {
125 22 : const lps::pins_data_type& type = p.data_type(p.process_parameter_type(index++));
126 22 : BOOST_CHECK(type.name() == data::pp(v.sort()));
127 : }
128 :
129 : // get the initial state
130 2 : state_vector initial_state = new int[N];
131 2 : state_vector dest_state = new int[N];
132 2 : int* labels = new int[p.edge_label_count()];
133 2 : p.get_initial_state(initial_state);
134 2 : std::cout << print_state(initial_state, N, "initial state: ") << std::endl;
135 :
136 : // find all successors of the initial state
137 2 : state_callback_function f_all(p.process_parameter_count());
138 2 : p.next_state_all(initial_state, f_all, dest_state, labels);
139 2 : std::cout << "f_all.state_count = " << f_all.state_count << std::endl;
140 :
141 : // find successors of the initial state for individual groups
142 2 : std::size_t count = 0;
143 22 : for (std::size_t group = 0; group < p.group_count(); group++)
144 : {
145 20 : state_callback_function f_long(p.process_parameter_count());
146 20 : p.next_state_long(initial_state, group, f_long, dest_state, labels);
147 20 : std::cout << "group " << group << " count = " << f_long.state_count << std::endl;
148 20 : count += f_long.state_count;
149 : }
150 2 : BOOST_CHECK(count == f_all.state_count);
151 :
152 : // find successors (without evaluating condition) of the initial state for individual groups
153 2 : count = 0;
154 22 : for (std::size_t group = 0; group < p.group_count(); group++)
155 : {
156 :
157 20 : std::size_t all_true = p.GUARD_TRUE;
158 40 : for(std::size_t guard = 0; guard < p.guard_info(group).size() && all_true == p.GUARD_TRUE; guard++) {
159 20 : all_true = p.eval_guard_long(initial_state, p.guard_info(group)[guard]);
160 : }
161 :
162 20 : if (all_true == p.GUARD_TRUE) {
163 4 : state_callback_function f_long(p.process_parameter_count());
164 4 : p.update_long(initial_state, group, f_long, dest_state, labels);
165 4 : std::cout << "group " << group << " count = " << f_long.state_count << std::endl;
166 4 : count += f_long.state_count;
167 : }
168 : }
169 2 : BOOST_CHECK(count == f_all.state_count);
170 :
171 2 : lps::pins_data_type& action_label_type = p.data_type(p.datatype_count() - 1);
172 2 : test_data_type(action_label_type);
173 :
174 2 : delete[] initial_state;
175 2 : delete[] dest_state;
176 2 : delete[] labels;
177 :
178 2 : std::cout << p.info() << std::endl;
179 :
180 : // test summand_action_names()
181 2 : std::cout << "--- summand action names ---" << std::endl;
182 22 : for (std::size_t i = 0; i < p.group_count(); i++)
183 : {
184 20 : std::cout << i << " {";
185 20 : std::set<std::string> s = p.summand_action_names(i);
186 40 : for (auto j = s.begin(); j != s.end(); ++j)
187 : {
188 20 : if (j != s.begin())
189 : {
190 0 : std::cout << ", ";
191 : }
192 20 : std::cout << *j;
193 : }
194 20 : std::cout << "}" << std::endl;
195 20 : }
196 2 : }
197 :
198 1 : void test_ltsmin()
199 : {
200 2 : lps::specification abp_spec = remove_stochastic_operators(lps::linearise(lps::detail::ABP_SPECIFICATION()));
201 1 : std::string abp_filename = "temporary_abp.lps";
202 1 : save_lps(abp_spec, abp_filename);
203 1 : test_ltsmin(abp_spec, abp_filename, "jitty");
204 : #ifdef MCRL2_ENABLE_JITTYC
205 1 : test_ltsmin(abp_spec, abp_filename, "jittyc");
206 : #endif // MCRL2_ENABLE_JITTYC
207 1 : std::remove(abp_filename.c_str());
208 1 : }
209 :
210 : template <typename Iter>
211 6 : std::string print_vector(Iter first, Iter last)
212 : {
213 6 : std::ostringstream out;
214 6 : out << "[";
215 8 : for (Iter i = first; i != last; ++i)
216 : {
217 2 : if (i != first)
218 : {
219 0 : out << ", ";
220 : }
221 2 : out << *i;
222 : }
223 6 : out << "]";
224 12 : return out.str();
225 6 : }
226 :
227 : template <typename Container>
228 6 : std::string print_vector(const Container& c)
229 : {
230 6 : return print_vector(c.begin(), c.end());
231 : }
232 :
233 : inline
234 : std::string read_groups(const lps::pins& p)
235 : {
236 : std::ostringstream out;
237 : for (std::size_t i = 0; i < p.group_count(); i++)
238 : {
239 : out << print_vector(p.read_group(i)) << std::endl;
240 : }
241 : return out.str();
242 : }
243 :
244 : inline
245 : std::string write_groups(const lps::pins& p)
246 : {
247 : std::ostringstream out;
248 : for (std::size_t i = 0; i < p.group_count(); i++)
249 : {
250 : out << print_vector(p.write_group(i)) << std::endl;
251 : }
252 : return out.str();
253 : }
254 :
255 : inline
256 : std::string update_groups(const lps::pins& p)
257 : {
258 : std::ostringstream out;
259 : for (std::size_t i = 0; i < p.group_count(); i++)
260 : {
261 : out << print_vector(p.update_group(i)) << std::endl;
262 : }
263 : return out.str();
264 : }
265 :
266 : inline
267 1 : void test_dependency_matrix()
268 : {
269 : std::string ONEBIT =
270 : "proc P(b: Bool) = \n"
271 : " tau . P(b = false); \n"
272 : " \n"
273 1 : "init P(true); \n"
274 : ;
275 :
276 1 : lps::specification spec = lps::parse_linear_process_specification(ONEBIT);
277 1 : std::string filename = "temporary_onebit.lps";
278 1 : save_lps(spec, filename);
279 2 : lps::pins p(filename, "jitty");
280 :
281 2 : for (std::size_t i = 0; i < p.group_count(); i++)
282 : {
283 1 : std::cout << "\n";
284 1 : std::cout << " read_group(" << i << ") = " << print_vector(p.read_group(i)) << std::endl;
285 1 : std::cout << " write_group(" << i << ") = " << print_vector(p.write_group(i)) << std::endl;
286 1 : std::cout << "update_group(" << i << ") = " << print_vector(p.update_group(i)) << std::endl;
287 : }
288 1 : BOOST_CHECK(print_vector(p.read_group(0)) == "[]");
289 1 : BOOST_CHECK(print_vector(p.write_group(0)) == "[0]");
290 1 : BOOST_CHECK(print_vector(p.update_group(0)) == "[]");
291 :
292 : // cleanup temporary files
293 1 : std::remove(filename.c_str());
294 1 : }
295 :
296 : inline
297 1 : void test_serialisation()
298 : {
299 : std::string EXAMPLE =
300 : "sort Piece = struct Red | Yellow | None; \n"
301 : " \n"
302 : "proc P(i: Pos, j: Nat, p: Piece) = \n"
303 : " tau . P(i = 1, j = 0, p = Red); \n"
304 : " \n"
305 1 : "init P(1, 1, None); \n"
306 : ;
307 :
308 1 : lps::specification spec = lps::parse_linear_process_specification(EXAMPLE);
309 1 : std::string filename = "temporary_onebit.lps";
310 1 : save_lps(spec, filename);
311 2 : lps::pins p1(filename, "jitty");
312 2 : lps::pins p2(filename, "jitty");
313 1 : std::cout << "datatypes: " << p1.datatype_count() << std::endl;
314 5 : for(std::size_t i=0; i < p1.datatype_count(); i++)
315 : {
316 4 : std::cout << i << ": " << p1.data_type(i).name() << std::endl;
317 : }
318 1 : std::vector<std::pair<std::string, std::size_t>> expressions;
319 1 : expressions.push_back(std::make_pair("1", 0));
320 1 : expressions.push_back(std::make_pair("0", 1));
321 1 : expressions.push_back(std::make_pair("1", 1));
322 1 : expressions.push_back(std::make_pair("Red", 2));
323 1 : expressions.push_back(std::make_pair("Yellow", 2));
324 :
325 6 : for(auto e : expressions)
326 : {
327 5 : std::string s = e.first;
328 5 : std::cerr << "STRING " << s << "\n";
329 5 : std::size_t type = e.second;
330 5 : std::cerr << "TYPE " << type << "\n";
331 :
332 5 : data::data_expression d1 = data::parse_data_expression(s, spec.data());
333 5 : std::cerr << "DATA EXPRESSION " << d1 << "\n";
334 5 : std::string serialised = p1.data_type(type).serialize(p1.data_type(type)[d1]);
335 5 : data::data_expression d2(p2.data_type(type).get(p2.data_type(type).deserialize(serialised)));
336 5 : std::cout << "string: " << s << std::endl;
337 5 : std::cout << "expression: " << d1 << std::endl;
338 5 : std::cout << "serialised: " << serialised << std::endl;
339 5 : std::cout << "result: " << d2 << std::endl;
340 5 : BOOST_CHECK(d1==d2);
341 5 : }
342 :
343 : // cleanup temporary files
344 1 : std::remove(filename.c_str());
345 1 : }
346 :
347 2 : BOOST_AUTO_TEST_CASE(test_main)
348 : {
349 1 : test_dependency_matrix();
350 1 : test_serialisation();
351 1 : test_ltsmin();
352 1 : }
|
