Closed ThomasArts closed 2 years ago
Fix the model such that operations get_lock and get_token with dead processes do not update the state. Those operations are no-ops, but it takes some time for the system to have the monitor DOWN signal actually make it a no-op.
This does not work, the implementation is non-deterministic and this fix just reveals another issue
Fix the model such that operations get_lock and get_token with dead processes do not update the state. Those operations are no-ops, but it takes some time for the system to have the monitor DOWN signal actually make it a no-op.