PlusCal translation loses fairness condition

[craft095]

TLA+ code in the module below has no WF_vars(P(1)) condition in the Spec:

---------------------------- MODULE FairnessBug ----------------------------

EXTENDS Sequences

(*--algorithm FairnessBug {

macro M() {
    call P();
}

procedure P() {
    Begin: skip;
    return;
}

fair process (x = 1) {
    X_L0: M(); \* Condition disappears
    \* X_L0: call P(); \* Condition appears
}
};

*)
\* BEGIN TRANSLATION (chksum(pcal) = "101b0c60" /\ chksum(tla) = "8e406937")
VARIABLES pc, stack

vars == << pc, stack >>

ProcSet == {1}

Init == /\ stack = [self \in ProcSet |-> << >>]
        /\ pc = [self \in ProcSet |-> "X_L0"]

Begin(self) == /\ pc[self] = "Begin"
               /\ TRUE
               /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
               /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]

P(self) == Begin(self)

X_L0 == /\ pc[1] = "X_L0"
        /\ stack' = [stack EXCEPT ![1] = << [ procedure |->  "P",
                                              pc        |->  "Done" ] >>
                                          \o stack[1]]
        /\ pc' = [pc EXCEPT ![1] = "Begin"]

x == X_L0

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == x
           \/ (\E self \in ProcSet: P(self))
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(x)

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION 

=============================================================================

[tyehle]

This looks like a dup of #431