Multiple initial states inccorrectly handled
I am using Spot 2.11.6.dev (rev 9957aa1a).
The following Buchi automaton has 4 initial states.
An issue is that autfilt --is-deterministic
returns true.
On the other hand, when adding deterministic
as a property in the HOA file, autfilt
outputs deterministic automata should have at most one initial state
.
Moreover autfilt --stats='%[r]S, %[u]S; %[r]s, %[u]s' --remove-unreachable-states
returns
61, 3; 61, 0
which suggests it considers 3 (out of the 4) initial states as unreachable.
HOA: v1
States: 64
Start: 4
Start: 19
Start: 34
Start: 49
AP: 13 "l0" "l1" "l2" "l3" "l4" "l5" "l6" "l7" "l8" "l9" "l10" "l11" "l12"
acc-name: Buchi
Acceptance: 1 Inf(0)
--BODY--
State: 0 {0}
[(!0&1&2&!3&4&!5&6&7&!8&9&!10&!11&12)] 0
State: 1 {0}
[(!0&1&!2&3&4&!5&6&7&!8&9&!10&!11&12)] 1
State: 2 {0}
[(!0&1&2&!3&!4&5&6&7&!8&9&!10&!11&12)] 2
State: 3 {0}
[(!0&1&!2&3&!4&5&6&7&!8&9&!10&!11&12)] 3
State: 4 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 5
State: 5 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 6
State: 6 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 7
State: 7 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 8
State: 8 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 9
State: 9 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 10
State: 10 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 11
State: 11 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 12
State: 12 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 13
State: 13 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 14
State: 14 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&11&!12)] 15
State: 15 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&!11&12)] 16
State: 16 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&!11&12)] 17
State: 17 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&!11&12)] 18
State: 18 {0}
[(!0&1&2&!3&4&!5&!6&7&!8&9&!10&!11&12)] 0
State: 19 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 20
State: 20 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 21
State: 21 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 22
State: 22 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 23
State: 23 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 24
State: 24 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 25
State: 25 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 26
State: 26 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 27
State: 27 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 28
State: 28 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 29
State: 29 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&11&!12)] 30
State: 30 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&!11&12)] 31
State: 31 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&!11&12)] 32
State: 32 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&!11&12)] 33
State: 33 {0}
[(!0&1&!2&3&4&!5&!6&7&!8&9&!10&!11&12)] 1
State: 34 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 35
State: 35 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 36
State: 36 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 37
State: 37 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 38
State: 38 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 39
State: 39 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 40
State: 40 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 41
State: 41 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 42
State: 42 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 43
State: 43 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 44
State: 44 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&11&!12)] 45
State: 45 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&!11&12)] 46
State: 46 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&!11&12)] 47
State: 47 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&!11&12)] 48
State: 48 {0}
[(!0&1&2&!3&!4&5&!6&7&!8&9&!10&!11&12)] 2
State: 49 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 50
State: 50 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 51
State: 51 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 52
State: 52 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 53
State: 53 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 54
State: 54 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 55
State: 55 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 56
State: 56 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 57
State: 57 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 58
State: 58 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 59
State: 59 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&11&!12)] 60
State: 60 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&!11&12)] 61
State: 61 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&!11&12)] 62
State: 62 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&!11&12)] 63
State: 63 {0}
[(!0&1&!2&3&!4&5&!6&7&!8&9&!10&!11&12)] 3
--END--