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

*From*: Hillel Wayne <hwayne@xxxxxxxxx>*Date*: Tue, 6 Jul 2021 11:13:45 -0500*Ironport-hdrordr*: A9a23:P1599ag7emopXnNztEgCTnCm6HBQXjAji2hC6mlwRA09TyXPrbHWoB19726WtN9xYhEdcL+7U5VoLUm3yXde2/h3AV7BZmbbURqTTb2KhLGKqwEIfReSygc378ldmsZFZOEYJGIK9frS0U2XE8sEyNLC2Ly0hOHEpk0dKz1CWuVP7xpdAg3eK1ZxRwVNGPMCZfihz/sCiTq8XHwdKv2hAHoIVfWGh9CjruOCXTc2QzAm9SyHhneQ87j4HxKEmi4XTjIn+8ZHzVT4*References*: <932afbd1-f11a-4be3-a69a-ac1289ad7e11n@googlegroups.com> <12016527-CCB4-422F-965E-0D71CA237511@gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b5577792-3591-7262-199a-282c22386be4%40gmail.com.

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

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

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

- 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:
**Re: [tlaplus] Fairness and either statement** - Previous by thread:
**Re: [tlaplus] Fairness and either statement** - Next by thread:
**Re: [tlaplus] Fairness and either statement** - Index(es):