const NM = 4
range M = 0..NM // messages with values up to 4
set S = {[M],[M][M]} // queue of up to three messages
PORT // empty state, only send permitted
= (send[x:M] -> PORT[x]),
PORT[h:M] // one message queued to port
= ( send[x:M] -> PORT[x][h]
| receive[h] -> PORT),
PORT[t:S][h:M] //two or more messages queued to port
= ( send[x:M] -> PORT[x][t][h]
| receive[h] -> PORT[t]).
Design a message passing system with a producer and a consumer. The
producer may only send up to N messages before it is blocked
by waiting for the consumer to receive a message. Verify using the
LTSA tool that the system prevents queue overflow (for N=3).
Hint: you can use an `empty' message to get the desired protocol: the consumer sends `empty' messages asynchronously to the producer; it can send at most N of these before going into a state where it must receive the `main' message from the producer before sending another empty messages. A port for (empty) acknowledge messages may be simply modelled as:
const N = 3
PORT_E = PORT_E[0],
PORT_E[i:0..N]
= ( when (i < N) send -> PORT_E[i+1]
| when (i > 0) receive -> PORT_E[i-1] ).
Hint: `inline' the block(), signal() and clearReady() calls in Channel.java, using the code path for inchoice == null. Compile and run applet from the book_applets sub-directory:
entry put, get;
int count = 0;
while (true)
select
when (count < size) and v = accept(put) =>
++count; // insert item v into buffer
reply(put, ' ');
or
when (count > 0) and accept(get) ->
--count; // get item v from buffer
reply(get, v);
end
Hint: see
EntryDemo.java for an example of the use of the Entry
class; see
MsgCarPark.run() for an example of the server using the Select
class. You can get the code for the bounded buffer state manipulation
from
BufferImpl.java; the appropriate instantiation for the template class
E will Character, i.e. you will be using
Entry<Character,Character>.