Global snapshots 2
Podrobnejšia špecifikácia:
pre zjednodušenie budeme predpokladat, ze stav sa zaznamenáva len raz (lahko sa to rozšíri pre viacnásobné pouzitie)
transformujeme daný program tak, ze potom tento zaznamená stav pôvodného programu
zaznamenaný stav ? stav, ktorý sa môze vyskytnút vo výpocte, a to medzi tým, ked je zaznamenávanie (záznam) inicializované a ukoncené
zaznamenávanie je inicializované, ak premennej begun je priradená hodnota true
nezaoberáme sa tým, kedy sa begun stane true
predpokladáme, ze ak begun sa stane true, ak v konecnom case sa ukoncí zaznamenávanie
pod stavom myslíme stav (t.j. hodnoty premenných) pôvodného programu
[s0] v [s1], kde s0, s1 sú stavy a v je konecná postupnost príkazov, znamená: ak zacneme v s0 a vykonáme v, tak skoncíme v s1
init ? stav, pri ktorom je zaznamenávanie inicializované (begun ? true)
rec ? stav zaznamenaný transformovaným programom