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"
acc-name: all
Acceptance: 0 t
properties: trans-labels explicit-labels state-acc 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 use ap() instead of discovering used atomic propositions so that --ap is more faithful to the input
• change print_hoa() to honor ap()
• introduce a remove_unused_ap() function, a relevant option in autfilt, and probably always call this in postproc.
• introduce a --used-ap filter to autfilt