alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tra2tba: Merge edges of resulting automaton

Browse source 
* spot/twaalgos/tra2tba.cc: Call 'merge_edges'
* tests/python/tra2tba.py: Update tests
This commit is contained in:
xlauko 2017-06-13 18:45:49 +02:00 • committed by Alexandre Duret-Lutz
parent 69cf3c5590
commit bd8ede6226
2 changed files with 24 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/tra2tba.cc
View file

@ -310,6 +310,8 @@ namespace spot
res->prop_complete(complete); res->prop_complete(complete);
res->prop_universal(deterministic); res->prop_universal(deterministic);
res->purge_dead_states(); res->purge_dead_states();
res->merge_edges();
return res; return res;
} }

50
tests/python/tra2tba.py
View file

@ -225,24 +225,20 @@ Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc properties: trans-labels explicit-labels trans-acc
--BODY-- --BODY--
State: 0 State: 0
[0&1] 1 [!1] 0
[0&!1] 0 [1] 1
[!0&1] 1
[!0&!1] 0
[0&!1] 2 [0&!1] 2
State: 1 State: 1
[0&1] 1 {0} [!1] 0 {0}
[0&!1] 0 {0} [1] 1 {0}
[!0&1] 1 {0}
[!0&!1] 0 {0}
[0&1] 3
[0&!1] 2 [0&!1] 2
[0&1] 3
State: 2 State: 2
[0&1] 3 {0}
[0&!1] 2 {0} [0&!1] 2 {0}
[0&1] 3 {0}
State: 3 State: 3
[0&1] 3 {0}
[0&!1] 2 {0} [0&!1] 2 {0}
[0&1] 3 {0}
--END--""" --END--"""
res = spot.tra_to_tba(aut) res = spot.tra_to_tba(aut)
@ -274,8 +270,7 @@ Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc properties: trans-labels explicit-labels state-acc
--BODY-- --BODY--
State: 0 State: 0
[0] 0 [t] 0
[!0] 0
[0] 1 [0] 1
State: 1 {0} State: 1 {0}
[0] 1 [0] 1
@ -330,17 +325,17 @@ Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels trans-acc properties: trans-labels explicit-labels trans-acc
--BODY-- --BODY--
State: 0 State: 0
[!0&1&2] 3
[!0&1&!2 | 0&!1&!2] 4
[!0&!1 | 0&1] 1 [!0&!1 | 0&1] 1
[0&!1&2] 2 [0&!1&2] 2
[!0&1&2] 3
[!0&1&!2 | 0&!1&!2] 4
State: 1 State: 1
[t] 1 {0} [t] 1 {0}
State: 2 State: 2
[0&2] 5
[0&!2] 6
[!0&2] 3 [!0&2] 3
[!0&!2] 4 [!0&!2] 4
[0&2] 5
[0&!2] 6
State: 3 State: 3
[0&2] 2 [0&2] 2
[!0&2] 3 [!0&2] 3
@ -348,14 +343,14 @@ State: 3
State: 4 State: 4
[t] 4 [t] 4
State: 5 State: 5
[0&2] 5
[0&!2] 6
[!0&2] 3 [!0&2] 3
[!0&!2] 4 [!0&!2] 4
[0&2] 5
[0&!2] 6
[0&2] 7 [0&2] 7
State: 6 State: 6
[0] 6 {0}
[!0] 4 [!0] 4
[0] 6 {0}
State: 7 State: 7
[0&2] 7 {0} [0&2] 7 {0}
--END--""" --END--"""
@ -389,11 +384,11 @@ Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc deterministic properties: trans-labels explicit-labels state-acc deterministic
--BODY-- --BODY--
State: 0 {0} State: 0 {0}
[1&!2] 1
[!1&!2] 0 [!1&!2] 0
[1&!2] 1
State: 1 State: 1
[1&!2] 1
[!1&!2] 0 [!1&!2] 0
[1&!2] 1
--END--""" --END--"""
res = spot.tra_to_tba(aut) res = spot.tra_to_tba(aut)
@ -426,9 +421,8 @@ Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc properties: trans-labels explicit-labels state-acc
--BODY-- --BODY--
State: 0 State: 0
[0&1] 0 [0] 0
[!0&1] 1 [!0&1] 1
[0&!1] 0
[0&1] 2 [0&1] 2
State: 1 {0} State: 1 {0}
[1] 1 [1] 1
@ -466,11 +460,11 @@ properties: trans-labels explicit-labels trans-acc complete
properties: deterministic properties: deterministic
--BODY-- --BODY--
State: 0 State: 0
[!0] 0 {0}
[0] 1 [0] 1
[!0] 0 {0}
State: 1 State: 1
[0] 1 {0}
[!0] 0 {0} [!0] 0 {0}
[0] 1 {0}
--END--""" --END--"""
res = spot.tra_to_tba(aut) res = spot.tra_to_tba(aut)
@ -504,13 +498,13 @@ Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc properties: trans-labels explicit-labels state-acc
--BODY-- --BODY--
State: 0 State: 0
[0] 1
[!0] 0 [!0] 0
[0] 1
[!0] 2 [!0] 2
[!0] 3 [!0] 3
State: 1 State: 1
[0] 1
[!0] 0 [!0] 0
[0] 1
[!0] 3 [!0] 3
State: 2 State: 2
[!0] 2 [!0] 2