# [tlaplus] PlusCal Translation problem

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?

Best,

Huaixi

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

EXTENDS Integers, TLC

(* --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