[tlaplus] Re: On when TLA+ can stutter

>[specification] allows for executions that stutter indefinitely from any point onwards, therefore termination is not guaranteed. Invariance to stuttering is a fundamental concept of TLA+, and for verifying liveness properties you >always need some fairness conditions in order to rule out indefinite stuttering.

In my example, with <<5>> sitting in q_in, the code at the dequeue label is enabled infinitely often. However, unless I tell TLA to assume weak fairness, TLA may assume unfair execution and simply leave the process unchanged ad infinitum whether, depending on taste and your preferred emphasis, it executes ' q_in := Tail(q_in)' or after running ' q_in := Tail(q_in); goto ....' but not the await itself. Telling TLA to assume weak fairness means that if an state is enabled infinitely often .... then TLA has to eventually transition into that state whence 5 is dequeued, q_out = <<1,2,3,4,5>> and the property is true.

Apologies if this is the stunningly obvious to others; writing whether asking or answering helps me learn and retain information.

On Thursday, November 19, 2020 at 5:10:37 PM UTC-5 recepient recepient wrote:

Consider this process in which the process is instructed to atomically await for work, dequeue an element from the input q and append it to the output queue doing this indefinitely until q_in empty:
process Dequeue \in 1..1

begin

dequeue:

await q_in /= <<>>;

q_out := q_out \o << Head(q_in) >>;

q_in := Tail(q_in);

goto dequeue;

end process;

Running this with a LTL property,
WorkDone == <>([](q_out=<<1,2,3,4,5>>))

and a good enqueue process (not shown) shows a violation. The violation is a result of stuttering, In fact, the last state in the trackback shows,

/\ i = (2 :> 6)
/\ pc = <<"dequeue", "Done">>
/\ q_in = <<5>>
/\ q_out = <<1, 2, 3, 4>>

which asks the question: since Dequeue is unconditionally instructed to loop back to the await statement whence 5 would be dequeue making q_out <<1,2,3,4,5>> thus satisfying WorkDone, why does TLA+ think it can stutter and think it can stutter with one element left? Are we to interpret this as Dequeue may have "crashed" there?