HW 1 CLARIFICATIONS

---------------------------------------------
Problem 1: 

Here is a skeleton of the desired service program.
Give the three things indicated below in UPPER CASE.

 service-program FifoManyToOne(N, Msg) {
   MsgSeq[1..N] txh := empty sequence; 
   MsgSeq rxh := empty sequence; 

   Tx(i,m)
     ec true
     ac append(txh[i],m)

   Rx(m)
     ec [STATE PREDICATE]
     ac append(txh[i],m)

   [STATE PROGRESS CONDITION (i.e., leadsto assertions)]
 }


---------------------------------------------
Problem 2: 

In the sliding window system using lossy channels, you already have 
a set of predicates Y1,Y2,...,Yn that are intended to be invariant. 
Let Yn be the predicate stating the desired lower bound on data j in transit. 
We want an assertional proof that Y1,...,Yn are invariant. 
There are two obstacles to overcome. 

------------------------------------------------------------
OBSTACLE 1

Y1,...,Yn almost satisfies the invariance rule, i.e. 
 - {true}init{Y1,...,Yn} holds.
 - {Y1,...,Yn}e{Yi} holds for every event e and every Yi except for 
   the case of event Rec(data nr) and the predicate Yn. 

To complete the assertional proof, we need a predicate Z such that 
Y1,...,Yn,Z satisfies the invariance rule, i.e., 
 - {true}init{Y1,...,Yn,Z} holds.
 - {Y1,...,Yn,Z}e{Yi} holds for every event e and Yi
 - {Y1,...,Yn,Z}e{Z} holds for every event e 

Given what already holds, it suffices to establish the following: 
 1. {true}init{Z} holds.
 2. {Y1,...,Yn,Z}e{Yn} holds for every event e. 
 3. {Y1,...,Yn,Z}e{Z} holds for every event e. 
 
So you just need to supply a predicate Z that satisfies the above
conditions 1,2,3. 

------------------------------------------------------------
OBSTACLE 2

Yn has the term "data j in transit from x to y".
Not surprisingly, Z also will state conditions on what is in transit. 
BUT, "in transit" is not defined. 
All we is Lxy.txh and Lxy.rxh.

If Lxy were a fifo channel, then the sequence of messages in transit 
can be defined as the unique sequence, say "tr", such that 
      Lxy.txh = Lxy.rxh o tr

But Lxy is a lossy channel, and the above won't work. 

So you have to state Z (and restate Yn) so that "in transit" is properly 
defined in terms of Lxy.txh, Lxy.rxh, and any auxiliary variables you need. 
------------------------------------------------------------

SUPPLY: 
 - Define any auxiliary variables you need. 
 - Restate Yn in terms of Lxy.txh, Lxy.rxh, and the auxiliary variables. 
 - State Z in terms of Lxy.txh, Lxy.rxh, and the auxiliary variables, 
   such that it satisfies the above conditions 1,2,3. 
   You do not need to show that these conditions hold. 

---------------------------------------------