| 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 | } |