bool Fail = false;
int num_of_messages = 3;
int num_of_recv_messages = 0;
bool message_exists = false;
bool ack_exists = false;
bool message_bit;
bool ack_bit;
bool send_bit = false;
bool recv_bit = false;
bool send_new_message = true;





proctype SENDER() {
do
  ::atomic{
    ((num_of_messages!=0)&&(send_new_message)) ->
    num_of_messages = num_of_messages-1;
    message_exists = true;
    message_bit = send_bit;
    send_new_message = false;
    };
  ::atomic{
    (!send_new_message) ->
    message_bit = send_bit;
    message_exists = true;
    };
  ::atomic{
    (ack_exists&&(ack_bit==send_bit)) ->
    send_bit = !send_bit;
    ack_exists = false;
    send_new_message = true;
    };
  ::atomic{
    (ack_exists&&(ack_bit!=send_bit)) ->
    ack_exists = false;
    };
  ::atomic{
    true ->
    num_of_messages = num_of_messages;
    };
od;
}

proctype RECEIVER() {
do
  ::atomic{
    (message_exists&&(message_bit==recv_bit)) ->
    message_exists = false;
    recv_bit = !recv_bit;
    ack_exists = true;
    ack_bit = message_bit;
    num_of_recv_messages = num_of_recv_messages+1;
    };
  ::atomic{
    (message_exists&&(message_bit!=recv_bit)) ->
    message_exists = false;
    ack_exists = true;
    ack_bit = message_bit;
    };
  ::atomic{
    true ->
    num_of_recv_messages = num_of_recv_messages;
    };
od;
}

init {
    if
      ::message_bit = true;
      ::message_bit = false;
    fi;


    if
      ::ack_bit = true;
      ::ack_bit = false;
    fi;


 atomic{
 run SENDER();
 run RECEIVER();
 };
}