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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
// http://spinroot.com/spin/Doc/Exercises.html
#define MaxSeq 3
#define inc(x) x = (x+1)%(MaxSeq+1)
mtype = { none, red, white, blue } // Wolper's test
bool sent_r, sent_b // initialized to false
bool received_r, received_b // initialized to false
chan q[2] = [MaxSeq] of { mtype, byte, byte }
chan source = [0] of { mtype }
active [2] proctype p5()
{ byte NextFrame, AckExp, FrameExp, r, s, nbuf, i
byte frames[MaxSeq+1]
mtype ball = none
chan inp, out
inp = q[_pid]
out = q[1-_pid]
do
:: nbuf < MaxSeq ->
nbuf++
if
:: _pid%2 -> source?ball
:: else
fi
frames[NextFrame] = ball
out!ball, NextFrame, (FrameExp + MaxSeq) % (MaxSeq + 1)
printf("MSC: nbuf: %d\n", nbuf)
inc(NextFrame)
:: inp?ball,r,s ->
if
:: r == FrameExp ->
printf("MSC: accept %e %d\n", ball, r)
if
:: !(_pid%2) && ball == red -> received_r = true
:: !(_pid%2) && ball == blue -> received_b = true
:: else
fi
inc(FrameExp)
:: else ->
printf("MSC: reject\n")
fi
do
:: ((AckExp <= s) && (s < NextFrame)) ||
((AckExp <= s) && (NextFrame < AckExp)) ||
((s < NextFrame) && (NextFrame < AckExp)) ->
nbuf--
printf("MSC: nbuf: %d\n", nbuf)
inc(AckExp)
:: else ->
printf("MSC: %d %d %d\n", AckExp, s, NextFrame)
break
od
:: timeout ->
NextFrame = AckExp
printf("MSC: timeout\n")
i = 1
do
:: i <= nbuf ->
if
:: _pid%2 -> ball = frames[NextFrame]
:: else
fi
out!ball, NextFrame, (FrameExp + MaxSeq) % (MaxSeq + 1)
inc(NextFrame)
i++
:: else ->
break
od
od
}
active proctype Source()
{
do
:: source!white
:: source!red ->
sent_r = true
break
od
do
:: source!white
:: source!blue ->
sent_b = true
break
od
end: do
:: source!white
od
}
ltl p1 { (<> sent_r -> <> (received_r && !received_b)) }
|
