Add graceful shutdown of threads for termination

A thread can be associated to a non-live role, in which case it can take
silent steps until it finishes, but it cannot take observable steps.

This allows to prove the yes-no example using the ``right'' model, that
is, the model we showed in the figure in the paper!