Potentially confusing behavior of a PlusCal algorithm

[Giuliano]

Hello, consider the following algorithm:

--algorithm Algo1 {

    variables b1 = FALSE, b2 = FALSE

    

    define {

        B1 == b1

    }

    

    fair process (stuck \in {"stuck"}) {

        l1: b1 := TRUE;

            await B1;

    }

    

    fair process (notstuck \in {"notstuck"}) {

        l2: b2 := TRUE;

            await b2;

    }

The process "stuck" will never reach the label "Done", while the process "notstuck" will reach it.

This kind of behavior may cause confusion in a more complex algorithm and I could not find any warning about it in the PlusCal user's manual.

Cheers,

Giuliano

[Leslie Lamport]

Please explain what you find confusing about this.

Thanks,

Leslie

[Stephan Merz]

Hi Giuliano,

if you look at the TLA+ produced by the PlusCal translator, you'll see that 

B1 == b1

l1 ==

  /\ b1' = TRUE

  /\ B1

  /\ ...

l2 ==

  /\ b2' = TRUE

  /\ b2'

  /\ ...

The translator notices that the await statement in l2 refers to the variable b2 that has been assigned to before, and that the expression b2 should therefore be translated as b2' rather than b2. However, it doesn't notice that B1 involves b1; this would require a finer syntactic analysis than what the translator appears to do.

I had a quick look at the PlusCal manual and did not see a clear description of how exactly expressions are translated. (There is a sentence that says that the expressions in TLA+ are mostly like the ones in the PlusCal algorithm except for some changes, including adding primes.) I do not think that anybody ever attempted to write up a more abstract operational semantics of PlusCal than what is implemented in the PlusCal translator.

Best,

Stephan

--
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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Leslie Lamport]

Hi

I'm sorry for my previous clueless response; I read your posting too
quickly.

The basic rule is that the PlusCal translator does not expand
definitions; occurrences of defined operators appear in the
translation exactly as they appear in the source code.  I believe this
is the best way to handle definitions.  If the user wants the
translator to do the expansion, she can use a macro (admittedly, not
in exactly the same way). 

Given this rule, there is nothing the translator can or should do.  In
your example, it would be possible to translate the occurrence of B1
as B1'.  But in general, the definition could contain variables that
both "should" and "shouldn't" be primed.  Also, since the user could
have defined B1 to equal b1' in your example, it's not at all clear
what he would want the translator to do.

That said, this is something that should have been documented better.
Currently, the documentation is by omission.  Appendix section B of
the manual states where the definitions appear in the translation, and
the description of how the code is translated says nothing about doing
anything special with definitions.  I will add a sentence or two to
Section 3.6 saying that uses of defined operators appear in the
translation as they appear in the code.  Please let me know if you
find anyplace else where that should appear.

Thanks,

Leslie


On Tuesday, October 20, 2015 at 5:21:39 PM UTC-7, Giuliano wrote:

[Giuliano]

Thanks Leslie and Stephan for your answers.

What about adding a subsection to section 3 about statement sequences that form an atomic step, describing when variables are primed and when not?

Giuliano

[Daniel Ricketts]

I’d like to resurrect this thread because I recently was surprised by the behavior described in the original post. I was surprised because I didn’t carefully read the part of the PlusCal manual that says:

Definitions, including ones in a define statement, are not expanded in the PlusCal to TLA+ translation. All defined symbols appear in the translation exactly as they appear in the PlusCal code.

However, the manual also says:

you can omit the labels and let the PlusCal translator add them as necessary. You are likely to do this only for uniprocess (sequential) algorithms, where the partitioning of the computation into steps does not affect the values computed

It seems like it is possible to violate this property using definitions. For example, the following two sequential algorithms compute different values, despite differing only in the labeling:

--algorithm A
{
    variables x = 0, y = 0;

    define {
        x_alias == x
    }

    {
        step1: x := 1;
               y := x_alias;
    }
}

--algorithm B
{
    variables x = 0, y = 0;

    define {
        x_alias == x
    }

    {
        step1: x := 1;
        step2: y := x_alias;
    }
}

Algorithm A terminates in a state in which x equals 1 and y equals 0, while algorithm B terminates in a state in which x and y both equal 1. Am I misunderstanding the manual?

[Calvin Loncaric]

This has shaken my confidence in PlusCal and I am less likely to use it in the future.

The problematic code contains a "hidden read-after-write"; in Dan's example, the x_alias definition hides a read of x that happens after the write to x. The PlusCal translator should do something reasonable instead of mistranslating hidden read-after-writes. For example:

1. Refuse to translate code containing a hidden read-after-write. Exit with an error explaining the problem and possible workarounds (such as adding additional labels or manually inlining the definition that hides the read).

