tra2tba.py 7.38 KB
Newer Older
1
2
3
4
import spot

# Test 1.
aut = spot.automaton("""
5
6
7
8
9
10
11
12
13
14
15
16
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
Acceptance: 2 (Fin(0) & Inf(1))
--BODY--
State: 0
[!0] 0 {1}
[0] 1
State: 1
[0] 1 {0}
--END--
17
""")
18

19
exp = """HOA: v1
20
21
22
23
24
25
26
27
28
29
30
31
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[!0] 0 {0}
[0] 1
State: 1
[0] 1
32
--END--"""
33

34
35
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
36

37
38
# Test 2.
aut = spot.automaton("""
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
HOA: v1
States: 3
Start: 0
AP: 1 "a"
Acceptance: 2 (Inf(1) & Fin(0))
--BODY--
State: 0
[!0] 0 {0}
[0] 1
State: 1
[0] 2 {}
State: 2
[!0] 1 {}
[0] 2 {1}
--END--
EOF
55
""")
56

57
exp = """HOA: v1
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
States: 3
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc deterministic
--BODY--
State: 0
[!0] 0
[0] 1
State: 1
[0] 2
State: 2
[!0] 1
[0] 2 {0}
73
--END--"""
74

75
76
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
77

78
79
# Test 3.
aut = spot.automaton("""
80
81
82
83
84
85
86
87
88
89
90
91
HOA: v1
States: 2
Start: 0
AP: 2 "a" "b"
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
--BODY--
State: 0
[!0] 0 {0}
[0] 1
State: 1
[0] 1 {2}
--END--
92
""")
93

94
exp = """HOA: v1
95
96
97
98
99
100
101
102
103
104
105
106
States: 2
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0
[!0] 0
[0] 1
State: 1
[0] 1
107
--END--"""
108

109
110
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
111

112
113
# Test 4.
aut = spot.automaton("""
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
HOA: v1
States: 3
Start: 0
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
AP: 2 "a" "b"
--BODY--
State: 0
[0 & 1] 0 {0 2}
  [!0] 1
  [!1] 2
State: 1
  [t] 1 {1}
State: 2
  [t] 2 {3}
--END--
129
""")
130

131
exp = """HOA: v1
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
States: 3
Start: 0
AP: 2 "a" "b"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[0&1] 0
[!0] 1
[!1] 2
State: 1 {0}
[t] 1
State: 2 {0}
[t] 2
147
--END--"""
148

149
150
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
151

152
153
# Test 5.
aut = spot.automaton("""
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
HOA: v1
States: 4
Start: 0
Acceptance: 6 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3)) | (Fin(4) & Inf(5))
AP: 3 "a" "b" "c"
--BODY--
State: 0
[0 & 1 &2] 0 {0 2 4}
  [!0] 1
  [!1] 2
  [!2] 3
State: 1
  [t] 1 {1}
State: 2
  [t] 2 {3}
State: 3
  [t] 3 {5}
--END--
172
""")
173

174
exp = """HOA: v1
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
States: 4
Start: 0
AP: 3 "a" "b" "c"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc complete
--BODY--
State: 0
[0&1&2] 0
[!0] 1
[!1] 2
[!2] 3
State: 1 {0}
[t] 1
State: 2 {0}
[t] 2
State: 3 {0}
[t] 3
193
--END--"""
194

195
196
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
197

198
199
# Test 6.
aut = spot.automaton("""
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
HOA: v1
States: 2
Start: 0
Acceptance: 4 Fin(0)&Inf(1) | Fin(2)&Inf(3)
AP: 2 "p3" "p2"
--BODY--
State: 1 "F(Gp3|GFp2)"
[0&1] 1 {1 3 }
[0&!1] 0 {1 3 }
[!0&1] 1 {1 2 3 }
[!0&!1] 0 {1 2 3 }
State: 0 "F(Gp3|GFp2)"
[0&1] 1 {3 }
[0&!1] 0 {3 }
[!0&1] 1 {2 3 }
[!0&!1] 0 {2 3 }
--END--
217
""")
218

