Q2. the Next loops are caused by the TLA+ (pc = "Done" /\ UNCHANGED vars) clause as can be seen by commenting them out. Not sure though what you have to do the PlusCal to prevent this clause being formed.
\* \/ (* Disjunct to prevent deadlock on termination *)
\* (pc = "Done" /\ UNCHANGED vars)
If I understand it correctly, pc' has become "Done" in Lbl_1, why is there still deadlock?
My another related question is about the clause:
Spec == Init /\ [Next]_vars
How does tla execute the spec? What's the execution logic when it encounters /\ and \/ ? Are they executed in a single step or not?
Also, I don't quite what [Next]_vars means.
Right now, I am fine with the pluscal language.