2. Automatically inline definitions like x_alias that hide a read-after-write. Then, x' can be used in place of x.

There may be other options as well.

To respond to a few of the points Dr. Lamport made back in 2015:

The basic rule is that the PlusCal translator does not expand definitions; [...] Given this rule, there is nothing the translator can or should do.

Then I think the rule should be changed. It leads to surprising behavior that contradicts other parts of the manual, and I can't see a good reason to keep it. Even if there is an implementation-level reason why the rule exists, I still feel that we should find a way to overcome it and fix this problem.

in general, the definition could contain variables that both "should" and "shouldn't" be primed.  Also, since the user could have defined B1 to equal b1' in your example, it's not at all clear what he would want the translator to do.

These are two very good points. The first can be overcome if the programmer or translator inlines the definition that hides the read. The second is trickier, and suggests that my first suggestion above is the right choice.

I hope we can decide on a course of action and get a fix out soon.

--

Calvin

--

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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e1d154c8-d6a8-40dc-be3c-33da8faf3446%40googlegroups.com.

[Leslie Lamport]

PlusCal had modest goals, and I am gratified that it is being used
enough to make its limitations a problem.  A solution that requires
the translator to expand the definitions would entail a lot of work.
Detecting and warning about the problem would be much
easier--especially because only definitions in the algorithm's define
clause need to be examined, since operators defined in the module that
appear in the algorithm can't contain variables.

An algorithm that detects a problem can also detect if the problem can
be resolved without expanding the definition--either by using the
defined operator unprimed or by priming it.  Priming can cause rare
problems--for example priming Op in the expression

   Op => /\ ...
         /\ ..

and I'm not sure how easy they would be to avoid. 

Without attempting to prime when possible, I estimate that it would
take between one and two months to implement the solution.  I don't
have time to do it myself, but I'll be happy to provide what
assistance I can to anyone who wants to give it a try.

Leslie

P.S. I would appreciate it if someone could identify the places in

the PlusCal manual that need to be changed because of this problem.

L.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe.

[Calvin Loncaric]

Unfortunately I don't have the time to help fix the problem, but I did my best to find the parts of the manual that need changing. I think the only parts that need correction are the two that Dan mentioned earlier.

In section 1:

"... uniprocess (sequential) algorithms, where the partitioning of the computation into steps does not affect the values computed."

There should be a note that there is one known exception to this rule, and a forward reference to whatever section explains the exception (perhaps 3.6).

In section 3.6:

"Definitions, including ones in a define statement, are not expanded in the PlusCal to TLA+ translation."

There should be some text here explaining the surprising implication here. Perhaps "As a result, definitions can hide variable uses from the PlusCal translator. This can cause definitions to read an old value of the variable, even if their use is preceded by an assignment. [insert example]". The manual could also note that macros do not exhibit this surprising behavior.

Optionally:

Sections 2.7 and 3.7, which discuss label placement, could also mention that label placement can affect what values get computed in uniprocess algorithms.

Section 3.2.1, which discusses the assignment statement, could also mention that while assignments affect all subsequent statements (as one would expect in an imperative language), using extra TLA+ definitions can thwart this behavior.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/88a4b115-ddd8-4d36-843e-f5115812357d%40googlegroups.com.

[Leslie Lamport]

Yes, this is a continuation of a conversation from more than a year

ago.  It was the result of something pretty obvious that I happened to

realize this morning.

First, I should apologize for not updating the PlusCal manual as

recommended by Calvin Loncaric.  As I'm afraid happens too often, I 

didn't get to it right away and then I forgot about it.  I will do

it today.

Now, the realization.  It's not a solution to the problem, but it's a

hack that can get around and even make use of the problem when you're

aware of it.  The PlusCal translator treats ' (prime) as if it were an

ordinary operator.  How you can make use of this is illustrated by the

following algorithm:

   --algorithm Test {

      variable x = 0 ;

      define {xxp == {x, x'}  xp == x}

      { x := 1 ;

        print <<xxp , xp'>>

      }

   }

   

which prints  <<{0, 1}, 1>> .  This will work only if each use of a

primed variable appears after an assignment to that variable in the

current step. (In other words, an assignment to the variable must

appear between the use and the preceding label.)

Note that explicitly primed variables can appear in the algorithm only

inside a definition.

Leslie

[Dan Tisdall]

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.

[Robin Luiten]

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

```

[Robin Luiten]

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.

[Stephan Merz]

    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

--
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+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/41971ee3-b348-4cd7-85e4-9402307d50e8n%40googlegroups.com.

[Robin Luiten]

Thank you so much Stephan, I am still learning and I believe part of my problem was confusing order not matter in TLA+ with PlusCal I believe.

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/vNPlerNO5yQ/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4947E10C-5716-4E8C-B95B-4C657130FC5B%40gmail.com.