Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm

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
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.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.