Question about some concepts

[yihao yang <yangyi...@xxxxxxxxx>]

Hello there,

I am learning TLA+ from Lamport's video course. I feel confused about some concepts.

Here are my questions.
1. Does deadlock mean that only the stuttering steps can be taken at the tail of the valid behaviors?
2. Is it possible to check deadlock directly by the TLA spec itself, but not by the toolbox option? What is the difference between deadlock and termination? How to specify the termination of a spec in the TLA+ spec?

Could any one give me some advices?

Thanks,
Yihao