// ------------------------------------------------------------
// This is a simple EntryProtocol that simply waits until lock is
// false and then sets lock, so that other processes can not
// leave their EntryProtocols. By interleaving, only one process can
// do this since setting the lock is done at the same time when
// testing the lock shows that it is false.
// ------------------------------------------------------------

package Communication.MutexProtocols.SpinLock;

module EntryProtocol(bool !spin, lock) {
   next(spin) = true;
   await(!lock);
   next(lock) = true;
   next(spin) = false;
}