Figure: Example of CTL