[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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

        curr := PeekStack(self);                 \* Fine: there is an element for sure
        pop_stack();                                    \* Now the stack could be empty
            if(StackIsEmpty(self)){              \* Checks the old stack, not stack' !
rebalance2:                                              \* This whole label is unreachable!
                call rotate(Null, Null, root);
            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.