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 pg_parse_test.cpp
10 : /// \brief Some io tests for boolean equation systems.
11 :
12 : #define BOOST_TEST_MODULE pg_parse_test
13 : #include "mcrl2/pbes/pg_parse.h"
14 :
15 : #include <boost/test/included/unit_test.hpp>
16 :
17 : using namespace mcrl2;
18 : using namespace mcrl2::pbes_system;
19 :
20 4 : void test_parse_pg(std::string const& in)
21 : {
22 4 : std::stringstream from(in);
23 4 : pbes bes;
24 4 : parse_pgsolver(from,bes);
25 4 : }
26 :
27 1 : void test_case()
28 : {
29 : std::string game =
30 : "0 2 0 1 \"undef\";\n"
31 : "1 2 1 2, 3 \"&\";\n"
32 : "2 2 1 4, 5 \"&\";\n"
33 : "4 2 1 5, 7, 8 \"&\";\n"
34 : "7 2 1 5, 10 \"&\";\n"
35 : "8 2 1 5, 11 \"&\";\n"
36 : "10 2 1 5, 13 \"&\";\n"
37 : "11 2 1 5, 14 \"&\";\n"
38 : "13 2 1 5, 16 \"&\";\n"
39 : "14 2 1 5, 17 \"&\";\n"
40 : "16 2 1 5, 20, 21 \"&\";\n"
41 : "17 2 1 2, 5 \"&\";\n"
42 : "20 2 1 1, 5 \"&\";\n"
43 : "21 2 1 5, 24 \"&\";\n"
44 : "24 2 1 5, 7 \"&\";\n"
45 : "3 1 0 6 \"undef\";\n"
46 : "5 1 0 31 \"undef\";\n"
47 : "6 1 1 5, 9 \"&\";\n"
48 : "9 1 0 12 \"undef\";\n"
49 : "12 1 1 5, 15 \"&\";\n"
50 : "15 1 1 18, 19 \"&\";\n"
51 : "18 1 1 5, 22 \"&\";\n"
52 : "19 1 1 5, 23 \"&\";\n"
53 : "22 1 0 25 \"undef\";\n"
54 : "23 1 0 26 \"undef\";\n"
55 : "25 1 0 5 \"undef\";\n"
56 : "26 1 1 5, 27 \"&\";\n"
57 : "27 1 0 28 \"undef\";\n"
58 : "28 1 1 5, 29 \"&\";\n"
59 : "29 1 0 30 \"undef\";\n"
60 : "30 1 1 3, 5 \"&\";\n"
61 1 : "31 0 0 31 \"undef\";\n";
62 :
63 1 : test_parse_pg(game);
64 1 : }
65 :
66 1 : void test_case_parity()
67 : {
68 : std::string game =
69 : "parity 31;\n"
70 : "0 2 0 1 \"undef\";\n"
71 : "1 2 1 2, 3 \"&\";\n"
72 : "2 2 1 4, 5 \"&\";\n"
73 : "4 2 1 5, 7, 8 \"&\";\n"
74 : "7 2 1 5, 10 \"&\";\n"
75 : "8 2 1 5, 11 \"&\";\n"
76 : "10 2 1 5, 13 \"&\";\n"
77 : "11 2 1 5, 14 \"&\";\n"
78 : "13 2 1 5, 16 \"&\";\n"
79 : "14 2 1 5, 17 \"&\";\n"
80 : "16 2 1 5, 20, 21 \"&\";\n"
81 : "17 2 1 2, 5 \"&\";\n"
82 : "20 2 1 1, 5 \"&\";\n"
83 : "21 2 1 5, 24 \"&\";\n"
84 : "24 2 1 5, 7 \"&\";\n"
85 : "3 1 0 6 \"undef\";\n"
86 : "5 1 0 31 \"undef\";\n"
87 : "6 1 1 5, 9 \"&\";\n"
88 : "9 1 0 12 \"undef\";\n"
89 : "12 1 1 5, 15 \"&\";\n"
90 : "15 1 1 18, 19 \"&\";\n"
91 : "18 1 1 5, 22 \"&\";\n"
92 : "19 1 1 5, 23 \"&\";\n"
93 : "22 1 0 25 \"undef\";\n"
94 : "23 1 0 26 \"undef\";\n"
95 : "25 1 0 5 \"undef\";\n"
96 : "26 1 1 5, 27 \"&\";\n"
97 : "27 1 0 28 \"undef\";\n"
98 : "28 1 1 5, 29 \"&\";\n"
99 : "29 1 0 30 \"undef\";\n"
100 : "30 1 1 3, 5 \"&\";\n"
101 1 : "31 0 0 31 \"undef\";\n";
102 :
103 1 : test_parse_pg(game);
104 1 : }
105 :
106 1 : void test_case_start()
107 : {
108 : std::string game =
109 : "start 0;\n"
110 : "0 2 0 1 \"undef\";\n"
111 : "1 2 1 2, 3 \"&\";\n"
112 : "2 2 1 4, 5 \"&\";\n"
113 : "4 2 1 5, 7, 8 \"&\";\n"
114 : "7 2 1 5, 10 \"&\";\n"
115 : "8 2 1 5, 11 \"&\";\n"
116 : "10 2 1 5, 13 \"&\";\n"
117 : "11 2 1 5, 14 \"&\";\n"
118 : "13 2 1 5, 16 \"&\";\n"
119 : "14 2 1 5, 17 \"&\";\n"
120 : "16 2 1 5, 20, 21 \"&\";\n"
121 : "17 2 1 2, 5 \"&\";\n"
122 : "20 2 1 1, 5 \"&\";\n"
123 : "21 2 1 5, 24 \"&\";\n"
124 : "24 2 1 5, 7 \"&\";\n"
125 : "3 1 0 6 \"undef\";\n"
126 : "5 1 0 31 \"undef\";\n"
127 : "6 1 1 5, 9 \"&\";\n"
128 : "9 1 0 12 \"undef\";\n"
129 : "12 1 1 5, 15 \"&\";\n"
130 : "15 1 1 18, 19 \"&\";\n"
131 : "18 1 1 5, 22 \"&\";\n"
132 : "19 1 1 5, 23 \"&\";\n"
133 : "22 1 0 25 \"undef\";\n"
134 : "23 1 0 26 \"undef\";\n"
135 : "25 1 0 5 \"undef\";\n"
136 : "26 1 1 5, 27 \"&\";\n"
137 : "27 1 0 28 \"undef\";\n"
138 : "28 1 1 5, 29 \"&\";\n"
139 : "29 1 0 30 \"undef\";\n"
140 : "30 1 1 3, 5 \"&\";\n"
141 1 : "31 0 0 31 \"undef\";\n";
142 :
143 1 : test_parse_pg(game);
144 1 : }
145 :
146 1 : void test_case_parity_and_start()
147 : {
148 : std::string game =
149 : "parity 31;\n"
150 : "start 0;\n"
151 : "0 2 0 1 \"undef\";\n"
152 : "1 2 1 2, 3 \"&\";\n"
153 : "2 2 1 4, 5 \"&\";\n"
154 : "4 2 1 5, 7, 8 \"&\";\n"
155 : "7 2 1 5, 10 \"&\";\n"
156 : "8 2 1 5, 11 \"&\";\n"
157 : "10 2 1 5, 13 \"&\";\n"
158 : "11 2 1 5, 14 \"&\";\n"
159 : "13 2 1 5, 16 \"&\";\n"
160 : "14 2 1 5, 17 \"&\";\n"
161 : "16 2 1 5, 20, 21 \"&\";\n"
162 : "17 2 1 2, 5 \"&\";\n"
163 : "20 2 1 1, 5 \"&\";\n"
164 : "21 2 1 5, 24 \"&\";\n"
165 : "24 2 1 5, 7 \"&\";\n"
166 : "3 1 0 6 \"undef\";\n"
167 : "5 1 0 31 \"undef\";\n"
168 : "6 1 1 5, 9 \"&\";\n"
169 : "9 1 0 12 \"undef\";\n"
170 : "12 1 1 5, 15 \"&\";\n"
171 : "15 1 1 18, 19 \"&\";\n"
172 : "18 1 1 5, 22 \"&\";\n"
173 : "19 1 1 5, 23 \"&\";\n"
174 : "22 1 0 25 \"undef\";\n"
175 : "23 1 0 26 \"undef\";\n"
176 : "25 1 0 5 \"undef\";\n"
177 : "26 1 1 5, 27 \"&\";\n"
178 : "27 1 0 28 \"undef\";\n"
179 : "28 1 1 5, 29 \"&\";\n"
180 : "29 1 0 30 \"undef\";\n"
181 : "30 1 1 3, 5 \"&\";\n"
182 1 : "31 0 0 31 \"undef\";\n";
183 :
184 1 : test_parse_pg(game);
185 1 : }
186 :
187 2 : BOOST_AUTO_TEST_CASE(test_main)
188 : {
189 1 : test_case();
190 1 : test_case_parity();
191 1 : test_case_start();
192 1 : test_case_parity_and_start();
193 1 : }
|
