[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Hillel Wayne <HWayne@xxxxxxxxx>*Date*: Wed, 6 Feb 2019 22:26:00 -0800 (PST)*References*: <7530440e-0b79-45ee-af76-8a0537a1fd30@googlegroups.com> <5f90e72c-7cee-4b38-a364-cad98fd77e93@googlegroups.com>

This is actually one of my case examples of the limits of PlusCal. What's going on is that one of two things can happen at oneMore: either we go to upx (pc' = "upx") or we go to upy (pc' = "upy"). By making oneMore fair, we are saying, very roughly, that it will eventually make progress, aka it will always do one of those two things. But we are *not* saying which one it will do! There's no restriction that we won't just go from oneMore to upx *every single time* we take the oneMore action. And, in fact, it's impossible to express this in just PlusCal, at least not without some janky process jury rigging.

On the other hand, if we write the same thing in TLA+ we could add in SF_x(oneMore /\ pc' = "upx") and then guarantee that we'd go from oneMore to upx infinitely often. We have to use strong fairness here because the action isn't always enabled.

H

On Wednesday, 6 February 2019 15:21:22 UTC-6, david streader wrote:

Thanks Ronso fairness (if offered infinitely often must eventually be taken) in TLA+ is only between differently named steps and, as I said, it is the fact that the State Graph has both looping and exiting steps with the same name that means that never taking the infinitely offered exit is deemed fair. Remember it is a design decision how to check fairness. As the state graph is build from the TLA+ fairness could be checked in the way I thought it would have been.Thats good to know that I need better use of labels but I have added labels on every line I am allowed to and still can not get termination with the current definition of fairness.begin Count:

while (x<Size) do

oneMore:+

either

upx:+

x := x + 1;

or

upy:+

y := (y + 1)%Size;

end either;

I know that the tool tells me that even restricting ourselves to fair behavior it is possible for this algorithm to never terminate. But this is not fair behavior as I understand it to be unless I conclude that the Calplus either.. or .. construct is inherently unfair? I interpret fairness to require that upx:+ must be taken more that Size times in any fair execution.

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.

**References**:**How does Fairness relate to the State Graph***From:*david streader

**Re: How does Fairness relate to the State Graph***From:*david streader

- Prev by Date:
**[tlaplus] Re: Generating a set of structs where each key ranges over a distinct set** - Next by Date:
**Re: [tlaplus] Re: Generating a set of structs where each key ranges over a distinct set** - Previous by thread:
**Re: How does Fairness relate to the State Graph** - Next by thread:
**Re: [tlaplus] How does Fairness relate to the State Graph** - Index(es):