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