/* Sliding window modelled as a modular high-level net
 * for the maria tool (http://www.tcs.hut.fi/Software/maria/).
 * Model constructed by Marko Mäkelä (msmakela@tcs.hut.fi), March 1, 2004.
 */

/** data payload */
#ifdef TESTER
typedef enum { a, b } payload_t;
bool is_b (payload_t data) data == is payload_t b;
#else // TESTER
typedef enum { c } payload_t;
#endif // TESTER

/* the synchronising transitions for producer and consumer */
trans :produce { payload_t data; };
trans :consume { payload_t data; };

/** producer process */
subnet producer
{
  /** payload */
  place p (#payload_t) payload_t const: payload_t p: p;
#ifdef TESTER
  /** flag: has a 'b' message been produced? */
  place sent_b (1) bool: false;
  deadlock !(place sent_b equals true) && fatal;
  
  /** produce a random piece of data */
  trans produce:trans produce
  in { place p: data; place sent_b: false; }
  out { place p: data; place sent_b: is_b (data); };
#else // TESTER
  trans produce:trans produce in { place p: data; } out { place p: data; };
#endif // TESTER
};

/** consumer process */
subnet consumer
{
  trans consume:trans consume;
};

/** Size of the transmission window */
unsigned tw = 1;
/** Size of the reception window */
unsigned rw = 1;
/** Amount of different sequence numbers (must be at least tw + rw - 1) */
unsigned w = tw + rw - 1;

/** Sequence numbers */
typedef unsigned (0..w) seq_t;

/* the synchronisation transitions for sender and receiver processes */
trans :send_msg { seq_t seq; payload_t data; };
trans :recv_msg { seq_t seq; payload_t data; };
trans :send_ack { seq_t seq; };
trans :recv_ack { seq_t seq; };

/** Modulus addition: (x + y) mod w */
seq_t modP (unsigned x, unsigned y) is seq_t ((x + y) % (w + 1));
/** Modulus subtraction: (x - y) mod w */
unsigned modM (unsigned x, unsigned y) (((w + 1) + x - y) % (w + 1));

/** sender process */
subnet sender
{
  /** transmission window indexes */
  typedef unsigned (0..tw) twindow_t;
  /** transmission buffer type */
  typedef payload_t[queue tw] tbuf_t;

  /** transmission buffer */
  place tbuf (1) tbuf_t: {};

  /** index of last available data item, plus one */
  place i (1) twindow_t: 0;
  /** index of next data item to be sent */
  place j (1) twindow_t: 0;
  /** sequence number for the first unacknowledged message */
  place seq (1) seq_t: 0;

  /** enqueue a data packet */
  trans enqueue:trans produce
  in {
    place i: i; place tbuf: tbuf;
  }
  out {
    place i: +i; place tbuf: tbuf + data;
  }
  gate i < tw;

  /** Send the next message from the input buffer */
  trans send_msg
  in {
    place i: i;
    place j: j;
    place seq: k;
    place tbuf: tbuf;
  }
  gate j < i
  {
    seq_t seq = modP (j, k);
    payload_t data = *tbuf[j];
  }
  : trans send_msg
  out {
    place i: i;
    place j: +j;
    place seq: k;
    place tbuf: tbuf;
  };

  /** Receive or ignore an acknowledgement,
   * depending on whether the sequence number
   * is within the transmission window. */
  trans recv_ack:trans recv_ack
  in {
    place i: i;
    place j: j;
    place seq: k;
    place tbuf: tbuf;
  }
  { unsigned a = modM (seq, k) + 1; }
  out {
    place i: a <= tw ? is twindow_t (is unsigned i < a ? 0 : i - a) : i;
    place j: a <= tw ? is twindow_t (is unsigned j < a ? 0 : j - a) : j;
    place seq: a <= tw ? +seq : k;
    place tbuf: a <= tw ? tbuf - a : tbuf;
  };

  /** Timeout (retransmission) */
  trans timeout
  in { place i: i; place j: i; }
  gate i > 0
  out { place i: i; place j: 0; };
};

/** receiver process */
subnet receiver
{
  /** Received sequence number */
  typedef unsigned (0..rw-1) rseq_t;

  /** Received data to be forwarded to the consumer */
  typedef payload_t[rseq_t] rbuf_t;
  place rbuf (1) rbuf_t: <rbuf_t;

  /** Acknowledged sequence numbers */
  typedef bool[rseq_t] ackarray_t;
  /** Acknowledged sequence numbers */
  place ackarray (1) ackarray_t: <ackarray_t;
  /** Expected sequence number */
  place e (1) seq_t: 0;

  /** Flag: receiving (true) or acknowledging (false) */
  place recv (1) bool: true;

  /** Receive a message, and accept or ignore it,
   * depending on whether it is within the reception window */
  trans recv_msg:trans recv_msg
  in {
    place recv: true;
    place e: e;
    place rbuf: rbuf;
    place ackarray: r;
  }
  { unsigned s = modM (seq, e) }
  { bool expected = s < rw; }
  out {
    place recv: false;
    place e: e;
    place rbuf: expected ? rbuf.{[is rseq_t s] data} : rbuf;
    place ackarray: expected ? r.{[is rseq_t s] true} : r;
  };

  /** Dequeue received data */
  trans dequeue:trans consume
  in {
    place recv: false;
    place rbuf: rbuf;
    place ackarray: r;
    place e: e;
  }
  gate r[0]
  { payload_t data = rbuf[0]; }
  out {
    place recv: false;
    place rbuf: (rbuf << 1).{ [rw - 1] < payload_t };
    place ackarray: (r << 1).{ [rw - 1] false };
    place e: +e;
  };

  /** Send an acknowledgement */
  trans send_ack
  in {
    place recv: false; place e: e; place ackarray: r;
  }
  { seq_t seq = |e; }
  : trans send_ack
  out {
    place recv: true; place e: e; place ackarray: r;
  };
};

/** message channel */
subnet msg_ch
{
  /** protocol data unit */
  typedef struct { seq_t seq; payload_t data; } pdu_t;
  /** message channel */
  place msg_ch (1) pdu_t[queue w]: {};

  /** transmit message */
  trans send:trans send_msg
  in { place msg_ch: ch; }
  out { place msg_ch: ch + is pdu_t { seq, data }; }
  gate %ch != 0;
  /** receive message */
  trans recv:trans recv_msg
  in { place msg_ch: ch; }
  { seq_t seq = (*ch).seq; payload_t data = (*ch).data; }
#ifdef DUPLICATING
  out { place msg_ch: bool dup! ? ch : -ch; }
#else // DUPLICATING
  out { place msg_ch: -ch; }
#endif // DUPLICATING
  gate /ch != 0;
};

/** acknowledgement channel */
subnet ack_ch
{
  /** Contents of the acknowledgement channel */
  place ack_ch (1) seq_t[queue w]: {};

  /** Enqueue a message */
  trans ack_send:trans send_ack
  in { place ack_ch: ch; }
  out { place ack_ch: ch + is seq_t seq; }
  gate %ch != 0;

  /** Dequeue a message */
  trans ack_recv:trans recv_ack
  in { place ack_ch: ch; }
  { seq_t seq = *ch; }
  out { place ack_ch: -ch; }
  gate /ch != 0;
};

deadlock true;