Re: How does Fairness relate to the State Graph

Strong fairness is not required here, and in any event, no kind of fairness means that *all* possible next states of a fair action will eventually be taken. A fair action, weak or strong, simply means that if a certain action is enabled "well enough" (strong and weak fairness differ on what "well enough" means), then eventually *one* of its next states will be taken. If you want a particular "branch" to be eventually taken, then that branch must be written as a separate fair action. In PlusCal that simply means marking it with its own label.

Ron

On Wednesday, February 6, 2019 at 8:52:54 PM UTC+1, david streader wrote:

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