Faulty channels 8 ? Progress vlastnosti

[ak správa m (a ziadna iná) je nekonecne vela krát pridaná do cs, tak sa m raz (eventually) objaví v cr]

• Predpokladáme mnozinu predikátov p.m (pre kazdé m predikát existuje)

  • ak p.m platí, ziadne iná správa ako m nemôze byt pridaná do cs
  • p.m platí nanajvýš pre jedno m (pocas „výpoctu“)
  • ak p.m je true, tak raz (eventually) bude false alebo m je pridané do cs (t.j. zvýši sa dlzka cs)

• za týchto predpokladov FC zarucí, ze ak raz p.m je true, potom sa raz (eventually) bude rovnat false alebo m sa objaví v cr

• Predpoklad: p.m ? p.n ? m = n

p.m ? cs = null unless ?p.m ? cs = ??m??

p.m ? (cs = cs0) ? (cs ? null) unless

?p.m ? cs = tail(cs0) ? cs = cs0;m

p.m ? |cs| = k ? ?p.m ? |cs| > k

• Záver: p.m ? ?p.m ? m ? cr

Previous slide

Next slide

Back to first slide

View graphic version