This program is a double buffer model.
The buffer size is n.
The producer waits till the buffer size is less than n before adding 
an element to the buffer.
The consumer waits till the buffer size is greater than 0 before removing
an element from the buffer.

In the Core program:
---------------------
 
there are two asynchronic modules:

PRODUCER and CONSUMER.

There are three global variables:

buffer_size - the size of the buffer.
next_free_element - the index of the next free element in the buffer.
next_occupied_element - the index of the next occupied element in the buffer.

The buffer is full when (next_free_element+1) mod n equals next_occupied_element.
The buffer is empty when next_free_element equals next_occupied_element.

At initialization , next_free_element and next_occupied_element are both set to 0.


Translation notes:
--------------------
* The smv default for assigning next value for variables that there is no specific assignment for
  their next value is choosing indeterminally a value from the type range of the variable. Since that 
  the core program the HOLD_PREVIOUS flag was on, the assignment next(buffer_size) := buffer_size  had
  to be written specifically in the smv program.