Re: [tlaplus] [PlusCal] Reading procedure result values from a calling process

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

Hi Deividas,

change your variables line to:

     variables result_proc = [p \in {"p_1"} |-> ""];

Markus

> On Dec 11, 2022, at 3:28 AM, Deividas Bražėnas <deividas.brazenas@xxxxxxxxx> wrote:
> 
> Hello,
> I want to call a procedure from the PlusCal process and then read the result immediately. With the current spec, I receive the following error when running model checker to see the output results:
> "Attempted to apply EXCEPT construct to the value defaultInitValue.". I've tried setting the default value to other, but still got the same result. As far as I understand, it happens in 
> 
> Do you know what I may be doing wrong in this case? Thanks for the answers!
> 
> Spec:
> ------------------------------ MODULE GeneratedRbc ------------------------------
> EXTENDS Naturals, Sequences, TLC
> 
> (*--algorithm Rbc
>   variables result_proc
> 
>   procedure proc(var)
>   begin
>     proc:
>       result_proc[self] := var;
>       return;
>   end procedure;
> 
> 
>   process p_1 \in {"p_1"}
>   begin
>     p_1:
>       call proc("p_1");
>       proc_1_res:
>         print <<"p_1: ", result_proc[self]>>;
>   end process;
> end algorithm; *)
> \* BEGIN TRANSLATION (chksum(pcal) = "893da67e" /\ chksum(tla) = "365cf215")
> \* Label proc of procedure proc at line 10 col 7 changed to proc_
> \* Label p_1 of process p_1 at line 18 col 7 changed to p_1_
> CONSTANT defaultInitValue
> VARIABLES result_proc, pc, stack, var
> 
> vars == << result_proc, pc, stack, var >>
> 
> ProcSet == ({"p_1"})
> 
> Init == (* Global variables *)
>         /\ result_proc = defaultInitValue
>         (* Procedure proc *)
>         /\ var = [ self \in ProcSet |-> defaultInitValue]
>         /\ stack = [self \in ProcSet |-> << >>]
>         /\ pc = [self \in ProcSet |-> "p_1_"]
> 
> proc_(self) == /\ pc[self] = "proc_"
>                /\ result_proc' = [result_proc EXCEPT ![self] = var[self]]
>                /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
>                /\ var' = [var EXCEPT ![self] = Head(stack[self]).var]
>                /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
> 
> proc(self) == proc_(self)
> 
> p_1_(self) == /\ pc[self] = "p_1_"
>               /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "proc",
>                                                           pc        |->  "proc_1_res",
>                                                           var       |->  var[self] ] >>
>                                                       \o stack[self]]
>                  /\ var' = [var EXCEPT ![self] = "p_1"]
>               /\ pc' = [pc EXCEPT ![self] = "proc_"]
>               /\ UNCHANGED result_proc
> 
> proc_1_res(self) == /\ pc[self] = "proc_1_res"
>                     /\ PrintT(<<"p_1: ", result_proc[self]>>)
>                     /\ pc' = [pc EXCEPT ![self] = "Done"]
>                     /\ UNCHANGED << result_proc, stack, var >>
> 
> p_1(self) == p_1_(self) \/ proc_1_res(self)
> 
> (* Allow infinite stuttering to prevent deadlock on termination. *)
> Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
>                /\ UNCHANGED vars
> 
> Next == (\E self \in ProcSet: proc(self))
>            \/ (\E self \in {"p_1"}: p_1(self))
>            \/ Terminating
> 
> Spec == Init /\ [][Next]_vars
> 
> Termination == <>(\A self \in ProcSet: pc[self] = "Done")
> 
> \* END TRANSLATION 
> 
> 
> ========================================================================
> 
> The content of this email, including all attachments, is confidential. If you are not the intended recipient, please notify us immediately and delete this email. Any disclosure, copying, distribution or any other use of its content is strictly prohibited.
> 
> -- 
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8d74a665-233f-4ed6-a22f-c49d3d2400a9n%40googlegroups.com.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4CB474CE-7CC6-4637-8D86-6E3BD2AE61E7%40lemmster.de.