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

*From*: Robin Luiten <robin.luiten@xxxxxxxxx>*Date*: Thu, 30 Dec 2021 03:48:25 -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> <db55b7e3-a6f5-4a81-a56f-a38ef318b577n@googlegroups.com>

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

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.

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; *)

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

**Follow-Ups**:**Re: [tlaplus] Potentially confusing behavior of a PlusCal algorithm***From:*Stephan Merz

**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm***From:*Robin Luiten

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

**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm***From:*Dan Tisdall

- Prev by Date:
**Re: [tlaplus] Checking Invariants vs Properties** - Next by Date:
**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm** - Previous by thread:
**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm** - Next by thread:
**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm** - Index(es):