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

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



    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 + small

Regards,
Stephan

On 30 Dec 2021, at 12:48, Robin Luiten <robin.luiten@xxxxxxxxx> 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 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.

--
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.