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

[Dan Tisdall <danwtisdall@xxxxxxxxx>]

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/db55b7e3-a6f5-4a81-a56f-a38ef318b577n%40googlegroups.com.