trunk/verif/Spin/Test/abp

   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 }