I am new to TLA+ (taking another go at playing at it since my last time) and was working through the tla-video's.
I got up to the exercise related to the Die Hard Water Jug problem.
I solved it using PlusCal just to see if i could before looking at the rest of the video on the problem.
Once I had it running I went back and improved what I had created and ran into this behavior.
It appears to me the generated TLA+ is using a primed identifier when it shouldn't be.
If i swap the lines around marked "Line A" and "Line B" one oriention works and the assert for `big /\ 4` works the other swapping lines does not trigger than alert.
I did some searching and found the github issue
"
PlusCal translation incorrectly depends on definition"
https://github.com/tlaplus/tlaplus/issues/338 This seemed related as it talked about primed and unprimed variables in the TLA+ translation.
This example worries me that the order of my statements in a block makes it behave different.
I have included the PlusCal code here.
Just paste it into a new spec generate new model and run it to see behavior.
The code below as pasted will not find the `assert big /= 4`
Which i believe means the line `/\ small' = big' + small` in TLA+ BigToSmall is primed access to big` which breaks it.
But swapping lineA and lineB around in the PlusCal it will stop on `assert big /= 4` behve as expected as it will use big and not big`.
```
EXTENDS TLC, Integers
\* Appears to be related issue
https://github.com/tlaplus/tlaplus/issues/338\* by reordering
(* --algorithm diehardJugProblem
variables small = 0, big = 0,
define
TypeOK ==
/\ small \in 0..3
/\ big \in 0..5
end define;
begin
WhileLoop:
while TRUE do
assert TypeOK;
assert big /= 4; \* this failing means we got to goal
either
FillBig:
big := 5;
or
FillSmall:
small := 3;
or
EmptyBig:
big := 0
or
EmptySmall:
small := 0
or
SmallToBig:
if big + small =< 5
then
big := big + small;
small := 0;
else
big := 5;
small := big + small - 5;
end if;
or
BigToSmall:
if big + small =< 3
then
big := 0; \* lineA first fails to assert big /= 4
small := big + small; \* lineB first will assert big /= 4 as expected
else
big := big + small - 3;
small := 3;
end if;
end either;
end while;
end algorithm; *)
```
On Friday, 5 February 2021 at 3:42:34 am UTC+10 Dan Tisdall wrote:
I'll just add this here as it may help somebody in the future track down this problem if they have a similar one. I was bitten by this today and it took me a while to find this thread which has cleared it up for me. My code had this problem and it was a bit hidden. Here is my code
```
rebalance1:
while(~StackIsEmpty(self)){
curr := PeekStack(self); \* Fine: there is an element for sure
pop_stack(); \* Now the stack could be empty
adjust_node_height(curr);
if(~IsBalanced(curr)){
if(StackIsEmpty(self)){ \* Checks the old stack, not stack' !
rebalance2: \* This whole label is unreachable!
call rotate(Null, Null, root);
return;
};
rebalance3:
assert ~StackIsEmpty(self); \* Will fail because we did not early return as may have been expected
```
Now I know that I should either not use operators in these situations, or use additional labels.