Readers?Writers Problem 2
ak 0 ? nr ? N ? 0 ? nw ? N, tak
[nw ? 1 ? (nr = 0 ? nw = 0)] ? [(nr + N?nw) ? N]
máme nový invariant t ? 0 (3)
modifikovaný program user:
declare t: int
always t = N ? (nr + N?nw)
assign
nr := nr + 1 if t ? 1 {started read}
nr := nr ? 1 {end read}
nw := nw + 1 if t ? N {started write}
nw := nw ? 1 {end write}
Toto riešenie nezarucuje „progress“ ani pre cítajúcich ani pre zapisujúcich. Nemáme poziadavku, ze cítanie alebo zápis niekedy raz skoncí, a teda nemôzeme tvrdit, ze iné cítanie alebo zápis zacnú.
nr a nw nám neumoznujú formulovat tvrdenia o jednotlivých cítaniach a zápisoch
Predpokladajme, ze všetky cítania skoncia v konecnom case. Modifikujeme riešenie tak, ze potom raz urcite (eventually) dôjde aj na zápis.
predpokladajme teda
nr = k ? k > 0 ? nr ? k (4)