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 it? Thanks! Brian |