219
exp = """HOA: v1
220
221
222
223
224
225
226
227
States: 4
Start: 0
AP: 2 "p3" "p2"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
228
229
[!1] 0
[1] 1
230
231
[0&!1] 2
State: 1
232
233
[!1] 0 {0}
[1] 1 {0}
234
[0&!1] 2
235
[0&1] 3
236
237
238
State: 2
[0&!1] 2 {0}
[0&1] 3 {0}
239
State: 3
240
[0&!1] 2 {0}
241
[0&1] 3 {0}
242
--END--"""
243

244
245
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
246

247
248
# Test 7.
aut = spot.automaton("""
249
250
251
252
253
254
255
256
257
258
259
260
261
HOA: v1
name: "FG(a)"
properties: deterministic
properties: complete
States: 1
Start: 0
Acceptance: 2 Fin(0)&Inf(1)
AP: 1 "a"
--BODY--
State: 0 "FG(a)"
[0] 0 {1 }
[!0] 0 {0 1 }
--END--
262
""")
263

264
exp = """HOA: v1
265
266
267
268
269
270
271
272
States: 2
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
273
[t] 0
274
275
276
[0] 1
State: 1 {0}
[0] 1
277
--END--"""
278

279
280
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
281

282
283
# Test 8.
aut = spot.automaton("""
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
HOA: v1
States: 7
Start: 0
Acceptance: 4 Fin(0)&Inf(1) | Fin(2)&Inf(3)
AP: 3 "p0" "p2" "p3"
--BODY--
State: 1 "0"
[t] 1 {1 }
State: 5 "1"
[0&2] 5 {0 1 3 }
[0&!2] 6 {0 1 3 }
[!0&2] 3 {0 1 2 3 }
[!0&!2] 4 {0 1 2 3 }
State: 0 "2"
[!0&1&2] 3 {0 1 2 }
[(0&!1&!2|!0&1&!2)] 4 {0 1 2 }
[(0&1|!0&!1)] 1 {0 1 2 }
[0&!1&2] 2 {0 1 2 }
State: 2 "3"
[0&2] 5 {0 1 }
[0&!2] 6 {0 1 }
[!0&2] 3 {0 1 2 }
[!0&!2] 4 {0 1 2 }
State: 4 "4"
[t] 4 {0 1 2 }
State: 6 "5"
[0] 6 {0 1 3 }
[!0] 4 {0 1 2 3 }
State: 3 "6"
[0&2] 2 {0 1 2 }
[!0&2] 3 {0 1 2 }
[!2] 4 {0 1 2 }
--END--
317
""")
318

319
exp = """HOA: v1
320
321
322
323
324
325
326
327
328
329
States: 8
Start: 0
AP: 3 "p0" "p2" "p3"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!0&!1 | 0&1] 1
[0&!1&2] 2
330
331
[!0&1&2] 3
[!0&1&!2 | 0&!1&!2] 4
332
333
334
335
336
State: 1
[t] 1 {0}
State: 2
[!0&2] 3
[!0&!2] 4
337
338
[0&2] 5
[0&!2] 6
339
340
341
342
343
344
345
346
347
State: 3
[0&2] 2
[!0&2] 3
[!2] 4
State: 4
[t] 4
State: 5
[!0&2] 3
[!0&!2] 4
348
349
[0&2] 5
[0&!2] 6
350
351
352
[0&2] 7
State: 6
[!0] 4
353
[0] 6 {0}
354
355
State: 7
[0&2] 7 {0}
356
--END--"""
357

358
359
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
360

361
362
# Test 9.
aut = spot.automaton("""
363
364
365
366
367
368
369
370
371
372
373
374
375
HOA: v1
States: 2
Start: 0
AP: 3 "p0" "p4" "p1"
Acceptance: 4 (Fin(0) & Inf(1)) | (Fin(2) & Inf(3))
--BODY--
State: 0
[0&!2] 1 {0 1 3}
[!0&!2] 0 {0 1 3}
State: 1
[0&!2] 1 {0 1}
[!0&!2] 0 {0 1}
--END--
376
""")
377

