I'm playing around with TLA+, and thought I'd write the following clearly false specification in PlusCal:
---- MODULE transfer ----
EXTENDS Naturals, TLC, Sequences
(* --algorithm transfer
\* Simple algorithm:
\* 1. Start with a shared-memory list with one element.
\* 2. A process adds arbitrary numbers of elements to the list.
\* 3. Another process removes arbitrary numbers of elements from the list,
\* but only if the list has more than one item in it. This check is
\* applied just before trying to removing an element.
\* Is it true that the list will always have a length of 1?
\* You would expect this to be false, since the adder process can add more elements
\* than the remover process can consume.
variables stack = <<0>>
process Adder = 0
begin
AddElement:
stack := Append(stack, Len(stack));
either goto AddElement
or skip
end either;
end process;
process Remover = 1
begin
RemoveElement:
\* Pop from the front of the stack
if Len(stack) > 1 then
stack := Tail(stack);
end if;
either goto RemoveElement
or skip
end either;
end process;
end algorithm *)
IsStackAlwaysUnitLength == Len(stack) = 1
====
After checking IsStackAlwaysUnitLength as one of the temporal properties to report on, I expected TLA+ to mark this property as failed.
However, all states passed! Why is it not failing?
On debugging with print statements, I noticed the following odd behaviour:
process Adder = 0
begin
AddElement:
print stack;
print "Adder applied!";
stack := Append(stack, Len(stack));
print stack;
print "Adder task complete!";
\* Force
either goto AddElement
or skip
end either;
end process;
process Remover = 1
begin
RemoveElement:
\* Pop from the front of the stack
print stack;
print "Remover applied!";
if Len(stack) > 1 then
stack := Tail(stack);
print stack;
print "Remover task complete!";
else
print "Remover task complete!";
end if;
either goto RemoveElement
or skip
end either;
end process;
yields in the debugging panel
<<0>>
"Adder applied!"
<<0>>
"Adder task complete!"
<<0>>
<<0>>
"Remover applied!"
"Remover applied!"
"Remover task complete!"
"Remover task complete!"
<<0>>
"Adder applied!"
<<0>>
"Adder task complete!"
I'm unsure why stack := Append(stack, Len(stack)); and stack := Tail(stack); are not updating the global stack variable.
---- MODULE transfer ----
EXTENDS Naturals, TLC, Sequences
(* --algorithm transfer
variables stack = <<0>>
process Adder = 0
begin
AddElement:
stack := Append(stack, Len(stack));
either goto AddElement
or skip
end either;
end process;
process Remover = 1
begin
RemoveElement:
\* Pop from the front of the stack
if Len(stack) > 1 then
stack := Tail(stack);
end if;
either goto RemoveElement
or skip
end either;
end process;
end algorithm *)
\* BEGIN TRANSLATION
VARIABLES stack, pc
vars == << stack, pc >>
ProcSet == {0} \cup {1}
Init == (* Global variables *)
/\ stack = <<0>>
/\ pc = [self \in ProcSet |-> CASE self = 0 -> "AddElement"
[] self = 1 -> "RemoveElement"]
AddElement == /\ pc[0] = "AddElement"
/\ stack' = [stack EXCEPT ![0] = Append(stack, Len(stack))]
/\ \/ /\ pc' = [pc EXCEPT ![0] = "AddElement"]
\/ /\ TRUE
/\ pc' = [pc EXCEPT ![0] = "Done"]
Adder == AddElement
RemoveElement == /\ pc[1] = "RemoveElement"
/\ IF Len(stack) > 1
THEN /\ stack' = [stack EXCEPT ![1] = Tail(stack)]
ELSE /\ TRUE
/\ stack' = stack
/\ \/ /\ pc' = [pc EXCEPT ![1] = "RemoveElement"]
\/ /\ TRUE
/\ pc' = [pc EXCEPT ![1] = "Done"]
Remover == RemoveElement
Next == Adder \/ Remover
\/ (* 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
IsStackAlwaysUnitLength == Len(stack) = 1
====
Congratulations, you've hit a PlusCal bug! And also an edge case that's not a bug but still unintuitive. Let's start with the bug.
Sometimes when using PlusCal we want to have multiple processes share labels. We do this with a procedure. In order to make it all work the PlusCal translator adds an extra bookkeeping variable called stack. Normally, if the user defines a variable foo that conflicts with a generated variable foo, the translation renames one to foo_. In this case, since there was no conflict, there wasn't any renaming.* The bug is that the translator got confused and translated the variable as if it was supposed to be the bookkeeping stack. You can see this as it turned the append into
stack' = [stack EXCEPT ![0] = Append(stack, Len(stack))]
When it should just be
stack' = Append(stack, Len(stack))
You can fix this by renaming stack to mystack. That should get the spec behaving properly. But it will still pass: that's because you put IsStackAlwaysUnitLength as a property and not an invariant. As a temporal property, IsStackAlwaysUnitLength is true if it's true in the initial state. As an invariant, IsStackAlwaysUnitLength is true if it's true in all states.** YOu can get the spec to fail properly by changing IsStackAlwaysUnitLength from a temporal property to an invariant in the "what is the model" page.
*Actually in this case the translator won't rename stack if you add a procedure, it just throws an error. But that's still fail-safe.
**This is because TLC (the model checker) treats the invariant P as the temporal property []P. It's syntactic sugar, basically.