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

*From*: "David N. Jansen" <dnjansen@xxxxxxxxx>*Date*: Wed, 29 Jul 2020 21:52:52 +0000*Accept-language*: nl-NL, zh-CN, en-US*References*: <d59b34af-0c76-45cb-8997-d19600266bb1o@googlegroups.com>*Thread-index*: AQHWZe0FbXLuKDi8yUymi4NOJrhB6akek0MA*Thread-topic*: [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.

**References**:**[tlaplus] PlusCal Translation problem***From:*luhuaixi2014

- Prev by Date:
**[tlaplus] PlusCal Translation problem** - Next by Date:
**[tlaplus] In TLC, what are "generated" vs "distinct" states?** - Previous by thread:
**[tlaplus] PlusCal Translation problem** - Next by thread:
**[tlaplus] In TLC, what are "generated" vs "distinct" states?** - Index(es):