Faulty channels 3

• zjemníme progress podmienku:

kr = n ? ks = n + 1 ? kr = n + 1

• to sa zabezpecí príkazom

ks := kr + 1 ? kr := ks

• pritom však toto nesplna podmienky (sRW) a (rRW)

• opät zjemníme progress podmienku:

kr = n ? y = n ? ks = n + 1 ? y = n + 1 ? kr = n + 1

• Program P1

  declare x, y, ks, kr: integer
  
  initially x, y, ks, kr = 1, 0, 1, 0
  assign
  y := kr {receiver}
  ? ks := y + 1 {sender}
  ? x := ks {sender}
  ? kr := x {receiver}

end{P1}

• x je chybový kanál, cez ktorý sa posiela ks

• y je chybový kanál, cez ktorý sa posiela potvrdenie

• invariant y ? kr ? x ? ks ? y + 1 (I1)

• Dôkaz:

  • na zaciatku (I1) platí
  • kazdé priradenie a := b splna a ? b,
    a teda vykonanie a := b zachová a ? b

Previous slide

Next slide

Back to first slide

View graphic version