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

*From*: Daniel Ricketts <daniel.bmore.ricketts@xxxxxxxxx>*Date*: Mon, 22 Jul 2019 17:13:31 -0700 (PDT)*References*: <4d003c31-6b8c-4782-8885-65649ffe5fbe@googlegroups.com> <737588d7-2282-4ebb-aceb-174940a1f8ae@googlegroups.com> <0f378b2a-24d0-4821-b309-6e1366a63bfe@googlegroups.com>

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;

}

}

{

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?

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

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

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

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

- Prev by Date:
**[tlaplus] Re: BUG: temporal properties are incorrectly evaluated** - Next by Date:
**[tlaplus] for all, the transition condition is true?** - Previous by thread:
**Re: Potentially confusing behavior of a PlusCal algorithm** - Next by thread:
**Re: [tlaplus] Re: Potentially confusing behavior of a PlusCal algorithm** - Index(es):