# CTL trouble translating text into formula

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?

$$\newcommand{AF}{\text{AF}\;}\newcommand{AG}{\text{AG}\;}$$Try to decode this:

For each path:

• In the future: p and
• In the future q and
• Always in the future not p

You correctly concluded that the correct formula is

$$\AF \left( p \land \AF \left( q \land \AG \neg p \right) \right).$$

The key thing to understand about CTL is that when you evaluate things like $$\AF (p \land \AF q)$$ then this is true if somewhere in the future $$p \land \AF q$$ is true, which means that $$\AF q$$ is evaluated in the state where $$p$$ is true.

• $AF(p \land AF(q \land AF AG(-p)))$ Dec 12, 2021 at 8:58
• The problem is I dont know how to express "in the future" because I only have aviable $A$ and $E$ Dec 12, 2021 at 9:12
• I always feel bad if dont get the hints people give me sorry xD. Im going to try it again. I already knew what that meant, there are even more great combinations :) Dec 12, 2021 at 10:26
• Im just thinking about how to state for all path excluded the path i've already been Dec 12, 2021 at 10:27
• I think I see. Due to the stacked and we find automatically the structure of a series. Dec 12, 2021 at 10:41