never {
s0_init:
    if
    :: (0) -> skip
    fi;
}