[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

PlusCal: implicit label Error (PlusCal translator bug?)


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

  procedure f(x) {
    call h(args, moreargs);
    if (condition)
      call g(x);

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"]
          /\ 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,