I would give it every example TLA+ file you can find, including PlusCal stuff (as reference). Also provide an up to date language manual and/or grammar if you have one.