in s0, a and thus also Fa are satisfied. From s1 on, we never see a again. Hence, Fa is not satisfied in s1. The weak until is satisfied if either the left side holds forever or at least to the point before the point when the right side is satisfied. Since b is nowhere satisfied, we'd have the left side forever but it is only satisfied in the first step. Thus, S1 isn't satisfied.