Re: Potentially confusing behavior of a PlusCal algorithm

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