Show $\textbf{AGF}p$ and $\textbf{AGEF}p$ specify different properties. I want to show that $\textbf{AGF}p$ and $\textbf{AGEF}p$ specify different properties.
The finite state diagram I drew:

My proof:
"    This model satisfies $\textbf{AGEF}p$ since $s_0(s_1)^\omega\vDash\textbf F p$ and $s_0s_2(s_3)^\omega\vDash\textbf F p$, but it doesn't satisfy $\textbf{AGF}p$ since $s_0(s_2)^\omega\nvDash\textbf F p$. "
I don't know whether my answer is totally correct or not because this is a comparison between a CTL* and a CTL formula, can somebody provides some suggestions?
Ref: Computation tree logic - Wikipedia
Thanks a lot!
Simplify Version
Give a model $\mathcal M = (S, \to, L)$ and $s\in S$ in below:



*

*The formula $\textbf{AGF}p$ is true in model $\mathcal M$ at state $s_0$ if from every state on every path
from $s_0(\textbf{AG})$, $p$ is eventually true$(\textbf F p)$ on that same path, and $s_0^{\omega_0}$ doesn't hold.

*The formula $\textbf{AGEF}p$ is true in model $\mathcal M$ at state $s_0$ if from every state on every path from $s_0(\textbf{AG})$, there exists a path on which $p$ is eventually true($\textbf{EF}p$), and $s_0(s_1)^{\omega_1}$ holds.    
Thus $\mathcal M, s_0\nvDash\textbf{AGF}p$ but $\mathcal M, s_0\vDash\textbf{AGEF}p$. 
 A: If you label $s_0$ with either $p$ or $\neg p$, then your structure is completely defined and, either way, is  a model of $\operatorname{\mathsf{AGEF}} p$, but not of $\operatorname{\mathsf{AGF}} p$.
Part of the proof still needs some work.  For the formula $\operatorname{\mathsf{AGF}} p$, producing a path like $s_0s_2^{\,\omega}$ along which $\operatorname{\mathsf{GF}} p$ does not hold is enough.  For the formula $\operatorname{\mathsf{AGEF}} p$, you need to argue that every state reachable from $s_0$ (that is, every state of the structure) satisfies $\operatorname{\mathsf{EF}} p$.
Note that now that you have a structure that illustrates the difference between $\operatorname{\mathsf{AGEF}} p$ and $\operatorname{\mathsf{AGF}} p$, you can try to simplify it.  (You only need two states.)
As for the general issue of comparing CTL formulae to CTL$^*$ formulae, every CTL formula is also a CTL$^*$ formula with the same "meaning," in the sense that it holds in precisely the same structures.  So, if you reason in CTL$^*$, all is well.  
In practice, though, you want to think of $\operatorname{\mathsf{AGEF}} p$ as a CTL formula, and of $\operatorname{\mathsf{GF}} p$ as an LTL formula, because answering both model checking questions is then immediate.  The semantic argument you used (here's a structure that is a model for one, but not for the other; hence the two formulae are not equivalent) is perfectly fine.  It is indeed the standard way to address issues of expressiveness of different logics or fragments thereof.
