I have updated the WL(1) implementation to iterate until fixpoint termination, and mentioned the failure case. Thank you for reading carefully!