[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

modeling resets

I've modeled a reader process and a writer process using PlusCal, and they
communicate via some global state.

I'd like to model a reset event (such as a power failure) in which, regardless
of its current state, each process is reset back to its initial state.
Some global state would be reset as well, but some global state is persistent
and survives the reset.

I was imagining something similar to the LoseMsg process in the ABProtocol
algorithm example, but I'm not sure how to reset the other processes.

Is there an example of something like this, or any ideas on how I might achieve