Module System



Module BUFFER :
local ready_to_produce : bool where ready_to_produce = true
local ready_to_deliver : bool where ready_to_deliver = false
local a_buffer_cell_empty : bool where a_buffer_cell_empty = true
local a_buffer_cell_filled : bool where a_buffer_cell_filled = false
local b_buffer_cell_empty : bool where b_buffer_cell_empty = true
local b_buffer_cell_filled : bool where b_buffer_cell_filled = false
local ready_to_remove : bool where ready_to_remove = true
local ready_to_consume : bool where ready_to_consume = false


Transition PRODUCE NoFairness:
enable (ready_to_produce/\(!ready_to_deliver))
assign ready_to_produce := false,ready_to_deliver := true

Transition DELIVER_TO_FIRST_BUFFER NoFairness:
enable (ready_to_deliver/\a_buffer_cell_empty/\(!ready_to_produce)/\(!a_buffer_cell_filled))
assign ready_to_deliver := false,a_buffer_cell_empty := false,ready_to_produce := true,a_buffer_cell_filled := true

Transition DELIVER_TO_SECOND_BUFFER NoFairness:
enable (ready_to_deliver/\b_buffer_cell_empty/\(!ready_to_produce)/\(!b_buffer_cell_filled))
assign ready_to_deliver := false,b_buffer_cell_empty := false,ready_to_produce := true,b_buffer_cell_filled := true

Transition REMOVE_FROM_FIRST_BUFFER NoFairness:
enable (a_buffer_cell_filled/\ready_to_remove/\(!ready_to_consume)/\(!a_buffer_cell_empty))
assign a_buffer_cell_filled := false,ready_to_remove := false,a_buffer_cell_empty := true,ready_to_consume := true

Transition REMOVE_FROM_SECOND_BUFFER NoFairness:
enable (b_buffer_cell_filled/\ready_to_remove/\(!ready_to_consume)/\(!b_buffer_cell_empty))
assign b_buffer_cell_filled := false,ready_to_remove := false,b_buffer_cell_empty := true,ready_to_consume := true

Transition CONSUME NoFairness:
enable (ready_to_consume/\(!ready_to_remove))
assign ready_to_consume := false,ready_to_remove := true
EndModule


Module SYSTEM :

include BUFFER : ( BUFFER )
EndModule