Parity Games - Attractor set computation

Question

I do not understand in this game (s0, s1, s2, s3, s4) why S2 is a part of attractor set of S4. 

I understand that S3 is a universal predecessor of S4 and hence part of its attractor set. But S2 can and preferably would pass to S1 (since S2 is a player 0 controlled state)

Now, the argument could be that S2 passes to S1 and S1 being a player 1  controlled state, would pass to S3 (which is already in the attractor set). But in this case, wouldn't S1 also be a part of the attractor set of S4 ?

In conclusion, my question is that what makes S2 a part of the attractor set of S4? 

Thank you

Answer 1

To compute attr(0,{s4}), we have to inspect the predecessor states of s4 which are s2 and s3. Both belong to player 0, so they belong to the attractor since player 0 can enforce from there to reach s4.

Going further, we have to inspect the predecessors of {s2,s3} which needs to consider state s1 which belongs to player 1. Player 1 may however choose the transition to s0, so s1 does not belong to the attractor.