Thanks But please correct me when I make a mistake because I need to better understand how this works so I can teach it.
If the state machine as a whole behaves strongly fair and if the State Graph is an accurate representation of that state machine must terminate. (yes/no)
My reasoning is simply that every loop has an exiting transition and hence must, under strong fairness, be exited eventually (until it arrives at "Done").
I assume from what is said that the reason why looping for ever and never taking the exit (from state X) that is offered infinitely often is deemed to be fair behaviour is because from the state X both the looping action and the exiting action are "named " the same. In this example "Count". (yes/no)
If I am correct then I can see no way encode fair behavior of an either .. or .. branch. I tried uncommenting the upx:+ and upy:+ labels but this still leaves a pair of "Count" transition as in the simpler example.
Is there any way to encode (ideally in PlusCal but if not then in TLA+) an algorithm that could take step "upy;+" forever but repeatedly is offered an exit step "upx:+". Hence with no fairness assumption will not terminate, but with a strong fairness assumption must take the exit and terminate.
kind regards david