# Re: [tlaplus] PlusCal Translation problem

Hi Huaixi,

> Op 29 jul. 2020, om 22:30 heeft luhuaixi2014@xxxxxxxxx het volgende geschreven:
>
> Hi,
>
> I encounter a problem regarding with PlusCal translation.
>
> One simple example is below: each process in A holds a queue;
>
> but if a process called "b1" work on one queue like "bb: queue["a1"] := queue["a1"] \cup {"temp"};", it will be translated to queue' = [queue EXCEPT !["b1"]["a1"] = queue["b1"]["a1"] \cup {"temp"}];
>
> but queue doesn't have a field called "b1"...
>
> Do you know how to deal with this problem?

In your code, queue is defined to be a variable of process A, not a global variable. Therefore, if process B refers to the variable, it is assumed to be a local variable as well. If you want to communicate between processes, you should define queue to be a global variable, perhaps like this:

(* --algorithm test {
variable queue = [a \in A |-> {}]; (* yes, it is ok to use A here; the translation will place the initialisation after the definition of A *)

define {
A == {"a1", "a2"}
}

fair process (a \in A)
{
aa: skip; (* refer to the queue variable as "queue[self]" *)
}

fair process (b = "b1")
{
bb: queue["a1"] := queue["a1"] \cup {"temp"};
}
}*)

Kind regards,
David N. Jansen.

--
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/25D44A03-369D-43D7-88EC-29FA41DBFF46%40ios.ac.cn.