The FSM below shows a simple traffic lights controller, which has $3$ states Green, Yellow, and Red $($denoted as S$0,$ S$1,$ and S$2,$ respectively$).$ Check whether the four LTL properties in Problem $2$ are satisfied by the FSM$.$ If not, give a counterexample of the system path that violates the LTL property. $($Note: A state machine starting from some initial states $\backslash ($ s$\_\{0\}\backslash )$ satisfies an LTL property $\backslash (\backslash$varphi $\backslash )$ if all system paths starting in $\backslash ($ s$\_\{0\}\backslash )$ satisfy the property $\backslash (\backslash$varphi $\backslash ).)$