Consider the following PROMELA program that sorts two

non$-$zero numbers in order:

proctype sort$($int x$,$y$)\{$

int temp;

do

:: $($x goto done

:: $($x$>$y$)->$ temp $=$ x;

x$=$y;

y$=$temp

:: $($x$==$y$)->$ goto done

od;

done:

printf$("$The order is: $\%$d$,\%$dFollowing

$",$ x$,$ y$)$

$\}$

init $\{$run sort$(14,15)\}$

Following the style of program illustrated in the above example of using

expression run, re$-$write PROMELA program Maximum we

discussed in Lecture Two $($the attached image$)$ and run it using SPIN.