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
|
/*
* a simple example of the use of inline's
* (requires Spin version 3.2 or later)
*
*/
mtype = { msg0, msg1, ack0, ack1 };
chan sender = [1] of { mtype };
chan receiver = [1] of { mtype };
inline phase(msg, good_ack, bad_ack)
{
do
:: sender?good_ack -> break
:: sender?bad_ack
:: timeout ->
if
:: receiver!msg;
:: skip /* lose message */
fi;
od
}
inline recv(cur_msg, cur_ack, lst_msg, lst_ack)
{
do
:: receiver?cur_msg -> sender!cur_ack; break /* accept */
:: receiver?lst_msg -> sender!lst_ack
od;
}
active proctype Sender()
{
do
:: phase(msg1, ack1, ack0);
phase(msg0, ack0, ack1)
od
}
active proctype Receiver()
{
do
:: recv(msg1, ack1, msg0, ack0);
recv(msg0, ack0, msg1, ack1)
od
}
|
