1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
/*
* Hajek's THE protocol
*/
#define MAX 8
#define printf(a,b) skip
chan q0 = [1] of { bit, byte };
chan q1 = [1] of { bit, byte };
proctype station(chan inp, out)
{ bit phased, phase, everaccepted, everfetched, c, v;
bit gotack = 1;
byte din, prev_din, dout=1;
do
:: empty(inp) ->
printf("%d empty\n", _pid);
c = 1;
goto pr
:: inp?v,din ->
if
:: c = 0
:: c = 1
fi;
pr: if
:: c == 0 ->
if
:: (!everaccepted && v) || (v != phased) ->
gotack = 1;
:: else
fi;
if
:: (v != phased) || (!everaccepted) ->
printf("%d accept\n", _pid);
assert(din == (prev_din+1)%MAX); /* ACCEPT */
prev_din = din;
everaccepted = 1;
phased = v;
phase = 1 - phase
:: else
fi
:: c != 0 ->
printf("%d error\n", _pid);
fi;
if
:: gotack ->
if
:: everfetched ->
progress: printf("%d fetch\n", _pid);
dout = (dout+1)%MAX
:: else
fi;
everfetched = 1
:: else
fi;
out!phase,dout;
gotack = 0
od
}
init {
atomic {
run station(q0, q1);
run station(q1, q0)
}
}
|
