Add small improvements to the Disruptor spec. #151
Conversation
nicholassm
commented
Sep 22, 2024
nicholassm
commented
- Add comment on 'Multicast' behaviour.
- Add ASSUME for MaxPublished constant.
- Add comment on the usage of the 'consumed' variable.
- Remove WF from write actions.
- Remove bounding of model happening in BeginWrite action. Use a State constraint instead. Use suggestion for liveliness property.
- (The last two items are not done yet for the MPMC spec - it's less straight forward to do because of the multiple producers behaviour.)
- Add comment on 'Multicast' behaviour. - Add ASSUME for MaxPublished constant. - Add comment on the usage of the 'consumed' variable. - Remove WF from write actions. - Remove bounding of model happening in BeginWrite action. Use a State constraint instead. Use suggestion for liveliness property. - (The last two items are not done yet for the MPMC spec - it's less straight forward to do because of the multiple producers behaviour.) Signed-off-by: Nicholas Schultz-Møller <[email protected]>
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
Signed-off-by: Nicholas Schultz-Møller <[email protected]>
- Flip 'Advance' and 'Access' states - they were flipped. - Remove model boundary from 'BeginWrite' action - separates spec and verification. - Fix 'published' variable which had an unused mapping. Signed-off-by: Nicholas Schultz-Møller <[email protected]>
|
Alright, added the same improvements to the Multi Producer Multi Consumer specification. |
|
I'm considering moving the "spec" section (Init, Next and Liveliness) to the top (i.e. below constants and variables) to make it easier to understand the models for users. Kind of like an article where you read the highlights in the subheading. What is generally recommended? |
|
The definition of a formula has to come before its use. In other words, the parser won't accept it. |
|
Makes sense. Is there anything else you can see that I can do to improve this PR? Kind regards, |
|
Hi guys, Is there anything else I should do to increase the quality further? Otherwise, I think it's ready for merging. :-) Kind regards |
