Alternate CTL solution

Question

For this question I worked out -> EFEG[AFXGa SU EXEFEGb]

Is my answer a valid CTL as well?

Comments

I don't think that this is correct. Where did you get the EG after the EF from?

Answer 1

It is definitely not a CTL formula since EFEG[AFXGa SU EXEFEGb] has temporal operators that are not preceded by a path quantifier. Moreover, you smuggled in the EG without justification, I don't see why that should hold.

Comments

I see the mistakes now. My usage of the templates seems dodgy. Also it is clear that AFXGa is a problematic term and I should have focused on dealing with that first.
Thanks.