Skip to content

accepting SCC incorrectly reported as rejecting by scc_info

Reported by Heňo.

On this automaton:

HOA: v1
States: 4
Start: 2
AP: 2 "p1" "p0"
acc-name: generalized-co-Buchi 2
Acceptance: 2 Fin(0)|Fin(1)
properties: trans-labels explicit-labels state-acc complete
properties: deterministic
--BODY--
State: 0 {0}
[1] 0
[!1] 1
State: 1 {0 1}
[1] 0
[!1] 1
State: 2
[0&1] 0
[0&!1] 1
[!0&1] 2
[!0&!1] 3
State: 3 {1}
[0&1] 0
[0&!1] 1
[!0&1] 2
[!0&!1] 3
--END--

we get:

autfilt --dot='sbarf(Lato)' hl2.hoa

hl2

where the second SCC is marked as rejecting despite the accepting loop above state 0.

Seems like a bug in scc_info.

Edited by Alexandre Duret-Lutz