I have an excercise where I have to translate verbally formulated statements into CTL formulas. I have particularly trouble with this one:
On every path q is true at least once and p was true sometime before, after no longer. My attempt is the following: $AF q \land (EF p) AU q$
This is obvously wrong. The first part is easy, then the second is more difficult. What I've stated there implies that there exists a path to $p$ before $q$ but not that $p$ was true on the previous path, and the third part to me looks impossible. Can anyone help?