Consider t he folowing PROMELA program code:

byte critical $=1$;

bool formalSW $=$ false;

active proctype P$()\{$

do

:: printf$("$Noncritical section P$")$;

critical $==1$;

printf$("$Critical section P$")$;

critical $=2$;

od

$\}$

active proctype Q$()\{$

do

:: printf$("$Noncritical section Q$")$;

critical $==2$;

formalSW $=$ true;

printf$("$Critical section Q$")$;

formalSW $=$ false;

critical $=1$;

od

$\}$

Define the mutual exclusion $($safety$)$ and liveness $($absence of

starvation$)$ properties for this program, and use SPIN to check if

the program satisfies these properties.