There are two specifications:

DieHard
  A very elementary example taken from a movie that introduces
  TLA  and the use of the TLC model checker.  It solves a of
  obtaining 4 gallons of water using two buckets of capacity 
  3 and 5 gallons.
  
DieHarder 
  A generalization of DieHard in which the amount of water
  to produce and the number of buckets and their capacities 
  are parameters.  It introduces the TLA  operators for
  handling functions (known to programmers as arrays).