Danny Dolev等在1982年提及了一種未改進(jìn)的extreme-find算法，該算法過程簡要描述如下：
算法中使用的消息類型有兩種：
M1：形式為<1，i>；
M2：形式為<2，i>。
其中，i表示存儲在進(jìn)程中的一個數(shù)字。每個進(jìn)程v都含有一個變量max(v)，當(dāng)該進(jìn)程是激活（active）狀態(tài)時，該變量可以用來存儲位于當(dāng)前進(jìn)程左邊的另一個激活的進(jìn)程的變量。
被動的（passive）進(jìn)程僅僅是簡單的傳遞它們接收到的消息。對于算法的描述，我們可以僅僅對其中一個進(jìn)程的行為進(jìn)行描述就可以了。
算法 A0. 發(fā)送消息<1，max(v)>.
A1. 如果接收到一條消息<1，i>，則執(zhí)行以下操作：
1. 如果i≠max(v)則發(fā)送消息<2，i>，并且將i復(fù)制給left(v)。
2. 否則，終止——max(v)是全局最大值。
A2. 如果接受到一條消息<2，i>，則執(zhí)行以下操作：
1. 如果left(v)大于j和max(v)則將left(v)賦值給max(v)，然后發(fā)送消息<1， max(v)>
2. 否則，變?yōu)楸粍舆M(jìn)程。
基于以上的算法描述，我們可以利用Spin建模語言Promela對其進(jìn)行建模如下：
1 mtype = { one, two, winner };
2 chan q[N] = [L] of { mtype, byte};
3
4 proctype node (chan in, out; byte mynumber)
5 { bit Active = 1, know_winner = 0;
6 byte nr, maximum = mynumber, neighbourR;
7
8 xr in;
9 xs out;
10
11 printf("MSC: %d\n", mynumber);
12 out!one(mynumber);
13 end: do
14 :: in?one(nr) ->
15 if
16 :: Active ->
17 if
18 :: nr != maximum ->
19 out!two(nr);
20 neighbourR = nr
21 :: else ->
22 know_winner = 1;
23 out!winner,nr;
24 fi
25 :: else ->
26 out!one(nr)
27 fi
28
29 :: in?two(nr) ->
30 if
31 :: Active ->
32 if
33 :: neighbourR > nr && neighbourR > maximum ->
34 maximum = neighbourR;
35 out!one(neighbourR)
36 :: else ->
37 Active = 0
38 fi
39 :: else ->
40 out!two(nr)
41 fi
42 :: in?winner,nr ->
43 if
44 :: nr != mynumber ->
45 printf("MSC: LOST\n");
46 :: else ->
47 printf("MSC: LEADER\n");
48 nr_leaders++;
49 assert(nr_leaders == 1)
50 fi;
51 if
52 :: know_winner
53 :: else -> out!winner,nr
54 fi;
55 break
56 od
57 }
該模型描述了每個進(jìn)程節(jié)點(diǎn)的行為，通過該算法，可以找出網(wǎng)絡(luò)中的領(lǐng)導(dǎo)者。算法的計(jì)算復(fù)雜度為2nlogn+O(n) 。