tra2tba.py 8.03 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
res = spot.remove_fin(aut)
35
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
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--
54
""")
55

56
exp = """HOA: v1
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
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}
72
--END--"""
73

74
res = spot.remove_fin(aut)
75
assert(res.to_str('hoa') == exp)
76

77
78
# Test 3.
aut = spot.automaton("""
79
80
81
82
83
84
85
86
87
88
89
90
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--
91
""")
92

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

108
res = spot.remove_fin(aut)
109
assert(res.to_str('hoa') == exp)
110

111
112
# Test 4.
aut = spot.automaton("""
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
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--
128
""")
129

130
exp = """HOA: v1
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
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
146
--END--"""
147

148
res = spot.remove_fin(aut)
149
assert(res.to_str('hoa') == exp)
150

151
152
# Test 5.
aut = spot.automaton("""
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
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--
171
""")
172

173
exp = """HOA: v1
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
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
192
--END--"""
193

194
res = spot.remove_fin(aut)
195
assert(res.to_str('hoa') == exp)
196

197
198
# Test 6.
aut = spot.automaton("""
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
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--
216
""")
217

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

243
res = spot.remove_fin(aut)
244
assert(res.to_str('hoa') == exp)
245

246
247
# Test 7.
aut = spot.automaton("""
248
249
250
251
252
253
254
255
256
257
258
259
260
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--
261
""")
262

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

278
res = spot.remove_fin(aut)
279
assert(res.to_str('hoa') == exp)
280

281
282
# Test 8.
aut = spot.automaton("""
283
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
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--
316
""")
317

318
exp = """HOA: v1
319
320
321
322
323
324
325
326
327
328
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
329
330
[!0&1&2] 3
[!0&1&!2 | 0&!1&!2] 4
331
332
333
334
335
State: 1
[t] 1 {0}
State: 2
[!0&2] 3
[!0&!2] 4
336
337
[0&2] 5
[0&!2] 6
338
339
340
341
342
343
344
345
346
State: 3
[0&2] 2
[!0&2] 3
[!2] 4
State: 4
[t] 4
State: 5
[!0&2] 3
[!0&!2] 4
347
348
[0&2] 5
[0&!2] 6
349
350
351
[0&2] 7
State: 6
[!0] 4
352
[0] 6 {0}
353
354
State: 7
[0&2] 7 {0}
355
--END--"""
356

357
res = spot.remove_fin(aut)
358
assert(res.to_str('hoa') == exp)
359

360
361
# Test 9.
aut = spot.automaton("""
362
363
364
365
366
367
368
369
370
371
372
373
374
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--
375
""")
376

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

393
res = spot.remove_fin(aut)
394
assert(res.to_str('hoa') == exp)
395

396
397
# Test 10.
aut = spot.automaton("""
398
399
400
401
402
403
404
405
406
407
408
409
410
411
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--
412
""")
413

414
exp = """HOA: v1
415
416
417
418
419
420
421
422
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
423
[0] 0
424
425
426
427
428
429
[!0&1] 1
[0&1] 2
State: 1 {0}
[1] 1
State: 2 {0}
[0&1] 2
430
--END--"""
431

432
res = spot.remove_fin(aut)
433
assert(res.to_str('hoa') == exp)
434

435
436
# Test 11.
aut = spot.automaton("""
437
438
439
440
441
442
443
444
445
446
447
448
449
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--
450
""")
451

452
exp = """HOA: v1
453
454
States: 2
Start: 0
455
AP: 2 "p0" "p2"
456
457
458
459
460
461
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
462
[!0] 0 {0}
463
[0] 1
464
State: 1
465
[!0] 0 {0}
466
[0] 1 {0}
467
468
--END--"""

469
470

res = spot.remove_fin(aut)
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
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
[!0] 3
509
State: 2 {0}
510
511
512
513
514
[!0] 2
State: 3 {0}
[!0] 3
--END--"""

515
res = spot.remove_fin(aut)
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
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
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
exp = """HOA: v1
States: 2
Start: 0
AP: 2 "p3" "p2"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[!1] 0 {0}
[1] 1
State: 1
[!1] 0 {0}
[1] 1 {0}
--END--"""

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

# Test 14.
aut = spot.automaton("""
HOA: v1
States: 1
Start: 0
Acceptance: 4 (Fin(0)&Inf(1)) | (Fin(2)&Inf(3))
AP: 2 "b" "a"
--BODY--
State: 0
 0 {3}          /*{}*/
 0 {1 3}        /*{b}*/
 0 {2}          /*{a}*/
 0 {2 1}        /*{b, a}*/
--END--""")

exp = """HOA: v1
States: 2
Start: 0
AP: 2 "b" "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!0] 0
586
[0] 0 {0}
587
[!0&!1] 1
588
[0&!1] 1 {0}
589
590
591
592
593
594
State: 1
[!1] 1 {0}
--END--"""

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