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
\* Last modified Wed Jul 29 16:27:10 EDT 2020 by huaixl
\* Created Wed Jul 29 16:18:17 EDT 2020 by huaixl