An example of BA translation that is better than its original TGBA
In this example a TGBA with 2 acceptance sets is degeneralized into a BA with one transition less (a self loop is removed).
% ltl2tgba -H 'GF(!a & X!a & Fa)'
HOA: v1
name: "GF(!a & X!a & Fa)"
States: 3
Start: 0
AP: 1 "a"
acc-name: generalized-Buchi 2
Acceptance: 2 Inf(0)&Inf(1)
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[t] 0 {0}
[!0] 1 {1}
State: 1
[!0] 1 {1}
[!0] 2
State: 2
[0] 0 {0}
--END--% ltl2tgba -BH 'GF(!a & X!a &Fa)'
HOA: v1
name: "GF(!a & X!a & Fa)"
States: 3
Start: 2
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[!0] 1
State: 1 {0}
[0] 2
State: 2
[!0] 0
[t] 2
--END--If we disable the simulation on the BA, we get a BA with the same structure as the original TGBA.
% ltl2tgba -x ba-simul=0 -BH 'GF(!a & X!a &Fa)'
HOA: v1
name: "GF(!a & X!a & Fa)"
States: 3
Start: 0
AP: 1 "a"
acc-name: Buchi
Acceptance: 1 Inf(0)
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0
[t] 0
[!0] 1
State: 1
[!0] 1
[!0] 2
State: 2 {0}
[0] 0
--END--It would be nice to have a similar reduction on the TGBA.
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information