NAME dekker VAR wantp$1$ : boolean; wantp$2$ : boolean; turn : $\{0,1,2\}$; pc$1$: $\{0,1,2\}$; $--$ not in critical section, in busy wait, in critical section pc$2$: $\{0,1,2\}$; $--$ not in critical section, in busy wait, in critical seciton INIT pc$1=0$ & pc$2=0$ & $!$wantp$1$ & $!$wantp$2$ & turn$=0$; RULES $--$ process $1$ pc$1=0$: wantp$1$ :$=$ true; if $($turn $=0$ & wantp$1)$ turn :$=1$ else skip fi; if $($wantp$2)$ if $($turn $=2)$ wantp$1$ :$=$ false; pc$1$ :$=1--$ go to busy wait else pc$1$ :$=2$ fi else pc$1$ :$=2$ fi pc$1=1$: $--$ in busy wait if $($turn $=1)$ wantp$1$ :$=$ true; pc$1$ :$=2$ else pc$1$ :$=1$ fi pc$1=2$: $--$ in critical section turn :$=2$; wantp$1$ :$=$ false; pc$1$ :$=0--$ process $2$ pc$2=0$: wantp$2$ :$=$ true; if $($turn $=0$ & wantp$2)$ turn :$=2$ else skip fi; if $($wantp$1)$ if $($turn $=1)$ wantp$2$ :$=$ false; pc$2$ :$=1--$ go to busy wait else pc$2$ :$=2$ fi else pc$2$ :$=2$ fi pc$2=1$: $--$ in busy wait if $($turn $=2)$ wantp$2$ :$=$ true; pc$2$ :$=2$ else pc$2$ :$=1$ fi pc$2=2$: $--$ in critical section turn :$=1$; wantp$2$ :$=$ false; pc$2$ :$=01.$ Use CTL formulas to express the mutual exclusion and freedom from starvation properties of Dekker$$s mutual exclusion algorithm. There can be more than one CTL formula needed to express each property. If you write more than $3$ formulas for each property, you will be penalised by deducting marks. $2.$ For each formula, explain whether it is a liveness or safety property. Execute the formulas on the model and report the results. $3.$ Use these results to detect a bug. Describe a buggy execution in your report. $4.$ Draw the Kripke structure of the code.