Add small improvements to the Disruptor spec.

[nicholassm]

• 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.)

[nicholassm]

Alright, added the same improvements to the Multi Producer Multi Consumer specification. Thanks.

[nicholassm]

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?

[lemmy]

The definition of a formula has to come before its use. In other words, the parser won't accept it.

[nicholassm]

Makes sense.

Is there anything else you can see that I can do to improve this PR? It's mostly related to (excellent) suggestions from @muenchnerkindl.

Kind regards, Nicholas

[nicholassm]

Hi guys,

Is there anything else I should do to increase the quality further? Otherwise, I think it's ready for merging. :-) Many thanks in advance.

Kind regards Nicholas