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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/932afbd1-f11a-4be3-a69a-ac1289ad7e11n%40googlegroups.com.
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
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/12016527-CCB4-422F-965E-0D71CA237511%40gmail.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/743b047f-7830-4805-8dc6-2635f1b29c80n%40googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/743b047f-7830-4805-8dc6-2635f1b29c80n%40googlegroups.com.