Co-locate steps to remove a process from waiting queue in ReadersWriters example

[wrobell]

The steps to remove a process from the waiting queue are

• get the head of the queue
• remove the head by keeping the tail of the queue

These two steps are spread across Read, Write, and ReadOrWrite operators. This makes the specification harder to understand.

Improve the readability of the specification by keeping all the steps within ReadOrWrite operator.

[wrobell]

BTW. Maybe renaming of the operators would be a good idea as well, i.e.

• TryRead -> EnqueueForRead
• TryWrite -> EnqueueForWrite
• ReadOrWrite -> DequeueProcess

[lemmy]

Naming is hard.