[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] On when TLA+ can stutter

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



    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.