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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Tue, 15 Dec 2020 11:25:36 -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>

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

On Saturday, November 2, 2019 at 1:00:50 PM UTC-7 Calvin Loncaric wrote:

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.

On Tue, Jul 30, 2019 at 11:52 AM Leslie Lamport <tlapl...@xxxxxxxxx> wrote:--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.LeslieP.S. I would appreciate it if someone could identify the places inthe PlusCal manual that need to be changed because of this problem.L.

On Tuesday, July 30, 2019 at 11:15:22 AM UTC-7, Calvin Loncaric wrote: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.--CalvinOn Mon, Jul 22, 2019, 5:13 PM Daniel Ricketts <daniel ricketts> wrote:--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 computedIt 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?On Thursday, October 22, 2015 at 7:03:57 AM UTC-7, Giuliano wrote: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

On Wednesday, October 21, 2015 at 4:16:13 AM UTC-4, Leslie Lamport wrote: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:Hello, consider the following algorithm:--algorithm Algo1 {variables b1 = FALSE, b2 = FALSEdefine {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

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e1d154c8-d6a8-40dc-be3c-33da8faf3446%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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/88a4b115-ddd8-4d36-843e-f5115812357d%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/4a97c30c-e004-4787-b455-9392222e2dcfn%40googlegroups.com.

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

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

- Prev by Date:
**[tlaplus] Re: Question: Given a system where an input can be any int, how can you describe it with TLA+ in a way that TLC can check?** - Next by Date:
**[tlaplus] How do define a higher-order CONSTANT operator?** - 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):