Module System

local buffer_size : int where buffer_size = 5
local next_free_element : int where next_free_element = 0
local next_occupied_element : int where next_occupied_element = 0


Module PRODUCER :


Transition PRODUCER_WAIT NoFairness:
enable (((next_free_element+1) mod buffer_size)=next_occupied_element)
assign next_free_element := next_free_element,next_occupied_element := next_occupied_element

Transition PRODUCE NoFairness:
enable (((next_free_element+1) mod buffer_size)!=next_occupied_element)
assign next_free_element := (next_free_element+1) mod buffer_size
EndModule


Module CONSUMER :


Transition CONSUMER_WAIT NoFairness:
enable (next_free_element=next_occupied_element)
assign next_free_element := next_free_element,next_occupied_element := next_occupied_element

Transition CONSUME NoFairness:
enable (next_free_element!=next_occupied_element)
assign next_occupied_element := (next_occupied_element+1) mod buffer_size
EndModule


Module SYSTEM :

include PRODUCER : ( PRODUCER )
 || CONSUMER : ( CONSUMER )
EndModule