counting atomic propositions and transitions
% cat >aut <<EOF
HOA: v1
States: 1
Start: 0
AP: 2 "a" "b"
Acceptance: 0 t
BODY
State: 0
[1] 0
END
EOF
This automaton declares two atomic propositions, but uses only one. So its single edge should count as two transitions.
Yet Spot counts it as a single transition, because the algorithm counting transitions only consider the atomic propositions that are actually used.
% autfilt stats=%t aut
1
A related issue (?) is
% autfilt ap=2 aut
HOA: v1
States: 1
Start: 0
AP: 1 "b"
accname: all
Acceptance: 0 t
properties: translabels explicitlabels stateacc deterministic
BODY
State: 0
[0] 0
END
which shockingly prints an automaton with a single atomic proposition, even though we filtered automata that have 2 atomic propositions. This is because ap
use the declared number of atomic propositions, while print_hoa()
outputs only the used propositions.
I suggests the following changes:

change
twa_sub_statistics()
to useap()
instead of discovering used atomic propositions so thatap
is more faithful to the input 
change
print_hoa()
to honorap()

introduce a
remove_unused_ap()
function, a relevant option inautfilt
, and probably always call this inpostproc
. 
introduce a
usedap
filter toautfilt
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information