public class BufferInt
This is used to create a buffered integer channel that never loses data.
The getState method returns EMPTY, NONEMPTYFULL or FULL according to the state of the buffer.
Constructor and description |
---|
BufferInt
(int size) Construct a new BufferInt with the specified size. |
Type | Name and description |
---|---|
Object |
clone() Returns a new (and EMPTY) BufferInt with the same creation parameters as this one. |
void |
endGet() Removes the oldest integer from the buffer. |
int |
get() Returns the oldest int from the BufferInt and removes it. |
int |
getState() Returns the current state of the BufferInt. |
void |
put(int value) Puts a new int into the BufferInt. |
void |
removeAll() |
int |
startGet() Returns the oldest integer from the buffer but does not remove it. |
Construct a new BufferInt with the specified size.
size
- the number of ints the BufferInt can store.Returns a new (and EMPTY) BufferInt with the same creation parameters as this one.
Note: Only the size and structure of the BufferInt is cloned, not any stored data.
Removes the oldest integer from the buffer.
Returns the oldest int from the BufferInt and removes it.
Pre-condition: getState must not currently return EMPTY.
Returns the current state of the BufferInt.
Puts a new int into the BufferInt.
Pre-condition: getState must not currently return FULL.
value
- the int to put into the BufferIntReturns the oldest integer from the buffer but does not remove it. Pre-condition: getState must not currently return EMPTY.
JCSP for Java 1.8 generated 14-10-2016 by Jon Kerridge, Edinburgh Napier University - j dot kerridge at napier dot ac dot uk