Module System

local num_of_messages : int where num_of_messages = 3
local num_of_recv_messages : int where num_of_recv_messages = 0
local message_exists : bool where message_exists = false
local ack_exists : bool where ack_exists = false
local message_bit : bool 
local ack_bit : bool 
local send_bit : bool where send_bit = false
local recv_bit : bool where recv_bit = false
local send_new_message : bool where send_new_message = true


Module SENDER :


Transition SEND_NEW_MESSAGE NoFairness:
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

Transition SEND_OLD_MESSAGE NoFairness:
enable (!send_new_message)
assign message_bit := send_bit,message_exists := true

Transition RECV_NEW_ACK NoFairness:
enable (ack_exists/\(ack_bit=send_bit))
assign send_bit := !send_bit,ack_exists := false,send_new_message := true

Transition RECV_OLD_ACK NoFairness:
enable (ack_exists/\(ack_bit!=send_bit))
assign ack_exists := false

Transition SENDER_DELAY NoFairness:
enable true
assign num_of_messages := num_of_messages
EndModule


Module RECEIVER :


Transition RECV_NEW_MESSAGE NoFairness:
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

Transition RECV_OLD_MESSAGE NoFairness:
enable (message_exists/\(message_bit!=recv_bit))
assign message_exists := false,ack_exists := true,ack_bit := message_bit

Transition RECEIVER_DELAY NoFairness:
enable true
assign num_of_recv_messages := num_of_recv_messages
EndModule


Module SYSTEM :

include SENDER : ( SENDER )
 || RECEIVER : ( RECEIVER )
EndModule