Note: in posting this, I may have inadvertently deleted another posting.
If I deleted your posting, please feel free to re-post.
The error message says
=> has both temporal formula and action as arguments
The [] in the formula means that the entire formula is a TLA+ temporal
formula. However, the subformula [Next]_vars, which is an action
formula, is not a legal TLA temporal formula. Hence the entire
formula is illegal. (The construct [N]_v can appear in a temporal
formula only in a subformula [][N]_v .)
The [] in the formula is spurious, and it should read
<2>1. Inv /\ [Next]_vars => Inv
Earlier versions of the parser did not catch that error; the check for
it was not added until October 2013. Apparently, the proof was not
rerun with the current version. TLAPS assumes that proofs have been
successfully parsed by the Toolbox. Since the "proof" of that step is
PROOF OMITTED, there is no reason TLAPS should have found the error.
Leslie