I am unable to interpret how the below formula works for CTL model checking.

S4=A F b | E [a SU a]

The answer received from the tool is: **{s0;s1;s2;s6}**.

However, I got the following states when I tried computing:

a = {s1}; (i.e., a is true only in s1)

E[a __U__** **a] = {s1}; (i.e., run where a __U__ a holds)

Fb = {s0, s1, s3, s4, s5, s6}; (i.e., There is an infinite path (s0 to s4 and back to s0), starting from s0, which makes sure Fb is true at s0 and traversal through s0 via all states will still satisfy Fb).

AFb = {s0, s1, s2, s3, ..., s6} (i.e., Every run will eventully reach Fb states and s2 satisfies trivially.)

Hence, I end up with the answer, i.e., **E[a **__U__ a] | AFb = {s0, s1, s2, s3, ..., s6}

Kindly request some help in understanding where I'm going wrong. Also, thanks in advance for all the support given so far.