1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2018 Laboratoire de Recherche et
3 // Développement de l'Epita.
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20 #include "config.h"
21 #include <iostream>
22 #include <spot/graph/graph.hh>
23
24 template <typename SL, typename TL>
25 void
dot_state(std::ostream & out,spot::digraph<SL,TL> & g,unsigned n)26 dot_state(std::ostream& out, spot::digraph<SL, TL>& g, unsigned n)
27 {
28 out << " [label=\"" << g.state_data(n) << "\"]\n";
29 }
30
31 template <typename TL>
32 void
dot_state(std::ostream & out,spot::digraph<void,TL> &,unsigned)33 dot_state(std::ostream& out, spot::digraph<void, TL>&, unsigned)
34 {
35 out << '\n';
36 }
37
38 template <typename SL, typename TL, typename TR>
39 void
dot_trans(std::ostream & out,spot::digraph<SL,TL> &,TR & tr)40 dot_trans(std::ostream& out, spot::digraph<SL, TL>&, TR& tr)
41 {
42 out << " [label=\"" << tr.data() << "\"]\n";
43 }
44
45 template <typename SL, typename TR>
46 void
dot_trans(std::ostream & out,spot::digraph<SL,void> &,TR &)47 dot_trans(std::ostream& out, spot::digraph<SL, void>&, TR&)
48 {
49 out << '\n';
50 }
51
52
53 template <typename SL, typename TL>
54 void
dot(std::ostream & out,spot::digraph<SL,TL> & g)55 dot(std::ostream& out, spot::digraph<SL, TL>& g)
56 {
57 out << "digraph {\n";
58 unsigned c = g.num_states();
59 for (unsigned s = 0; s < c; ++s)
60 {
61 out << ' ' << s;
62 dot_state(out, g, s);
63 for (auto& t: g.out(s))
64 {
65 out << ' ' << s << " -> " << t.dst;
66 dot_trans(out, g, t);
67 }
68 }
69 out << "}\n";
70 }
71
72
73 static bool
g1(const spot::digraph<void,void> & g,unsigned s,int e)74 g1(const spot::digraph<void, void>& g,
75 unsigned s, int e)
76 {
77 int f = 0;
78 for (auto& t: g.out(s))
79 {
80 (void) t;
81 ++f;
82 }
83 return f == e;
84 }
85
86 static bool
f1()87 f1()
88 {
89 spot::digraph<void, void> g(3);
90
91 auto s1 = g.new_state();
92 auto s2 = g.new_state();
93 auto s3 = g.new_state();
94 g.new_edge(s1, s2);
95 g.new_edge(s1, s3);
96 g.new_edge(s2, s3);
97 g.new_edge(s3, s1);
98 g.new_edge(s3, s2);
99 g.new_edge(s3, s3);
100
101 dot(std::cout, g);
102
103 int f = 0;
104 for (auto& t: g.out(s1))
105 {
106 (void) t;
107 ++f;
108 }
109 return f == 2
110 && g1(g, s3, 3)
111 && g1(g, s2, 1)
112 && g1(g, s1, 2);
113 }
114
115
116 static bool
f2()117 f2()
118 {
119 spot::digraph<int, void> g(3);
120
121 auto s1 = g.new_state(1);
122 auto s2 = g.new_state(2);
123 auto s3 = g.new_state(3);
124 g.new_edge(s1, s2);
125 g.new_edge(s1, s3);
126 g.new_edge(s2, s3);
127 g.new_edge(s3, s2);
128
129 dot(std::cout, g);
130
131 int f = 0;
132 for (auto& t: g.out(s1))
133 {
134 f += g.state_data(t.dst);
135 }
136 return f == 5;
137 }
138
139 static bool
f3()140 f3()
141 {
142 spot::digraph<void, int> g(3);
143
144 auto s1 = g.new_state();
145 auto s2 = g.new_state();
146 auto s3 = g.new_state();
147 g.new_edge(s1, s2, 1);
148 g.new_edge(s1, s3, 2);
149 g.new_edge(s2, s3, 3);
150 g.new_edge(s3, s2, 4);
151
152 dot(std::cout, g);
153
154 int f = 0;
155 for (auto& t: g.out(s1))
156 {
157 f += t.label;
158 }
159 return f == 3 && g.states().size() == 3;
160 }
161
162 static bool
f4()163 f4()
164 {
165 spot::digraph<int, int> g(3);
166
167 auto s1 = g.new_state(2);
168 auto s2 = g.new_state(3);
169 auto s3 = g.new_state(4);
170 g.new_edge(s1, s2, 1);
171 g.new_edge(s1, s3, 2);
172 g.new_edge(s2, s3, 3);
173 g.new_edge(s3, s2, 4);
174
175 dot(std::cout, g);
176
177 int f = 0;
178 for (auto& t: g.out(s1))
179 {
180 f += t.label * g.state_data(t.dst);
181 }
182 return f == 11;
183 }
184
185 static bool
f5()186 f5()
187 {
188 spot::digraph<void, std::pair<int, float>> g(3);
189
190 auto s1 = g.new_state();
191 auto s2 = g.new_state();
192 auto s3 = g.new_state();
193 g.new_edge(s1, s2, std::make_pair(1, 1.2f));
194 g.new_edge(s1, s3, std::make_pair(2, 1.3f));
195 g.new_edge(s2, s3, std::make_pair(3, 1.4f));
196 g.new_edge(s3, s2, std::make_pair(4, 1.5f));
197
198 int f = 0;
199 float h = 0;
200 for (auto& t: g.out(s1))
201 {
202 f += std::get<0>(t);
203 h += std::get<1>(t);
204 }
205 return f == 3 && (h > 2.49 && h < 2.51);
206 }
207
208 static bool
f6()209 f6()
210 {
211 spot::digraph<void, std::pair<int, float>> g(3);
212
213 auto s1 = g.new_state();
214 auto s2 = g.new_state();
215 auto s3 = g.new_state();
216 g.new_edge(s1, s2, 1, 1.2f);
217 g.new_edge(s1, s3, 2, 1.3f);
218 g.new_edge(s2, s3, 3, 1.4f);
219 g.new_edge(s3, s2, 4, 1.5f);
220
221 int f = 0;
222 float h = 0;
223 for (auto& t: g.out(s1))
224 {
225 f += t.first;
226 h += t.second;
227 }
228 return f == 3 && (h > 2.49 && h < 2.51) && g.is_existential();
229 }
230
231 static bool
f7()232 f7()
233 {
234 spot::digraph<int, int> g(3);
235 auto s1 = g.new_state(2);
236 auto s2 = g.new_state(3);
237 auto s3 = g.new_state(4);
238 g.new_univ_edge(s1, {s2, s3}, 1);
239 g.new_univ_edge(s1, {s3}, 2);
240 g.new_univ_edge(s2, {s3}, 3);
241 g.new_univ_edge(s3, {s2}, 4);
242
243 int f = 0;
244 for (auto& t: g.out(s1))
245 for (unsigned tt: g.univ_dests(t))
246 f += t.label * g.state_data(tt);
247
248 g.dump_storage(std::cout);
249
250 return f == 15 && !g.is_existential();
251 }
252
253
254 struct int_pair
255 {
256 int one;
257 int two;
258
operator <<(std::ostream & os,int_pair p)259 friend std::ostream& operator<<(std::ostream& os, int_pair p)
260 {
261 os << '(' << p.one << ',' << p.two << ')';
262 return os;
263 }
264
265 #if __GNUC__ <= 4 && __GNUC_MINOR__ <= 6
int_pairint_pair266 int_pair(int one, int two)
267 : one(one), two(two)
268 {
269 }
270
int_pairint_pair271 int_pair()
272 {
273 }
274 #endif
275 };
276
277 static bool
f8()278 f8()
279 {
280 spot::digraph<int_pair, int_pair> g(3);
281 auto s1 = g.new_state(2, 4);
282 auto s2 = g.new_state(3, 6);
283 auto s3 = g.new_state(4, 8);
284 g.new_edge(s1, s2, 1, 3);
285 g.new_edge(s1, s3, 2, 5);
286 g.new_edge(s2, s3, 3, 7);
287 g.new_edge(s3, s2, 4, 9);
288
289 dot(std::cout, g);
290
291 int f = 0;
292 for (auto& t: g.out(s1))
293 {
294 f += t.one * g.state_data(t.dst).one;
295 f += t.two * g.state_data(t.dst).two;
296 }
297 return f == 69;
298 }
299
300
main()301 int main()
302 {
303 bool a1 = f1();
304 bool a2 = f2();
305 bool a3 = f3();
306 bool a4 = f4();
307 bool a5 = f5();
308 bool a6 = f6();
309 bool a7 = f7();
310 bool a8 = f8();
311 std::cout << a1 << ' '
312 << a2 << ' '
313 << a3 << ' '
314 << a4 << ' '
315 << a5 << ' '
316 << a6 << ' '
317 << a7 << ' '
318 << a8 << '\n';
319 return !(a1 && a2 && a3 && a4 && a5 && a6 && a7 && a8);
320 }
321