I havn't looked at the new video series, but when I was trying to get started with TLA+ using the Eclipse toolbox, i got stuck trying to define a behaviour spec for the model checker. Do you know of any good documentation for this? Thanks