%<pre>

network{msg: TYPE;}: CONTEXT =
BEGIN
  bufferstate: TYPE = {empty, full};
  action: TYPE = {read, write, overwrite, copy};

network: MODULE =
BEGIN
  INPUT  act: action, inms: msg
  OUTPUT nstate: bufferstate, buffer: msg
INITIALIZATION
  nstate = empty;
TRANSITION
[   
 act' = write AND nstate = empty -->
  buffer' = inms';
  nstate' = full;
[]
 act' = overwrite AND nstate = full -->
  buffer' = inms';
[]
 act' = read AND nstate = full -->
  nstate' = empty;
[]
 act' = copy AND nstate = full -->
  nstate' = nstate;   
[]
 ELSE -->
]
END;

END