Re: [tlaplus] Fairness and either statement

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.