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

[Robin Luiten <robin.luiten@xxxxxxxxx>]

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.

-- 
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/41971ee3-b348-4cd7-85e4-9402307d50e8n%40googlegroups.com.