Re: [tlaplus] PlusCal Translation problem

["David N. Jansen" <dnjansen@xxxxxxxxx>]

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.