2 * a simple example of the use of inline's
3 * (requires Spin version 3.2 or later)
7 mtype = { msg0, msg1, ack0, ack1 };
9 chan sender = [1] of { mtype };
10 chan receiver = [1] of { mtype };
12 inline phase(msg, good_ack, bad_ack)
15 :: sender?good_ack -> break
20 :: skip /* lose message */
25 inline recv(cur_msg, cur_ack, lst_msg, lst_ack)
28 :: receiver?cur_msg -> sender!cur_ack; break /* accept */
29 :: receiver?lst_msg -> sender!lst_ack
33 active proctype Sender()
36 :: phase(msg1, ack1, ack0);
37 phase(msg0, ack0, ack1)
41 active proctype Receiver()
44 :: recv(msg1, ack1, msg0, ack0);
45 recv(msg0, ack0, msg1, ack1)