0b55f123 |
1 | /* |
2 | * a simple example of the use of inline's |
3 | * (requires Spin version 3.2 or later) |
4 | * |
5 | */ |
6 | |
7 | mtype = { msg0, msg1, ack0, ack1 }; |
8 | |
9 | chan sender = [1] of { mtype }; |
10 | chan receiver = [1] of { mtype }; |
11 | |
12 | inline phase(msg, good_ack, bad_ack) |
13 | { |
14 | do |
15 | :: sender?good_ack -> break |
16 | :: sender?bad_ack |
17 | :: timeout -> |
18 | if |
19 | :: receiver!msg; |
20 | :: skip /* lose message */ |
21 | fi; |
22 | od |
23 | } |
24 | |
25 | inline recv(cur_msg, cur_ack, lst_msg, lst_ack) |
26 | { |
27 | do |
28 | :: receiver?cur_msg -> sender!cur_ack; break /* accept */ |
29 | :: receiver?lst_msg -> sender!lst_ack |
30 | od; |
31 | } |
32 | |
33 | active proctype Sender() |
34 | { |
35 | do |
36 | :: phase(msg1, ack1, ack0); |
37 | phase(msg0, ack0, ack1) |
38 | od |
39 | } |
40 | |
41 | active proctype Receiver() |
42 | { |
43 | do |
44 | :: recv(msg1, ack1, msg0, ack0); |
45 | recv(msg0, ack0, msg1, ack1) |
46 | od |
47 | } |