Exam Sept 2022, Problem 8a

Question - S1 = AF(p | q)

S2 = AFp | AFq

In the solution provided, s0 is an empty initial state. s1 is state p with an infinite loop, and s2 is state q with an infinite loop. s0 has path to s1 and s2

Please correct my understanding - For S1 - AF(p|q) is always a path in the future; there is p(s0,s1) or q(s0,s2). So S1 satisfies all three states.

For S2: According to my understanding, There is always a path in the future AF(p) is satisfied in (s0,s1) and AF(q) is satisfied in (s0,s2). How is it not holding in s0?

Please help me understand the significant difference. I appreciate any help you can provide.

Pavithra