Consider the following state machine:

$($Recall that the dashed line represents a default transition.$)$ For each of the fol$-$

lowing LTL formulas, determine whether it is true or false, and if it is false, give a

counterexample:

$($a$)$ x $=$ Fb

$($b$)$ G$($x $=$ F$($y $=1))$

$($c$)($Gx$)=$ F$($y $=1)$

$($d$)($Gx$)=$ GF$($y $=1)$

$($e$)$ G$(($b $$x$)=$ FGc$)$

$($f$)$ G$(($b $$x$)=$ Gc$)$

$($g$)($GF$$x$)=$ FGc