Two global int variables, x and y$,$ are initialized to $10$ and $0.$Two threads execute the following statements $($in mixed syntax$)$:

Thread $1$: while $($x $!=$ y$)\{$ x $=$ x $-1$; y $=$ y $+1$; $\}$

Thread $2$: await $($x $==$ y$)$; atomic $\{$ x $=8$; y $=2$; $\}$

Like in Promela, each assignment is an atomic action. Write a Promela model that captures the behavior of this system and

$1.$ Use Spin to check if both threads always terminate, and to show what the final values of x and y can be$.$

$2.$ Explain what happens if the two assignments in Thread $2$ are not done atomically, and confirm your explanation using Spin.

Note: There may $($or may not$)$ be two or more final values.

Hint: Suppose you think that the possible final values are $($x$1,$ y$1)$ and $($x$2,$ y$2).$ Then you need to verify three things:

$1.($x$1,$ y$1)$ is a possible outcome.

$2.($x$2,$ y$2)$ is a possible outcome.

$3.$ Any pair of values other than $($x$1,$ y$1)$ and $($x$2,$ y$2)$ are not possible.