TLC simulation error with liveness properties

[lemmy]

When PSet is defined to be a tuple and TLC in simulation mode (Toolbox 1.5.6/TLC 2.12 of 29 January 2018) is set to verify the Worked (or generated Termination) liveness property, TLC fails with:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to apply EXCEPT construct to the string "Done".

------------------------------ MODULE bug ---------------------------------
EXTENDS Naturals

Worked == <>(TRUE)

PSet == {"p"} \X (1..2)

(* --algorithm bug {

  process (p \in PSet) {
       lbl: skip;
  }
  
} *)
===================================

This bug shows up for both liveness implementations /tlatools/src/tlc2/tool/liveness/LiveCheck1.java and /tlatools/src/tlc2/tool/liveness/LiveCheck.java

---

Unknown sourcecode changes have resulted in a change of the error message in the version of TLC as of 08/21/2019:

Wrong invocation of TLC error printer. Error code not found.