Re: [tlaplus] Re: add fairness properties to a specification with PlusCal INSTANCEs

Stephan

On 23 Feb 2019, at 03:36, david streader <davidistreader@xxxxxxxxx> wrote:

Thanks Stephan
In your original AlternatingBit algorithm you placed the error behaviour in a separate process. As I can see how to define fair behaviour between processes I assumed that this was why you place the error behaviour there. In you latest version both the error and correct behaviour or data transmission is in the same process - which is what I wanted. I can see that I had not appreciated the significants of the data variables in the definition of fairness.
The reason why I labeled each branch was to differentiate data transmission from dropping data. But you are able to differentiate these branches by restricting the data variables over which fairness is defined. Something alas I had overlooked completely.

Many thanks I finally understand and will apply this technique to my specification.

kind regards david

p.s. I built a model for your spec and instantiated Data as a singleton set {1}. TLC built 6 * 10^7 distinct states in 20 mins and was still growing so I am going to have to wait till I get into the office before I can try on a larger machine.
Is Data <- {1} the best I can use or is there a better way to instantiate Data ?

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.