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,
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.