CSE 128 Spring
2004
Concurrency
Problem 4.8: ReadersWriters won't pass TLC the way it's
written. This is because the length of the pending queue can be any
natural number. So, I've updated ReadersWriters.tla to include a
definition of bounded sequences to be a sequence no longer than the
length of the cardinality of Client.
I've also fixed a typo in ReadPriority.java.