counting atomic propositions and transitions
% cat >aut <<EOF HOA: v1 States: 1 Start: 0 AP: 2 "a" "b" Acceptance: 0 t --BODY-- State: 0  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" acc-name: all Acceptance: 0 t properties: trans-labels explicit-labels state-acc deterministic --BODY-- State: 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:
ap()instead of discovering used atomic propositions so that
--apis more faithful to the input
remove_unused_ap()function, a relevant option in
autfilt, and probably always call this in