1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2014-2018 Laboratoire de Recherche et Développement de
3 // 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/ngraph.hh>
23 #include <spot/twa/twa.hh>
24
25 template <typename SL, typename TL>
26 void
dot_state(std::ostream & out,const spot::digraph<SL,TL> & g,unsigned n)27 dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n)
28 {
29 out << " [label=\"" << g.state_data(n) << "\"]\n";
30 }
31
32 template <typename TL>
33 void
dot_state(std::ostream & out,const spot::digraph<void,TL> &,unsigned)34 dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned)
35 {
36 out << '\n';
37 }
38
39 template <typename SL, typename TL>
40 void
dot_state(std::ostream & out,const spot::digraph<SL,TL> & g,unsigned n,std::string name)41 dot_state(std::ostream& out, const spot::digraph<SL, TL>& g, unsigned n,
42 std::string name)
43 {
44 out << " [label=\"" << name << "\\n" << g.state_data(n) << "\"]\n";
45 }
46
47 template <typename TL>
48 void
dot_state(std::ostream & out,const spot::digraph<void,TL> &,unsigned,std::string name)49 dot_state(std::ostream& out, const spot::digraph<void, TL>&, unsigned,
50 std::string name)
51 {
52 out << " [label=\"" << name << "\"]\n";
53 }
54
55
56 template <typename SL, typename TL, typename TR>
57 void
dot_trans(std::ostream & out,const spot::digraph<SL,TL> &,TR & tr)58 dot_trans(std::ostream& out, const spot::digraph<SL, TL>&, TR& tr)
59 {
60 out << " [label=\"" << tr.data() << "\"]\n";
61 }
62
63 template <typename SL, typename TR>
64 void
dot_trans(std::ostream & out,const spot::digraph<SL,void> &,TR &)65 dot_trans(std::ostream& out, const spot::digraph<SL, void>&, TR&)
66 {
67 out << '\n';
68 }
69
70
71 template <typename SL, typename TL>
72 void
dot(std::ostream & out,const spot::digraph<SL,TL> & g)73 dot(std::ostream& out, const spot::digraph<SL, TL>& g)
74 {
75 out << "digraph {\n";
76 unsigned c = g.num_states();
77 for (unsigned s = 0; s < c; ++s)
78 {
79 out << ' ' << s;
80 dot_state(out, g, s);
81 for (auto& t: g.out(s))
82 {
83 out << ' ' << s << " -> " << t.dst;
84 dot_trans(out, g, t);
85 }
86 }
87 out << "}\n";
88 }
89
90 template <typename G1, typename G2, typename G3, typename G4>
91 void
dot(std::ostream & out,const spot::named_graph<G1,G2,G3,G4> & g)92 dot(std::ostream& out, const spot::named_graph<G1, G2, G3, G4>& g)
93 {
94 out << "digraph {\n";
95 auto& gg = g.graph();
96 unsigned c = gg.num_states();
97 for (unsigned s = 0; s < c; ++s)
98 {
99 out << ' ' << s;
100 dot_state(out, gg, s, g.get_name(s));
101 for (auto& t: gg.out(s))
102 {
103 out << ' ' << s << " -> " << t.dst;
104 dot_trans(out, gg, t);
105 }
106 }
107 out << "}\n";
108 }
109
110
111 static bool
g1(const spot::digraph<void,void> & g,unsigned s,int e)112 g1(const spot::digraph<void, void>& g, unsigned s, int e)
113 {
114 int f = 0;
115 for (auto& t: g.out(s))
116 {
117 (void) t;
118 ++f;
119 }
120 return f == e;
121 }
122
f1()123 static bool f1()
124 {
125 spot::digraph<void, void> g(3);
126 spot::named_graph<spot::digraph<void, void>, std::string> gg(g);
127
128 auto s1 = gg.new_state("s1");
129 auto s2 = gg.new_state("s2");
130 auto s3 = gg.new_state("s3");
131 gg.new_edge("s1", "s2");
132 gg.new_edge("s1", "s3");
133 gg.new_edge("s2", "s3");
134 gg.new_edge("s3", "s1");
135 gg.new_edge("s3", "s2");
136 gg.new_edge("s3", "s3");
137
138 dot(std::cout, gg);
139
140 int f = 0;
141 for (auto& t: g.out(s1))
142 {
143 (void) t;
144 ++f;
145 }
146 return f == 2
147 && g1(g, s3, 3)
148 && g1(g, s2, 1)
149 && g1(g, s1, 2);
150 }
151
152
f2()153 static bool f2()
154 {
155 spot::digraph<int, void> g(3);
156 spot::named_graph<spot::digraph<int, void>, std::string> gg(g);
157
158 auto s1 = gg.new_state("s1", 1);
159 gg.new_state("s2", 2);
160 gg.new_state("s3", 3);
161 gg.new_edge("s1", "s2");
162 gg.new_edge("s1", "s3");
163 gg.new_edge("s2", "s3");
164 gg.new_edge("s3", "s2");
165
166 dot(std::cout, gg);
167
168 int f = 0;
169 for (auto& t: g.out(s1))
170 {
171 f += g.state_data(t.dst);
172 }
173 return f == 5;
174 }
175
f3()176 static bool f3()
177 {
178 spot::digraph<void, int> g(3);
179 spot::named_graph<spot::digraph<void, int>, std::string> gg(g);
180
181 auto s1 = gg.new_state("s1");
182 gg.new_state("s2");
183 gg.new_state("s3");
184 gg.new_edge("s1", "s2", 1);
185 gg.new_edge("s1", "s3", 2);
186 gg.new_edge("s2", "s3", 3);
187 gg.new_edge("s3", "s2", 4);
188
189 dot(std::cout, gg);
190
191 int f = 0;
192 for (auto& t: g.out(s1))
193 {
194 f += t.label;
195 }
196 return f == 3 && g.states().size() == 3;
197 }
198
f4()199 static bool f4()
200 {
201 spot::digraph<int, int> g(3);
202 spot::named_graph<spot::digraph<int, int>, std::string> gg(g);
203
204 auto s1 = gg.new_state("s1", 2);
205 gg.new_state("s2", 3);
206 gg.new_state("s3", 4);
207 gg.new_edge("s1", "s2", 1);
208 gg.new_edge("s1", "s3", 2);
209 gg.new_edge("s2", "s3", 3);
210 gg.new_edge("s3", "s2", 4);
211
212 dot(std::cout, gg);
213
214 int f = 0;
215 for (auto& t: g.out(s1))
216 {
217 f += t.label * g.state_data(t.dst);
218 }
219 return f == 11;
220 }
221
f5()222 static bool f5()
223 {
224 typedef spot::digraph<void, std::pair<int, float>> graph_t;
225 graph_t g(3);
226 spot::named_graph<graph_t, std::string> gg(g);
227
228 auto s1 = gg.new_state("s1");
229 gg.new_state("s2");
230 gg.new_state("s3");
231 gg.new_edge("s1", "s2", std::make_pair(1, 1.2f));
232 gg.new_edge("s1", "s3", std::make_pair(2, 1.3f));
233 gg.new_edge("s2", "s3", std::make_pair(3, 1.4f));
234 gg.new_edge("s3", "s2", std::make_pair(4, 1.5f));
235
236 int f = 0;
237 float h = 0;
238 for (auto& t: g.out(s1))
239 {
240 f += std::get<0>(t);
241 h += std::get<1>(t);
242 }
243 return f == 3 && (h > 2.49 && h < 2.51);
244 }
245
f6()246 static bool f6()
247 {
248 typedef spot::digraph<void, std::pair<int, float>> graph_t;
249 graph_t g(3);
250 spot::named_graph<graph_t, std::string> gg(g);
251
252 auto s1 = gg.new_state("s1");
253 gg.new_state("s2");
254 gg.new_state("s3");
255 gg.new_edge("s1", "s2", 1, 1.2f);
256 gg.new_edge("s1", "s3", 2, 1.3f);
257 gg.new_edge("s2", "s3", 3, 1.4f);
258 gg.new_edge("s3", "s2", 4, 1.5f);
259
260 int f = 0;
261 float h = 0;
262 for (auto& t: g.out(s1))
263 {
264 f += t.first;
265 h += t.second;
266 }
267 return f == 3 && (h > 2.49 && h < 2.51) && g.is_existential();
268 }
269
f7()270 static bool f7()
271 {
272 typedef spot::digraph<int, int> graph_t;
273 graph_t g(3);
274 spot::named_graph<graph_t, std::string> gg(g);
275
276 auto s1 = gg.new_state("s1", 2);
277 gg.new_state("s2", 3);
278 gg.new_state("s3", 4);
279 gg.new_univ_edge("s1", {"s2", "s3"}, 1);
280 // Standard edges can be used as well
281 gg.new_edge("s1", "s3", 2);
282 gg.new_univ_edge("s2", {"s3"}, 3);
283 gg.new_univ_edge("s3", {"s2"}, 4);
284
285 int f = 0;
286 for (auto& t: g.out(s1))
287 for (unsigned tt: g.univ_dests(t.dst))
288 f += t.label * g.state_data(tt);
289
290 return f == 15 && !g.is_existential();
291 }
292
293
294 struct int_pair
295 {
296 int one;
297 int two;
298
operator <<(std::ostream & os,int_pair p)299 friend std::ostream& operator<<(std::ostream& os, int_pair p)
300 {
301 os << '(' << p.one << ',' << p.two << ')';
302 return os;
303 }
304
305 #if __GNUC__ <= 4 && __GNUC_MINOR__ <= 6
int_pairint_pair306 int_pair(int one, int two)
307 : one(one), two(two)
308 {
309 }
310
int_pairint_pair311 int_pair()
312 {
313 }
314 #endif
315 };
316
f8()317 static bool f8()
318 {
319 typedef spot::digraph<int_pair, int_pair> graph_t;
320 graph_t g(3);
321 spot::named_graph<graph_t, std::string> gg(g);
322 auto s1 = gg.new_state("s1", 2, 4);
323 gg.new_state("s2", 3, 6);
324 gg.new_state("s3", 4, 8);
325 gg.new_edge("s1", "s2", 1, 3);
326 gg.new_edge("s1", "s3", 2, 5);
327 gg.new_edge("s2", "s3", 3, 7);
328 gg.new_edge("s3", "s2", 4, 9);
329
330 dot(std::cout, gg);
331
332 int f = 0;
333 for (auto& t: g.out(s1))
334 {
335 f += t.one * g.state_data(t.dst).one;
336 f += t.two * g.state_data(t.dst).two;
337 }
338 return f == 69;
339 }
340
341 struct my_state: public spot::state
342 {
343 public:
~my_statemy_state344 virtual ~my_state() noexcept
345 {
346 }
347
my_statemy_state348 my_state() noexcept
349 {
350 }
351
my_statemy_state352 my_state(const my_state&) noexcept
353 {
354 }
355
operator =my_state356 my_state& operator=(const my_state&) noexcept
357 {
358 return *this;
359 }
360
comparemy_state361 int compare(const spot::state* other) const override
362 {
363 auto o = spot::down_cast<const my_state*>(other);
364
365 // Do not simply return "other - this", it might not fit in an int.
366 if (o < this)
367 return -1;
368 if (o > this)
369 return 1;
370 return 0;
371 }
372
hashmy_state373 size_t hash() const override
374 {
375 return reinterpret_cast<size_t>(this);
376 }
377
clonemy_state378 my_state* clone() const override
379 {
380 return const_cast<my_state*>(this);
381 }
382
destroymy_state383 void destroy() const override
384 {
385 }
386
operator <<(std::ostream & os,const my_state &)387 friend std::ostream& operator<<(std::ostream& os, const my_state&)
388 {
389 return os;
390 }
391 };
392
f9()393 static bool f9()
394 {
395 typedef spot::digraph<my_state, int_pair> graph_t;
396 graph_t g(3);
397 spot::named_graph<graph_t, std::string> gg(g);
398 auto s1 = gg.new_state("s1");
399 gg.new_state("s2");
400 auto s3 = gg.new_state("s3");
401 gg.alias_state(s3, "s3b");
402
403 gg.new_edge("s1", "s2", 1, 3);
404 gg.new_edge("s1", "s3", 2, 5);
405 gg.new_edge("s2", "s3b", 3, 7);
406 gg.new_edge("s3", "s2", 4, 9);
407
408 dot(std::cout, gg);
409
410 int f = 0;
411 for (auto& t: g.out(s1))
412 {
413 f += t.one + t.two;
414 }
415
416
417 return (f == 11) &&
418 g.state_data(s1).compare(&g.state_data(gg.get_state("s1"))) == 0 &&
419 g.state_data(s1).compare(&g.state_data(gg.get_state("s2"))) != 0;
420 }
421
main()422 int main()
423 {
424 bool a1 = f1();
425 bool a2 = f2();
426 bool a3 = f3();
427 bool a4 = f4();
428 bool a5 = f5();
429 bool a6 = f6();
430 bool a7 = f7();
431 bool a8 = f8();
432 bool a9 = f9();
433 std::cout << a1 << ' '
434 << a2 << ' '
435 << a3 << ' '
436 << a4 << ' '
437 << a5 << ' '
438 << a6 << ' '
439 << a7 << ' '
440 << a8 << ' '
441 << a9 << '\n';
442 return !(a1 && a2 && a3 && a4 && a5 && a6 && a7 && a8 && a9);
443 }
444