Description:
The Write First property states that a reader should never read before some writer has written. Stated another way, a reader should not read from an empty document.
As far as the central data server is concerned, all readers behave in a symmetrical manner. This means that checking this property for a single reader is sufficient. If the property is not possible for the chosen reader, it is not possible for any of them. This property is specified in terms of reader 1. This allows the same property specification to be used when the problem is scaled.
This property should be invalid when analyzed by any of the finite state verification tools. This is due to the fact that the shared data is not being modeled.
Specification:
Back to Readers/Writers
Back to main