Weryfikacja wspomagana komputerowo |
Let us conceive a program to solve a consequent problem.
G goats and W wolves travelling together come across the Vistula and want to cross it. There is no bridge, but a boat is on the shores. It can welcome L animals at the same time (who can drive the boat, yes. You are not require to explain how they do that). The trouble is that if at any time in the boat or one of the banks there are strictly more wolves than goats, the predator nature of these otherwise nice animals will take over. And we don’t want any casualty.
Last week, we had a big number of maximum message exchanged. We will try to lower that number.
The idea is that now, each process will have two states: active and passive. At the beginning, everybody is active.
If a process is active, he takes two messages of its two predecessors (p1 then p2) and compare them with his number n. If p1 is bigger than the two others, it updates its number to p1 and stays active. Otherwise, it becomes passive.
If a process is passive, he just passes down whatever he receives.
If an active process receives a message equal to its number as its first message, he concludes that he is the only left active process, send a special message of victory, and then every process passes it down, determining on the way if he is the leader or not (by comparing with its initial number), and when the victory message reaches the sender, he shuts down.
This document was translated from LATEX by HEVEA.