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

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

I forgot to mention I'm on windows 10, and using TLA+ Toolbox 1.7.1.
I did try 1.8.0 version when i saw it was out and it showed the same behavior.
On Thursday, 30 December 2021 at 9:48:25 pm UTC+10 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"
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`.


\* Appears to be related issue https://github.com/tlaplus/tlaplus/issues/338
\* by reordering

(* --algorithm diehardJugProblem
variables small = 0, big = 0,
  TypeOK ==
    /\ small \in 0..3
    /\ big \in 0..5
end define;

while TRUE do
  assert TypeOK;
  assert big /= 4; \* this failing means we got to goal

    big := 5;
    small := 3;
    big := 0
    small := 0
    if big + small =< 5
        big := big + small;
        small := 0;
        big := 5;
        small := big + small - 5;
    end if;
    if big + small =< 3
        big := 0;             \* lineA first fails to assert big /= 4
        small := big + small; \* lineB first will assert big /= 4 as expected
        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

        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/242334be-7b76-48ac-bb60-00121f191144n%40googlegroups.com.