I believe I see your misunderstanding:
The temporal-property violating loop occurs under the following steps:
- we start in your initial state
- then we take a `rData` step, pink arrow, wherein `wayBack` becomes <<1>>
- then we take an `aWire` step, green arrow, wherein `endBack` becomes <<1>> and `wayBack` returns to <<>>
- then we take an `sData` step, blue arrow, which brings us back to the initial state
As a reminder, Spec looks like this
Spec == /\ Init /\ [][Next]_vars
/\ WF_vars(Next)
/\ SF_vars(ackWire)
/\ SF_vars(sData \/ ssd)
/\ SF_vars(receiver)
(I replaced `sender` with `sData \/ ssd`, as that is what `sender` is defined as)
If we look at your initial state in the state graph, we can see that there are two possible exists from it:
- A pink arrow to the right, 'rData', which is the one involved in the infinite loop
- A blue arrow to the left, 'sData', which is the one you _want_ to see eventually taken
Your question roughly is: "Why is an infinite loop allowed, shouldn't strong fairness guarantee that we eventually take that `sData` step out of the initial state?"
Let's recall what strong fairness means:
"Strong fairness asserts the a step `A` must occur if `A` is repeatedly enabled, even if it is also repeatedly disabled"
i.e., if some step is repeatedly made possible to take, then we'll eventually take it.
But now let's look at the steps that are taking place in your infinite loop:
rData -> aWire -> sData
Those steps take place over and over. And what's the third step there? An `sData` step! So your strong fairness is satisfied!
We've told the system that if `sData` is repeatedly enabled, then it must eventually be taken. The confusion in your system is that it's enabled _both_ from your initial state, but also after the `aWire` step takes place. It's enabled in two different places along the path of your infinite loop!
So while you personally would like to see that step taken from the initial state, the conditions of strong fairness are perfectly satisfied by that infinite loop. `sData` is repeatedly enabled in that infinite looping behaviour, and the `sData` step is always eventually taken. It always happens to only take the step in one of the two possible places it _could_ take the step, but that doesn't matter to TLA+.
I hope that helps!