Problem $2(40\backslash \%)$

Express the following properties using LTL formulas

$1)$ The light is always green.

$2)$ Whenever the light is red, it eventually becomes green.

$3)$ Whenever the light is green, it remains green until it becomes yellow.

$4)$ Whenever the light is yellow, it becomes read immediately after.

Problem $3(40\backslash \%)$

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 ).)$