Global snapshots
Úloha: modifikovat daný program tak, aby sme mohli zaznamenat stav jeho výpoctu
toto je problémom pri asynchrónnych a distribuovaných systémoch
Program EG
declare x, y, z: integer
initially x, y, z = 0, 0, 0
assign x := z + 1 ? y := x ? z := y
stavom EG je trojica hodnôt x, y, z
lahko vidno, ze jediná mozná postupnost stavov EG je
(0, 0, 0) ? (1, 0, 0) ? (1, 1, 0) ? (1, 1, 1) ? (2, 1, 1) ? (2, 2, 1) ? …
EG splna invariant
invariant (x ? y) ? (y ? z) ? (z + 1 ? x)
ak hodnotu x zaznamenáme v stave (0, 0, 0) a hodnoty y a z v stave (1, 1, 0), tak zaznamenaný stav (0, 1, 0) nie je stavom ziadneho výpoctu