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. ---------------------------------------------