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

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.