Three people, P$1,$ P$2,$ and P$3,$ want to find the earliest meeting date d$.$ Each P is available every ai days starting from day bi bi $$ ai$),$ i$.$e$.,$ Pi $$s available days are bi$,$ ai $+$ bi$,2$ai $+$ bi$,...$

Let fi be a function that maps the $($current$)$ candidate date t to Pi$$s earliest available date on or after t$.$ Clearly, fi$($t$)>=$ t$,$ and fi$($u$)!=$ u holds for all u such that t u $$ fi$($t$).$

To find the earliest meeting date d$,$ they $($who don$$t know the other people$$s ai and bi$)$ start communication using a ring of message channels $($see figure$).$ They have no other means of communication $($such as shared global variables$).$

Each Pi locally holds his$/$her own candidate date di whose initial value is $0($representing today$),$ and asynchronously and repeatedly performs the following:

$-$update di to his$/$her earliest available date fi$($di$)$ and send it to the next person,$$

$-$receive the previous person$$s candidate date dj and update di to dj if dj$>$di$.$

$($Note: if you think the above rules are underspecified or inaccurate, you may refine them as necessary.$)$

Anybody can start communication independently.

The communication can terminate when all the Pi$$s realize that no further updates of di will be made.

Q$1$ Describe the above algorithm in Promela and test it with a$1=5,$ a$2=6$ and a$3=7.$ For bi$,$ we know that bi for each i but not their exact values. Use the verification mode to figure out

$($i$)$ the largest possible value of the earliest meeting date d and

$($ii$)$ which bi$$s lead to that meeting date.

Q$2$How can each Pi notice that no further updates of di will be made

$($and communication can be stopped$)?$ Design and implement a termination mechanism and verify that the algorithm always terminate$($with a$1=5,$ a$2=6$ and a$3=7).$