const
	MININT	:	-32768;
	MAXINT	:	32767;
var
	PC	:	MININT..MAXINT;
	send_new_message	:	BOOLEAN;
	recv_bit	:	BOOLEAN;
	send_bit	:	BOOLEAN;
	ack_bit	:	BOOLEAN;
	message_bit	:	BOOLEAN;
	ack_exists	:	BOOLEAN;
	message_exists	:	BOOLEAN;
	num_of_recv_messages	:	MININT..MAXINT;
	num_of_messages	:	MININT..MAXINT;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable ack_bit */ 
Ruleset i : BOOLEAN Do
Rule 
PC=0
==>
begin
  ack_bit:=i;
  if PC=0 then
    PC:=1
  end;
end;
end;

/* Ruleset created to simulate non-deterministic initialization for not-initialized variable message_bit */ 
Ruleset i : BOOLEAN Do
Rule 
PC=1
==>
begin
  message_bit:=i;
  if PC=1 then
    PC:=2
  end;
end;
end;

Rule "SENDER_DELAY"
PC=2 & TRUE
==>
begin
  num_of_messages:=num_of_messages;
end;

Rule "RECV_OLD_ACK"
PC=2 & (ack_exists & (ack_bit!=send_bit))
==>
begin
  ack_exists:=FALSE;
end;

Rule "RECV_NEW_ACK"
PC=2 & (ack_exists & (ack_bit=send_bit))
==>
begin
  send_bit:=!send_bit;
  ack_exists:=FALSE;
  send_new_message:=TRUE;
end;

Rule "SEND_OLD_MESSAGE"
PC=2 & (!send_new_message)
==>
begin
  message_bit:=send_bit;
  message_exists:=TRUE;
end;

Rule "SEND_NEW_MESSAGE"
PC=2 & ((num_of_messages!=0) & (send_new_message))
==>
begin
  num_of_messages:=num_of_messages - 1;
  message_exists:=TRUE;
  message_bit:=send_bit;
  send_new_message:=FALSE;
end;

Rule "RECV_NEW_MESSAGE"
PC=2 & (message_exists & (message_bit=recv_bit))
==>
begin
  message_exists:=FALSE;
  recv_bit:=!recv_bit;
  ack_exists:=TRUE;
  ack_bit:=message_bit;
  num_of_recv_messages:=num_of_recv_messages + 1;
end;

Rule "RECV_OLD_MESSAGE"
PC=2 & (message_exists & (message_bit!=recv_bit))
==>
begin
  message_exists:=FALSE;
  ack_exists:=TRUE;
  ack_bit:=message_bit;
end;

Rule "RECEIVER_DELAY"
PC=2 & TRUE
==>
begin
  num_of_recv_messages:=num_of_recv_messages;
end;

startstate
begin
  num_of_messages:=3;
  num_of_recv_messages:=0;
  message_exists:=FALSE;
  ack_exists:=FALSE;
  message_bit:=TRUE;
  ack_bit:=TRUE;
  send_bit:=FALSE;
  recv_bit:=FALSE;
  send_new_message:=TRUE;
  PC:=0;
end;