simulating a crash in PlusCal

[Michal Jaszczyk]

I'm writing a spec about a file system in PlusCal:

* my global variables represent various data structures, both in memory and on disk

* my processes represent various components of the system, internal threads, user threads etc.

In order to simulate a crash, I'd like to do the following:

* clear all data structures according to how the crash affects them (e.g. in-memory caches are emptied, but on-disk state remains)

* re-initialize affected data structures according to how the recovery procedure works

* reset affected processes to the beginning

Specifically I have a question about that last point:

1) Is it sufficient to simply reset the 'pc' variable to the first label of a process?

2) What about procedure call stacks? (I don't have procedures currently, but I might)

3) What about process local variables? (Currently they are always initialized before being used, so I don't rely on their initial values in the initial state).

Thanks,

M.