StopAndWait.prot

// Stop-and-Wait protocol, where process A waits for B
// to receive its message before sending a new one.
//
// For stabilization, we must have (SeqSz > AB + BA).

// Size of message and sequence number.
constant MsgSz := 3;
constant SeqSz := 3;

// Size of channels from A to B and B to A.
constant AB := 1;
constant BA := 1;

// Used for determining next message in somewhat variable way.
constant DiffSz := MsgSz-1;

puppet variable msg[(2+AB)] < MsgSz;
puppet variable seq[(2+AB+BA)] < SeqSz;

shadow variable y[2] < MsgSz;
direct variable d[1] < DiffSz;

((future & shadow) % puppet)
  (y[0]==y[1] || y[0]==(y[1]+d[0]+1)%MsgSz);


process A[id < 1]
{
  let i := 0;

  write: y[0];
  read: y[1];

  write: seq[i];
  read: seq[i-1];

  write: msg[i];
  read: d[0];

  // Value of {msg} should represent {y}.
  (assume & closed)  (y[0]==msg[0]);

  shadow: ( y[0]==y[1] --> y[0]:=y[0]+d[0]+1; );

  puppet:
    ( seq[i]==seq[i-1] --> msg[i]:=msg[i]+d[0]+1; seq[i]:=seq[i]+1; y[0]:=msg[i]+d[0]+1; )
    ;
}


process B[id < 1]
{
  let i := AB+1;

  read: y[0];
  write: y[1];

  read: seq[i-1];
  write: seq[i];

  read: msg[i-1];
  write: msg[i];

  // Value of {msg} should represent {y}.
  (assume & closed)  (y[1]==msg[i]);

  // Keep receiving new messages within the legitimate states.
  shadow: ( y[0]!=y[1] --> y[1]:=y[0]; );

  puppet:
    ( msg[i]!=msg[i-1] || seq[i]!=seq[i-1] --> msg[i]:=msg[i-1]; seq[i]:=seq[i-1]; y[1]:=msg[i-1]; )
    ;
}


// Channel from A to B.
process CommAB[id < AB]
{
  let i := id+1;
  read: msg[i-1];
  read: seq[i-1];
  write: msg[i];
  write: seq[i];

  puppet: ( msg[i]!=msg[i-1] || seq[i]!=seq[i-1] --> msg[i]:=msg[i-1]; seq[i]:=seq[i-1]; );
}

// Channel from B to A.
process CommBA[id < BA]
{
  let i := id+AB+2;
  read: seq[i-1];
  write: seq[i];

  puppet: ( seq[i]!=seq[i-1] --> seq[i]:=seq[i-1]; );
}