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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Tue, 6 Jul 2021 12:35:54 -0700 (PDT)*Ironport-hdrordr*: A9a23:ri0UgK9JaAJpxcKQCXJuk+BRI+orL9Y04lQ7vn2ZbSYlI/Bw8PrezMjztCWE2wr5N0tQzOxoVJPwaE80lqQFv7X5Q43SdDUO0VHARPA+nNeSnAEIfReOoNK1vp0QJJRWOZnZAER/5PyKtDVQa+xQkuWvweSVoaP1yndgShwvQ6xs9G5CYWz3fiIZJWk2ZutaZf/sgrsh1lzQAAVuH7/LfAh5LpSz2Ky05eOWEW90dmxXnXj7/ETYns+yYlDolWZVIn4/jcZsgCa10n24l+bT8YD/u1uskB6Uns0mwKq7u4F+OPA=*References*: <932afbd1-f11a-4be3-a69a-ac1289ad7e11n@googlegroups.com> <12016527-CCB4-422F-965E-0D71CA237511@gmail.com> <b5577792-3591-7262-199a-282c22386be4@gmail.com> <743b047f-7830-4805-8dc6-2635f1b29c80n@googlegroups.com> <CAE7Z=+6Km0geBTPARkOSwwPDJB=jfwDUuZMKqe_bByiF1u2dfg@mail.gmail.com>

I feel like the programmer in me understood fairness a lot better when I learned how liveness is modelchecked. TLC tries to find "lasso"-shaped state traces as counterexamples to your desired liveness properties - lasso-shaped as in the trace loops back to some state found earlier in the trace (in the case of stuttering, this is just looping at the final state). Since all liveness properties are of the form <>P, finding a lasso where P is not satisfied suffices as a counterexample. Asserting fairness is a way of disallowing certain lasso counterexamples. If you want to disallow a stuttering counterexample, you use weak fairness. If you want to disallow a non-stuttering lasso counterexample, you use strong fairness. A loose analogy is that assuming weak fairness assumes that the system will eventually do something (as opposed to sitting there doing nothing), and assuming strong fairness assumes the system will eventually make the correct decision at a branch (usually fail or not fail).

I guess this isn't a full account of fairness (it doesn't really account for what it means when fairness itself is the liveness property you want to prove) but it has worked well for all the systems I've specified in TLA+ so far.

Andrew

On Tuesday, July 6, 2021 at 1:31:42 PM UTC-4 hua...@xxxxxxxxx wrote:

