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 + smallRegards,StephanOn 30 Dec 2021, at 12:48, Robin Luiten 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 diehardJugProblemvariables small = 0, big = 0,define  TypeOK ==     /\ small \in 0..3     /\ big \in 0..5end define;beginWhileLoop: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 coderebalance1:    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 expectedNow 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. -- 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/4947E10C-5716-4E8C-B95B-4C657130FC5B%40gmail.com.