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

as Leslie once observed, processes are in the eye of the beholder [1]. I am not sure I get your remark about using a separate process for dropping packets: aren't you doing the same with your two processes dataChannel and dropChannel? But certainly you could combine the two into a single process that non-deterministically chooses between transmitting and dropping a message. You would then add a (strong) fairness condition on the subaction that corresponds to data transmission.

[1] http://lamport.azurewebsites.net/pubs/pubs.html#lamport-eye-of-beholder, with an explicit reference to process algebra

On 18 Feb 2019, at 22:45, david streader <davidistreader@xxxxxxxxx> wrote:

Thanks for your reply Stephan.
Your AlternatingBit.tla solution is not one I would have thought of and I will need more time to consider how you came to it. The two key ideas I lacked were (1) placing the dropping of packets in a separate process and (2) writing more sophisticated fairness conditions. I mistakenly thought only single steps could be used in fairness conditions - I am still not thinking of everything being a logical statement.

I know there are significant differences between process algebras and TLA+. But, I normally get students to sketch out a state graph of the individual process they want to model - it is then mechanical to translate finite state graphs into process algebra. For teaching purposes I have been trying to follow (find) a similar approach in TLA+. So my first step would be to isolate the required processes, Sender, Receiver and FaultyChannel. Your TLA+ solution although much neater than mine has introduced a separate process for dropping packets. I will try to adopt your more sophisticated fairness conditions while avoiding the use of the separate process for dropping packets. Or do you know is the additional process needed in TLA+ order to specify the fairness conditions?

I am still unsure how to define fairness in my modular version of ABP but will check if I can get a more sophisticated fairness condition to parse where I have failed to get what I thought of as simple conditions to parse.

Again many thanks - I am finally getting a sense of understanding TLA+

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