Hi,
I found a very interesting behaviour in Toolbox when compiling PlusCal to TLA+.
The versions are:
This is Version 1.5.1 of 1 June 2015 and includes:
- SANY Version 2.1 of 24 February 2014
- TLC Version 2.07 of 1 June 2015
- PlusCal Version 1.8 of 2 April 2013
- TLATeX Version 1.0 of 12 April 2013
I have a variable s, which would represent in the end the stack of some processes, hence to start with, I chose it to be a simple array of sequences, one "stack" per process.
If I name the variable "s", the part of the TLA compilation of the first step, (where a "Push" operation is implemented), looks fine,
step: s[self] := Append(s[self], 1); compiles to
/\ s' = [s EXCEPT ![self] = Append(s[self], 1)]
However if I rename it to "stack", the TLA compilation adds an extra "[self]" to the translation - obviously leading to errors.
step: stack[self] := Append(stack[self], 1); compiles to
/\ stack' = [stack EXCEPT ![self][self] = Append(stack[self], 1)]Can you please help me to understand this behaviour?
As a matter of fact it seems only "stack" case sensitive causes the issue, even "Stack" behaves correctly.
Thank you,
Balint
ps.: the full PlusCal algorithms
with stack:
------------------------ MODULE TestArrayOfSequences ------------------------
(*
--algorithm TestArrayOfSequences {
variable stack = [ i \in 1..NumberOfProcesses |-> <<>>];
process (proc \in 1 .. NumberOfProcesses) {
step: stack[self] := Append(stack[self], 1);
}
}
*)
\*BEGIN TRANSLATION
VARIABLES stack, pc
vars == << stack, pc >>
ProcSet == (1 .. NumberOfProcesses)
Init == (* Global variables *)
/\ stack = [ i \in 1..NumberOfProcesses |-> <<>>]
/\ pc = [self \in ProcSet |-> "step"]
step(self) == /\ pc[self] = "step"
/\ stack' = [stack EXCEPT ![self][self] = Append(stack[self], 1)] \* the error
/\ pc' = [pc EXCEPT ![self] = "Done"]
proc(self) == step(self)
Next == (\E self \in 1 .. NumberOfProcesses: proc(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\*END TRANSLATION
=============================================================================
------------------------ MODULE TestArrayOfSequences ------------------------
EXTENDS Integers, Sequences, TLC
CONSTANT NumberOfProcesses
(*
--algorithm TestArrayOfSequences {
variable s = [ i \in 1..NumberOfProcesses |-> <<>>];
process (proc \in 1 .. NumberOfProcesses) {
step: s[self] := Append(s[self], 1);
}
}
*)
\*BEGIN TRANSLATION
VARIABLES s, pc
vars == << s, pc >>
ProcSet == (1 .. NumberOfProcesses)
Init == (* Global variables *)
/\ s = [ i \in 1..NumberOfProcesses |-> <<>>]
/\ pc = [self \in ProcSet |-> "step"]
step(self) == /\ pc[self] = "step"
/\ s' = [s EXCEPT ![self] = Append(s[self], 1)] \* the good version
/\ pc' = [pc EXCEPT ![self] = "Done"]
proc(self) == step(self)
Next == (\E self \in 1 .. NumberOfProcesses: proc(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\*END TRANSLATION
============================================================ =================