Re: [tlaplus] Re: PlusCal: implicit label Error (PlusCal translator bug?)

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

Bump. Reattaching the minimal test-case.

On 02.12.2015 15:45, Jaak Ristioja wrote:
> On 01.12.2015 18:28, Leslie Lamport wrote:
>> A goto to the "Error" label is supposed to be executed when execution
>> reaches the end of a procedure without finding a return statement.  I
>> suspect that in this case, the return is returning to someplace that
>> drops it off the end of a calling procedure.  I can't tell exactly
>> what's happening without seeing a complete example.  If you have an
>> example in which such a goto is being executed when it shouldn't be,
>> please send it to me.  (But please try to pare it down to the smallest
>> example you can find.)
> 
> I've attached a minimum testcase to this email. It seems that a
> workaround is to write
> 
>   if (cond) {
>     call g();
>   };
>   return;
> 
> instead of simply:
> 
>   if (cond)
>     call g();
>   return;

Any update on this?

>> The translator does not produce an error because it doesn't know
>> whether that goto "Error" can actually be executed.  Determining
>> whether a particular statement in a program will be executed is an
>> unsolvable problem, and we had more important things to do than add
>> heuristics to the translator for attempting to solve this problem.
> 
> I agree, but I don't currently see why anybody would want to or should
> be allowed to write PlusCal procedures which fall off the end. Can you
> present an use-case for this? Wouldn't it just be better for the PlusCal
> procedure to always return implicitly when it reaches the end of the
> procedure block?

I've been thinking about this for a few days and have come up with no
good use case. Anybody?

Best regards,
Jaak

-------------------------------- MODULE bug --------------------------------
EXTENDS Sequences

(* --algorithm bug {

procedure g() { return; }

procedure f() {
  if (FALSE)
    call g();
  return;
} 

{ call f(); } \* Single process

} *)

\* BEGIN TRANSLATION
VARIABLES pc, stack

vars == << pc, stack >>

Init == /\ stack = << >>
        /\ pc = "Lbl_3"

Lbl_1 == /\ pc = "Lbl_1"
         /\ pc' = Head(stack).pc
         /\ stack' = Tail(stack)

g == Lbl_1

Lbl_2 == /\ pc = "Lbl_2"
         /\ IF FALSE
               THEN /\ stack' = << [ procedure |->  "g",
                                     pc        |->  Head(stack).pc ] >>
                                 \o Tail(stack)
                    /\ pc' = "Lbl_1"
               ELSE /\ pc' = "Error"
                    /\ stack' = stack

f == Lbl_2

Lbl_3 == /\ pc = "Lbl_3"
         /\ stack' = << [ procedure |->  "f",
                          pc        |->  "Done" ] >>
                      \o stack
         /\ pc' = "Lbl_2"

Next == g \/ f \/ Lbl_3
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

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