/* Alternating bit protocol 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), August 25, 2003.
 */

/** 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 */
trans :produce { payload_t data; };
trans :consume { payload_t data; };
trans :send_msg { bool bit; payload_t data; };
trans :recv_msg { bool bit; payload_t data; };
trans :send_ack { bool bit; };
trans :recv_ack { bool bit; };

/** 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;
};

/** sender process */
subnet sender
{
  /** the bit of the sender process */
  place sender (1) bool: false;
  /** data to be sent */
  place data (0..1) payload_t;
  /** no data? */
  place nodata (1) bool: place data equals empty;

  /** enqueue a data packet */
  trans enqueue:trans produce
  in { place nodata: true; }
  out { place data: data; place nodata: false; };

  /** send a message */
  trans "!message":trans send_msg
  in { place sender: bit; place data: data; }
  out { place sender: bit; place data: data; };

  /** receive acknowledgement and dequeue data packet if appropriate */
  trans "?acknowledgement":trans recv_ack
  in {
    place sender: b;
    place nodata: nd; place data: (!nd)#data;
  }
  out {
    place sender: !bit;
    place nodata: nd || b == bit; place data: (!(nd || b == bit))#data;
  };
};

/** receiver process */
subnet receiver
{
  /** the bit of the receiver process */
  place receiver (1) bool: false;

  /** received data */
  place recv (0..1) payload_t;
  /** no received data? */
  place norecv (1) bool: place recv equals empty;
  /** pending acknowledgement */
  place pending (0..1) bool;
  /** no pending acknowledgement? */
  place nopending (1) bool: place pending equals empty;

  /** dequeue the received data if no acknowledgement is pending */
  trans dequeue:trans consume
  in { place nopending: true; place norecv: false; place recv: data; }
  out { place nopending: true; place norecv: true; };

  /** receive data if no acknowledgement is pending */
  trans recv:trans recv_msg
  in {
    place nopending: true; place receiver: receiver;
    place norecv: true;
  }
  out {
    place nopending: false; place pending: bit; place receiver: !bit;
    place norecv: bit != receiver; place recv: (bit == receiver)#data;
  };
  /** acknowledge data */
  trans ack:trans send_ack
  in { place nopending: false; place pending: bit; }
  out { place nopending: true; };
};

/** message channel */
subnet msg_ch
{
  /** message channel */
  place msg (0..1) struct { bool bit; payload_t data; };
  /** message channel empty? */
  place nomsg (1) bool: place msg equals empty;

  /** transmit message */
  trans send:trans send_msg
  in { place nomsg: true; }
  out { place nomsg: false; place msg: { bit, data }; };
  /** receive message */
  trans recv:trans recv_msg
  in { place nomsg: false; place msg: { bit, data }; }
#ifdef DUPLICATING
  out { place nomsg: bool nodup!; place msg: (!nodup)#{ bit, data }; };
#else // DUPLICATING
  out { place nomsg: true; };
#endif // DUPLICATING
};

/** acknowledgement channel */
subnet ack_ch
{
  /** acknowledgement channel */
  place ack (0..1) bool;
  /** acknowledgement channel empty? */
  place noack (1) bool: place ack equals empty;

  /** transmit acknowledgement */
  trans send:trans send_ack
  in { place noack: true; }
  out { place noack: false; place ack: bit; };

  /** receive acknowledgement */
  trans recv:trans recv_ack
  in { place noack: false; place ack: bit; }
  out { place noack: true; };
};

deadlock true;