Faulty channels 7 ? Safety vlastnosti
FC môze len odobrat (head) z cs
stable cs je suffix cs0
- všeobecne kvantifikované, cs0 je konštantná postupnost
FC môze pridat na koniec cr
FC môze stratit správu z cs alebo duplikovat správu do cr
invariant (cs ? cs) loss cr
- cs: celá „história“ cs
- cs ? cs: prefix cs bez cs
- u loss v: v je mozný výstup z chybného kanála, za predpokladu, ze vstup je u
- (null loss null)
- (u loss v) ? (u;m loss v) strata
- (u;m loss v) ? (u;m loss v;m) duplikácia