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