CMU MSE 15-671	Models of Software Systems	Fall 1995
CSP 2
Garlan & Wing	Homework 11	Due:  November 15, 1995
1. Communication: Write a CSP process that represents a two-place buffer that has the behavior that it throws away the oldest piece of buffered data if a new one arrives before the oldest is removed.
2. Non-determinism: Consider the following two processes:
	P = a ¡  P  []  b ¡  P  
	Q = a ¡ Q  À  b ¡ Q  
a. What are the trace sets of each of these processes?
b. Define a process R that distinguishes between the two processes when it is put in parallel with them. That is, R || P has different behavior from R || Q.
3. Reasoning: Simplify the following expression using CSP axioms to eliminate the parallel operator.
	P = (a ® b ® P | b ® P)
	Q = (a ® (b ® Q | c ® Q))
Case A. Assuming that aP = {a,b,c} and aQ = {a,b,c}
Case B. Assuming that aP = {a,b} and aQ = {a,b,c}
4. Induction: Prove that the process VMS = coin ® choc ® VMS satisfies the specification:
	FAIR = (tr ¯ coin) ² (tr ¯ choc + 1)
5.	Wright: (for this problem refer to the paper "Formalizing Architectural Connection" handed out in the lecture)
a.	Using Wright, specify a connector for a client-server interaction that has the following properties:
The client must initialize the server using a "start-session" event.
The server provides two kinds of services, s1 and s2.
Each service request generates a reply: r1 and r2 (respectively).
Optionally, instead of generating a reply, the server can signal an error after a request for a service.
The client may terminate the session using "end-session", after which no more interactions can take place. This should not happen between a request and a reply, however.
b.	Write a port of a client that uses only service s1, and in addition terminates the session whenever an error is encountered. 
c.	Write a port of a server that accepts requests for services s1, s2, and s3.