TLA+ (Temporal Logic of Actions)

These specs are inspired by questions that have come up in the TLA+ email group, exercises in the tutorial, strange situations I have personally encountered while using TLA+ and related tools, or things I generally find interesting.

I hope you enjoy :)