Hello,
the previous specification already ensured the required safety properties, as well as liveness for readers. The remaining issue was that readers could arrive in rapid succession, thereby locking our writers. If we want to make sure this cannot happen, a waiting writer must be able to block new readers from being served.
Your solution does this by imposing a FIFO treatment of all requests. This serializes all (read and write) requests at the waiting queue, and that's why you don't observe any difference between weak or strong fairness: there is only one request that can possibly be served, and once it is enabled, it remains enabled until it is served.
Attached is a different, more relaxed solution where requests may be served in different orders. I obtained it from the previous spec by adding a "waiting room" that can hold at most one writer that arrives when there are active readers. As soon as the waiting room is non-empty, new readers are blocked. You can play with different combinations of WF and SF, and TLC will show you different counter-examples.
Which specification you prefer depends on the system you are aiming at.
I suggest we leave it at that: a mailing list is not the right place for a conversation between two persons.
Stephan