PlusCal: implicit label Error (PlusCal translator bug?)

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

Hello!

I'm using a less than a week old nightly build. I have a procedure like
this:

  procedure f(x) {
  f_start:
    call h(args, moreargs);
  myLabel:
    if (condition)
      call g(x);
    return;
  }

The PlusCal code under myLabel gets translated to something like:

  myLabel(self) ==
    /\ pc[self] = "myLabel"
    /\  IF cond THEN
          /\ /\ stack' = [stack EXCEPT ![self] =
                    << [ procedure |-> "g",
                        pc |-> Head(stack[self]).pc,
                        x_M |-> x_M[self] ] >>
                    \o Tail(stack[self])
                ]
             /\ x_M' = [x_M EXCEPT ![self] = x_O[self]]
          /\ pc' = [pc EXCEPT ![self] = "g_start"]
        ELSE
          /\ pc' = [pc EXCEPT ![self] = "Error"]
          /\ UNCHANGED << stack, x_M >>
    /\ UNCHANGED << long, list, of, vars, here >>

Can anybody explain why the ELSE branch jumps to the implicit Error label?

Secondly, as this resulted in TLC detecting a deadlock after running for
almost a whole working day, I began to wonder: Why does PlusCal even
have an implicit Error label? Why doesn't the PlusCal translator,
instead of emitting TLA+ code for a jump (to the implicit Error label)
just fail with an error? This would have saved me many hours on waiting
on TLC to finish.


Best regards,
Jaak