Module System

local buffer_filled : bool where buffer_filled = false
local buffer_empty : bool where buffer_empty = true


Module PRODUCER :
local ready_to_produce : bool where ready_to_produce = true
local ready_to_deliver : bool where ready_to_deliver = false


Transition PRODUCE NoFairness:
enable ready_to_produce=true
assign ready_to_produce := false,ready_to_deliver := true

Transition DELIVER NoFairness:
enable ((ready_to_deliver=true)/\(buffer_empty=true))
assign ready_to_deliver := false,buffer_empty := false,ready_to_produce := true,buffer_filled := true
EndModule


Module CONSUMER :
local ready_to_remove : bool where ready_to_remove = true
local ready_to_consume : bool where ready_to_consume = false


Transition CONSUME NoFairness:
enable ready_to_consume=true
assign ready_to_consume := false,ready_to_remove := true

Transition REMOVE NoFairness:
enable ((buffer_filled=true)/\(ready_to_remove=true))
assign buffer_filled := false,ready_to_remove := false,buffer_empty := true,ready_to_consume := true
EndModule


Module SYSTEM :

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