module QUEUE (TYPES, CHANNELS, FUNCTIONS) is

process Queue [G: Operation] (in var val: Nat) is
   -- process modeling a shared queue offering the operations fetch_and_store,
   -- compare_and_swap, and read_and_increment; "val" is the initial value
   var new_val: Nat in
      loop
         alt
            G (Read, val, ?any Pid)
         []
            G (Write, ?val, ?any Pid)
         []
            G (Fetch_and_Store, val, ?val, ?any Pid)
            -- 2nd parameter: current value
            -- 3rd parameter: new value
            -- 4th parameter: id of the process performing the operation
         []
            G (Compare_and_Swap, val, ?val, true, ?any Pid)
            -- 2nd parameter: old value
            -- 3rd parameter: new value
            -- 4th parameter: true iff (old value == current value)
            -- 5th parameter: id of the process performing the operation
         []
            G (Compare_and_Swap, ?new_val, ?any Nat, false, ?any Pid)
            where (val != new_val)
            -- 2nd-5th parameters: same as above
         []
            G (Read_and_Increment, val of Pid, ?any Pid);
            -- 2nd parameter: current value
            -- 3rd parameter: id of the process performing the operation
            val := (val + 1) mod N
         end alt
      end loop
   end var
end process

end module