[tlaplus] PlusCal Translation Problem

Hi,

I came across a problem related to PlusCal Translation.

Each process in A maintains a queue, but if another process called “b1” tries to work on one of the queues like “bb: queue["a1"] := queue["a1"] \cup {"temp"};”, it will be translated into “queue' = [queue EXCEPT !["b1"]["a1"] = queue["b1"]["a1"] \cup {"temp"}]”. But queue doesn’t have a field named “b1” or a variable called queue…

Do you know how to deal with this problem? The example code is attached.

Best,

Huaixi

-------------------------------- MODULE test --------------------------------

EXTENDS Integers, TLC

\* TLC is used to assert

(* --algorithm test {

define {

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

}

fair process (a \in A)

variable queue = {};

{

aa: skip

}

fair process (b = "b1")

{

bb: queue["a1"] := queue["a1"] \cup {"temp"};

}

\* BEGIN TRANSLATION - the hash of the PCal code: PCal-a27fafedd7e2ba12347a0c996d5f9fc3

VARIABLE pc

(* define statement *)

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

VARIABLE queue

vars == << pc, queue >>

ProcSet == (A) \cup {"b1"}

Init == (* Process a *)

/\ queue = [self \in A |-> {}]

/\ pc = [self \in ProcSet |-> CASE self \in A -> "aa"

[] self = "b1" -> "bb"]

aa(self) == /\ pc[self] = "aa"

/\ TRUE

/\ pc' = [pc EXCEPT ![self] = "Done"]

/\ queue' = queue

a(self) == aa(self)

bb == /\ pc["b1"] = "bb"

/\ queue' = [queue EXCEPT !["b1"]["a1"] = queue["b1"]["a1"] \cup {"temp"}]

/\ pc' = [pc EXCEPT !["b1"] = "Done"]

b == bb

(* Allow infinite stuttering to prevent deadlock on termination. *)

Terminating == /\ \A self \in ProcSet: pc[self] = "Done"

/\ UNCHANGED vars

Next == b

\/ (\E self \in A: a(self))

\/ Terminating

Spec == /\ Init /\ [][Next]_vars

/\ \A self \in A : WF_vars(a(self))

/\ WF_vars(b)

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-87e5d335b185538961bc5497fdefd792

=============================================================================

\* Modification History

\* Last modified Wed Jul 29 16:27:10 EDT 2020 by huaixl

\* Created Wed Jul 29 16:18:17 EDT 2020 by huaixl