attr1({s0}) is the set of states where player 1 can enforce that state s0 is reached, no matter what player 0 will do. Player 1 controls the rectangled states, so all rectangled states that can reach s0 only through rectangled states belong to attr1({s0}). This way, we get s1,s2,s8, but s4 and s6 have to pass through states controlled by player 0, and unfortunately, s3 can always select the transition to s4 so that the states s3,s4,s5,s6,s7 do not belong to attr1({s0}). Hence, attr1({s0}) = {s0,s1,s2,s8}