My high-school daughter finds it hard to understand why there are the same amount of even numbers as the nature numbers...Also, why "0.99999...." equal to 1. Because: too much...:-)On Tue, Jul 6, 2021 at 10:04 AM Leslie Lamport <tlapl...@xxxxxxxxx> wrote:Fairness is probably the part of TLA+ that most people find hardest tounderstand. This is not a problem with TLA+. Most other formalismsdon't have this problem because they simply can't express the kind offairness that you need. The fundamental reason fairness, and livenessin general, are hard to understand is that they are properties ofinfinite behaviors, and people have trouble understanding theinfinite. For example, their minds are usually blown by "Hilbert'shotel", which is always full but always has room for another guestbecause it has an infinite number of rooms. (You can look it up onthe web.)If you learn PlusCal and enough about TLA+ to understand how toexpress the fairness properties you will need, you should have notrouble learning to write TLA+ specs. You will then have the freedomto use either PlusCal or TLA+, whichever is best for an application.You can also use PlusCal together with TLA+ specifications offairness. You can write a PlusCal algorithm with no fairnessrequirements, which will be translated to a specification named Spec.You can then add, after the translation, the definitionFairSpec == Spec /\ some fairness conditionsand use FairSpec as your specification. (Don't modify the definitionof Spec because your modifications will disappear the next time yourun the translator.) You can also put some fairness conditions in thePlusCal code and put additional fairness conditions that can't beexpressed easily in PlusCal in the definition of FairSpec.Incidentally, you can always express any TLA+ fairness conditions inPlusCal. However, this often requires changing the process structureof the PlusCal code. In your example, that can be done by replacingthe process that executes either branch1 or branch2 with twoprocesses: one that executes branch1 and one that executes branch2.When you understand TLA+, you will understand that processes are notinherent in an algorithm but represent a particular way of writing theTLA+ formula that is the algorithm.

Leslie--On Tuesday, July 6, 2021 at 9:13:48 AM UTC-7 hwa...@xxxxxxxxx wrote:IMO needing to put fairness on a non-deterministic decision is one of the points where you should be considering switching to TLA+ over using PlusCal.

H

On 7/6/2021 1:34 AM, Stephan Merz wrote:

Hello,

requiring strong fairness for the branch1 action won't help because the non-deterministic decision of which branch to enter is taken earlier (at the "either" statement labeled "example"). This is one of the cases where the intended fairness condition has to be expressed in TLA+. You probably want to write something like

/\ SF_vars(example /\ pc' = [pc EXCEPT !["test"] = "branch1"])/\ SF_vars(example /\ pc' = [pc EXCEPT !["test"] = "branch2"])

in order to express that both branches will be taken infinitely often if execution arrives infinitely often at the "either" statement.

Hope this helps,Stephan--

On 1 Jul 2021, at 14:53, p.to...@xxxxxxxxxxxxxxxxx <p.to...@xxxxxxxxxxxxxxxxx> wrote:

Hi all, i don't know how to use the either statement in pluscal with fairness condition on the options of the either or statement. I have tried the following example with a label for each option of the statement but it doesn't seems to work:

begin example:

while TRUE do

either

branch1:

set := {1};

or

branch2:

set := {2};

end either;

later:

skip;

end while;

and the formula prop2 == <>(set={1}) doesn't hold true, the system cycle over all branch2 options. I have tried to add the fairness in the tla translated specification putting an /\ SF_vars(branch1) but the problem persists, here is the tla+ translation from pluscal:

VARIABLES set, pc

(* define statement *)

prop2 == <>(set={1})

vars == << set, pc >>

ProcSet == {"test"}

Init == (* Global variables *)

/\ set = {}

/\ pc = [self \in ProcSet |-> "example"]

example == /\ pc["test"] = "example"

/\ \/ /\ pc' = [pc EXCEPT !["test"] = "branch1"]

\/ /\ pc' = [pc EXCEPT !["test"] = "branch2"]

/\ set' = set

later == /\ pc["test"] = "later"

/\ TRUE

/\ pc' = [pc EXCEPT !["test"] = "example"]

/\ set' = set

branch1 == /\ pc["test"] = "branch1"

/\ set' = {1}

/\ pc' = [pc EXCEPT !["test"] = "later"]

branch2 == /\ pc["test"] = "branch2"

/\ set' = {2}

/\ pc' = [pc EXCEPT !["test"] = "later"]

test == example \/ later \/ branch1 \/ branch2

Next == test

Spec == /\ Init /\ [][Next]_vars

/\ WF_vars(Next)

/\ SF_vars(test)

/\ SF_vars(branch1)

someone can help? thanks

--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/932afbd1-f11a-4be3-a69a-ac1289ad7e11n%40googlegroups.com.

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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/12016527-CCB4-422F-965E-0D71CA237511%40gmail.com.

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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/743b047f-7830-4805-8dc6-2635f1b29c80n%40googlegroups.com.

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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b8547e2c-f1e7-4dbb-b6dd-8fff117dadfdn%40googlegroups.com.

**References**:**[tlaplus] Fairness and either statement***From:*p.to...@xxxxxxxxxxxxxxxxx

**Re: [tlaplus] Fairness and either statement***From:*Stephan Merz

**Re: [tlaplus] Fairness and either statement***From:*Hillel Wayne

**Re: [tlaplus] Fairness and either statement***From:*Leslie Lamport

**Re: [tlaplus] Fairness and either statement***From:*Huailin

- Prev by Date:
**Re: [tlaplus] Re: Is the latex source for specifying systems available? Or any other version of the published pdf file?** - Next by Date:
**[tlaplus] About Enabled semantics** - Previous by thread:
**Re: [tlaplus] Fairness and either statement** - Next by thread:
**[tlaplus] Re: Is the latex source for specifying systems available? Or any other version of the published pdf file?** - Index(es):