HOLD_PREVIOUS

 VAR

num_of_messages: integer INITVAL 3;
num_of_recv_messages: integer INITVAL 0;
message_exists: boolean INITVAL false;
ack_exists: boolean INITVAL false;
message_bit: boolean;
ack_bit: boolean;
send_bit: boolean INITVAL false;
recv_bit: boolean INITVAL false;
send_new_message: boolean INITVAL true;

MODULE SENDER(){
	TRANS SEND_NEW_MESSAGE:
		enable: ((num_of_messages != 0)/\(send_new_message));
		assign: num_of_messages' := num_of_messages - 1;
			message_exists' := true;
			message_bit' := send_bit;
			send_new_message' := false;
	TRANS SEND_OLD_MESSAGE:
		enable: (!send_new_message);
		assign: message_bit' := send_bit;
			message_exists' := true;
	TRANS RECV_NEW_ACK:
		enable: (ack_exists /\ (ack_bit = send_bit));
		assign: send_bit' := !send_bit;
			ack_exists' := false;
			send_new_message' := true;
	TRANS RECV_OLD_ACK:
		enable: (ack_exists /\ (ack_bit != send_bit));
		assign: ack_exists' := false;
	TRANS SENDER_DELAY:
		enable: true;
		assign: num_of_messages' := num_of_messages;
}

MODULE RECEIVER(){
	TRANS RECV_NEW_MESSAGE:
		enable: (message_exists /\  (message_bit = recv_bit));
		assign: message_exists' := false;
			recv_bit' := !recv_bit;
			ack_exists' := true;
			ack_bit' := message_bit;
			num_of_recv_messages' := num_of_recv_messages + 1;
	TRANS RECV_OLD_MESSAGE:
		enable: (message_exists /\ (message_bit != recv_bit));
		assign: message_exists' := false;
			ack_exists' := true;
			ack_bit' := message_bit;
	TRANS RECEIVER_DELAY:
		enable: true;
		assign: num_of_recv_messages' := num_of_recv_messages;
}

MODULE SYSTEM(){
	(SENDER() ||| RECEIVER())
}