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

*From*: Dan Tisdall <danwtisdall@xxxxxxxxx>*Date*: Thu, 4 Feb 2021 09:40:19 -0800 (PST)*References*: <4d003c31-6b8c-4782-8885-65649ffe5fbe@googlegroups.com> <737588d7-2282-4ebb-aceb-174940a1f8ae@googlegroups.com> <0f378b2a-24d0-4821-b309-6e1366a63bfe@googlegroups.com> <e1d154c8-d6a8-40dc-be3c-33da8faf3446@googlegroups.com> <CABf5HMj5QFqdY8w=SiXrMfiCnrcYhte=cvs1Z-HBEGZ=7q_9ow@mail.gmail.com> <88a4b115-ddd8-4d36-843e-f5115812357d@googlegroups.com> <CABf5HMgx1di5rXcphy2hw+m_Fc-p28W=KxtmbcOeigxU=bXW7g@mail.gmail.com> <4a97c30c-e004-4787-b455-9392222e2dcfn@googlegroups.com>

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.

**References**:**Potentially confusing behavior of a PlusCal algorithm***From:*Giuliano

**Re: Potentially confusing behavior of a PlusCal algorithm***From:*Leslie Lamport

**Re: Potentially confusing behavior of a PlusCal algorithm***From:*Giuliano

**[tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm***From:*Daniel Ricketts

**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm***From:*Calvin Loncaric

**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm***From:*Leslie Lamport

**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm***From:*Calvin Loncaric

**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm***From:*Leslie Lamport

- Prev by Date:
**[tlaplus] Re: What are the TLA+ source files in the model folder?** - Next by Date:
**[tlaplus] Modelling the Philosophers Dining Problem** - Previous by thread:
**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm** - Next by thread:
**Issues with running TLA toolbox on Mac OS X 10.10.5** - Index(es):