[tlaplus] On when TLA+ can stutter

[recepient recepient <netsmaza@xxxxxxxxx>]

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? 

-- 
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/ea38473b-0cfd-4bc0-8bff-dd4bd733a6bbn%40googlegroups.com.