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

Thank you so much Stephan, I am still learning and I believe part of my problem was confusing order not matter in TLA+ with PlusCal I believe.

On Fri, 31 Dec 2021 at 00:18, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
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 [...]

This version first empties the big jug, then pours the rest (i.e., nothing) into the small jug. It does not transfer the contents of the big jug to the small one.

Subsequent assignments in a group of PlusCal statements without an intervening label are executed in sequence (but without interruption from the execution of other processes). If you'd rather have the assignments being performed in parallel, you should write

big := 0 || small := big + small

Regards,
Stephan

On 30 Dec 2021, at 12:48, Robin Luiten <robin.luiten@xxxxxxxxx> wrote:

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.