378
exp = """HOA: v1
379
380
States: 2
Start: 0
381
AP: 3 "p4" "p0" "p1"
382
383
384
385
386
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic
--BODY--
State: 0 {0}
387
388
[!1&!2] 0
[1&!2] 1
389
State: 1
390
[!1&!2] 0
391
[1&!2] 1
392
--END--"""
393

394
395
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
396

397
398
# Test 10.
aut = spot.automaton("""
399
400
401
402
403
404
405
406
407
408
409
410
411
412
HOA: v1
States: 2
Start: 0
acc-name: Rabin 1
Acceptance: 2 Fin(0)&Inf(1)
AP: 2 "p0" "p2"
--BODY--
State: 0 "0"
[0&1] 0 {1 }
[!0&1] 1 {1 }
[0&!1] 0 {0 1 }
State: 1 "1"
[1] 1 {1 }
--END--
413
""")
414

415
exp = """HOA: v1
416
417
418
419
420
421
422
423
States: 3
Start: 0
AP: 2 "p0" "p2"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
424
[0] 0
425
426
427
428
429
430
[!0&1] 1
[0&1] 2
State: 1 {0}
[1] 1
State: 2 {0}
[0&1] 2
431
--END--"""
432

433
434
res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)
435

436
437
# Test 11.
aut = spot.automaton("""
438
439
440
441
442
443
444
445
446
447
448
449
450
HOA: v1
States: 2
Start: 0
Acceptance: 4 Fin(0)&Inf(1) | Fin(2)&Inf(3)
AP: 2 "p2" "p0"
--BODY--
State: 1 "1"
[1] 1 {1 2 3 }
[!1] 0 {1 3 }
State: 0 "3"
[1] 1 {2 3 }
[!1] 0 {3 }
--END--
451
""")
452

453
exp = """HOA: v1
454
455
States: 2
Start: 0
456
AP: 2 "p0" "p2"
457
458
459
460
461
462
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
463
[!0] 0 {0}
464
[0] 1
465
State: 1
466
[!0] 0 {0}
467
[0] 1 {0}
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
--END--"""

res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)

# Test 12.
aut = spot.automaton("""
HOA: v1
properties: deterministic
properties: complete
States: 2
Start: 0
Acceptance: 3 Fin(0) | Fin(1)&Inf(2)
AP: 2 "p2" "p0"
--BODY--
State: 1 "1"
[1] 1 {0 1 2}
[!1] 0 {0 2}
State: 0 "3"
[1] 1 {1 2}
[!1] 0 {2}
489
--END--
490
491
492
493
494
495
496
497
498
499
500
501
""")

exp = """HOA: v1
States: 4
Start: 0
AP: 2 "p0" "p2"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[!0] 0
502
[0] 1
503
504
505
506
[!0] 2
[!0] 3
State: 1
[!0] 0
507
[0] 1
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
[!0] 3
State: 2
[!0] 2
State: 3 {0}
[!0] 3
--END--"""

res = spot.tra_to_tba(aut)
assert(res.to_str('hoa') == exp)

# Test 13.
aut = spot.automaton("""
HOA: v1
properties: deterministic
properties: complete
States: 2
Start: 0
Acceptance: 3 Inf(0) | Fin(1)&Inf(2)
AP: 2 "p3" "p2"
--BODY--
State: 1 "F(Gp3|GFp2)"
[0&1] 1 {0 2}
[0&!1] 0 {0}
[!0&1] 1 {0 1 2}
[!0&!1] 0 {0 1 2}
State: 0 "F(Gp3|GFp2)"
[0&1] 1 {2}
[0&!1] 0 {0}
[!0&1] 1 {}
[!0&!1] 0 {2}
--END--
""")
540

541
542
543
544
545
res = spot.tra_to_tba(aut)
tba = spot.tgba_determinize(res)
a = spot.dtwa_complement(aut).intersects(tba)
b = spot.dtwa_complement(tba).intersects(aut)
assert(a == b)