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

Hello David,

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.

In fact this is the crux of my confusion. I can find no way to do this.

I understand that my sentence was perhaps a bit mysterious, so just to make it concrete here is what I had in mind: a variant of the ABP specification that I posted earlier, with the two channels made explicit processes. As before, the (strong) fairness conditions enforce that the channels eventually transmit data and acknowledgements.

I believe your objection is that the fairness conditions are not of the form SF_vars(...) but of the form SF_ch(...) where ch is the variable that represents the data channel [1], and that such fairness conditions cannot be written in PlusCal using fairness on processes or individual labels. So now we are back to the earlier thread [2] on expressing fair choice in PlusCal. I believe that the discussion in that thread argued quite convincingly that the translation of such a construct would not be straightforward, and would (at least) introduce additional labeling rules. (In your proposed "hack", you assume that each branch is labeled.) I agree with the arguments provided in the earlier thread to the effect that it is preferable to identify the intended fairness condition using TLA+ than PlusCal in these cases.

Best regards,

Stephan

[1] Alternatively, one could write SF_vars(dtCh /\ sndC' = Append(sndC, sndOut)).

[2] https://groups.google.com/forum/#!topic/tlaplus/FqGPF_2-ljE

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

Attachment: AlternatingBit.tla
Description: Binary data

Attachment: Transmission.tla
Description: Binary data

On 20 Feb 2019, at 23:02, david streader <davidistreader@xxxxxxxxx> wrote:

Thanks the reference explains much of my confusion.
In process algebras, PA, process are in the eye of the beholder in as much as you can compute the observational equivalence of a set of communication processes with a single process. For finite state processes this can be done mechanically. None the less individual problems have explicitly or implicitly distinct processes for example the ABP has two processes the Sender and the Receiver which if all four were thought of as a single process there would be little need to use any communication channels.

So my intention was only to have four processes that I actually thought to be implicit in the question, the Sender, Receiver and the two communication Channels. I split each of these four into two processes not because I wanted to to but because I could not find a way of doing what you say can be done:

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.

In fact this is the crux of my confusion. I can find no way to do this.
At the moment this seems impossible give the how the either.. or .. command and the if .. then command work with component steps.

I need to be very careful here as non-determinism and fairness are defined very subtly differently in TLA+ and PA. I am not trying to say one is wrong and one right. The State Graph for fairSimple has a branch between two steps with the same name "myStart" in PA this would be called internal (or non-deterministic) choice whereas the State Graph for fairHacked has a branch between steps with different names "myLoop" and "myEnd" in PA this would be called external (or deterministic) choice. I believe that in TLA+ both are non-deterministic but have different fairness properties. So simply to distinguish them I will call them unfair choice and fair choice.

In PA we are forced to define fairness on processes we cannot define fairness on single actions (events) because we wish to analyse processes by hiding internal events and this can change which action exits a loop. In this sence TLA+ is certainly more expressive that PA.

I have attached a process simpleFair.tla with fair behaviour that loops forever and ignores the either branch that exits the loop. This is correct behaviour as the loop only appears to offer the myEnd step infinitely often whereas actually even in a fair execution myEnd need never be offered in the loop as can be seen from the State Graph.

I do not claim to have a detailed understanding of TLA+ or its internal working but have come up with a very tentative
alternative translation of either .. or.. that prevents fair behaviour from allowing the myEnd step being forever ignored.
This can be found in fairHacked.tla

I freely accept that I may have completely got the wrong end of the stick and there is a way to encode fair non-determinism in a single process.

kind regards david

--
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.
<fairHacked.tla><fairHacked.tla><fairSimple.tla>