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 useap()
instead of discovering used atomic propositions so that--ap
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 --used-ap
filter toautfilt