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

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



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.